From patchwork Tue Sep 12 11:31:06 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Josselin Poiret X-Patchwork-Id: 53760 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 1948527BBE9; Tue, 12 Sep 2023 12:36:42 +0100 (BST) X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-0.7 required=5.0 tests=BAYES_00,DKIM_INVALID, DKIM_SIGNED,FROM_SUSPICIOUS_NTLD,MAILING_LIST_MULTI,PDS_OTHER_BAD_TLD, SPF_HELO_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no version=3.4.6 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTPS id 6245E27BBE2 for ; Tue, 12 Sep 2023 12:36:40 +0100 (BST) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1qg1cz-0005of-8m; Tue, 12 Sep 2023 07:32:21 -0400 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1qg1ck-0005l2-Hp for guix-patches@gnu.org; Tue, 12 Sep 2023 07:32:10 -0400 Received: from debbugs.gnu.org ([2001:470:142:5::43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1qg1cg-00014D-UU for guix-patches@gnu.org; Tue, 12 Sep 2023 07:32:06 -0400 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1qg1cg-0007Ls-31; Tue, 12 Sep 2023 07:32:02 -0400 X-Loop: help-debbugs@gnu.org Subject: [bug#64249] [PATCH] fixup! gnu: coq: Update to 8.17.1. Resent-From: Josselin Poiret Original-Sender: "Debbugs-submit" Resent-CC: julien@lepiller.eu, pukkamustard@posteo.net, guix-patches@gnu.org Resent-Date: Tue, 12 Sep 2023 11:32:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 64249 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: pukkamustard , 64249@debbugs.gnu.org Cc: Julien Lepiller , Josselin Poiret , Julien Lepiller , pukkamustard X-Debbugs-Original-Xcc: Julien Lepiller , pukkamustard Received: via spool by 64249-submit@debbugs.gnu.org id=B64249.169451830028230 (code B ref 64249); Tue, 12 Sep 2023 11:32:02 +0000 Received: (at 64249) by debbugs.gnu.org; 12 Sep 2023 11:31:40 +0000 Received: from localhost ([127.0.0.1]:56310 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1qg1cK-0007LG-7E for submit@debbugs.gnu.org; Tue, 12 Sep 2023 07:31:40 -0400 Received: from jpoiret.xyz ([206.189.101.64]:40060) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1qg1cC-0007Kp-Cp for 64249@debbugs.gnu.org; Tue, 12 Sep 2023 07:31:35 -0400 Received: from authenticated-user (jpoiret.xyz [206.189.101.64]) by jpoiret.xyz (Postfix) with ESMTPA id C3C00184D43; Tue, 12 Sep 2023 11:31:24 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=jpoiret.xyz; s=dkim; t=1694518285; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=ZEDLNjLNA4/CQSSkZxqNdA5M+mmwYfyx5H/OwS2ggtI=; b=nprYa0X0BzjqCrFxSBqoP7RbTDA3N34LiChcp7rWyXsprFzEtrV4Y0G7F/9MHww1L9kvGO miMT2giGzvWZ8IMudJDomqbvbBwPZI77DlEaHyoEiGfo/RL3TCKHOH2McgkHsXF3Y6kU3P 8XEytt1syn/kUwJqD4h0oYaTGs2RCdrq8K01KURVxVON558HhW/NLMpcCMNeaghvFV02ov qWJzHdZM/YU7y6DLziBCil+5SI15a8eRRP64Zev4UqL+v8G7915k+Hq3dkZOp4z0oYKaFL 57jx1Vww4nzegVmHST4RvfR62Ho4k8Na9Ho4Jf6uYelHs1JEBnTknp80E1p4jA== Date: Tue, 12 Sep 2023 13:31:06 +0200 Message-ID: <4c1fa55b62e1e172f123f18a334575c7c0a4f7a9.1694517929.git.dev@jpoiret.xyz> In-Reply-To: <11daee2634fa3df963864662c6c3aba35f63d90c.1694501410.git.pukkamustard@posteo.net> References: <11daee2634fa3df963864662c6c3aba35f63d90c.1694501410.git.pukkamustard@posteo.net> MIME-Version: 1.0 X-Spamd-Bar: ++++ Authentication-Results: jpoiret.xyz; auth=pass smtp.auth=jpoiret@jpoiret.xyz smtp.mailfrom=dev@jpoiret.xyz X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Reply-to: Josselin Poiret X-ACL-Warn: , Josselin Poiret via Guix-patches X-Patchwork-Original-From: Josselin Poiret via Guix-patches via From: Josselin Poiret Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org X-getmail-retrieved-from-mailbox: Patches From: Josselin Poiret --- Hi pukkamustard, Since we're dropping the coq-core and coq-stdlib separation, why not get rid of all our custom stuff that came with it? Here's a fixup patch that does precisely that! Best, gnu/local.mk | 1 - gnu/packages/coq.scm | 49 ++++++++------------ gnu/packages/patches/coq-fix-envvars.patch | 53 ---------------------- 3 files changed, 20 insertions(+), 83 deletions(-) delete mode 100644 gnu/packages/patches/coq-fix-envvars.patch base-commit: 9996896dc252a02ba3b17473a685ce8957237546 prerequisite-patch-id: 86064275d4e6973b4c6e0e92928e9f0492f1c1e8 prerequisite-patch-id: 1e373b37413142bb32fa4a3eac0c429cc06aade6 prerequisite-patch-id: 62f9047b558dc9ad8be2415eda1ca5a7f45afbd5 prerequisite-patch-id: f419c33161039acab8d70e190fbcf155ce69c392 prerequisite-patch-id: d03ea10df36ace9b645d943ee867c8ae3837871e prerequisite-patch-id: fa3b358bf025ea4632af1d04265129af844583c3 prerequisite-patch-id: 30facf29a23518f813ee17eb213c9dda2c9891e9 prerequisite-patch-id: 4dffccb9ce6bc4446f8683035567e06d2dc7c98d prerequisite-patch-id: d33f5858aa29cc2a674b4bd53170fc3484e6bc2a prerequisite-patch-id: cde7bed13eeac7d6e836f2d02528885985f0fffb prerequisite-patch-id: c6b875244504ca1effdd8a81e96dab5f988607be prerequisite-patch-id: d04a32a675e2c778d3fa96eea636f44ae50b4968 diff --git a/gnu/local.mk b/gnu/local.mk index d9b4229729..8925e483b5 100644 --- a/gnu/local.mk +++ b/gnu/local.mk @@ -1036,7 +1036,6 @@ dist_patch_DATA = \ %D%/packages/patches/converseen-hide-non-free-pointers.patch \ %D%/packages/patches/cool-retro-term-wctype.patch \ %D%/packages/patches/coreutils-gnulib-tests.patch \ - %D%/packages/patches/coq-fix-envvars.patch \ %D%/packages/patches/cppcheck-disable-char-signedness-test.patch \ %D%/packages/patches/cpuinfo-system-libraries.patch \ %D%/packages/patches/cpulimit-with-glib-2.32.patch \ diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index d68f00a63c..6169b5f819 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -64,40 +64,31 @@ (define-public coq (file-name (git-file-name name version)) (sha256 (base32 - "0gg6hizq0i08lk741b579cbswhy6qvkh6inc3d3i5a2af98psq63")) - (patches (search-patches "coq-fix-envvars.patch")))) + "0gg6hizq0i08lk741b579cbswhy6qvkh6inc3d3i5a2af98psq63")))) (native-search-paths (list (search-path-specification (variable "COQPATH") - (files (list "lib/ocaml/site-lib/coq/user-contrib" - "lib/coq/user-contrib"))) - (search-path-specification - (variable "COQLIBPATH") - (files (list "lib/ocaml/site-lib/coq"))) - (search-path-specification - (variable "COQCORELIB") - (files (list "lib/ocaml/site-lib/coq-core")) - (separator #f)))) + (files (list "lib/coq/user-contrib"))))) (build-system dune-build-system) (arguments - `(#:package "coq-core,coq-stdlib,coq" - #:phases - (modify-phases %standard-phases - (add-before 'build 'configure - (lambda* (#:key outputs #:allow-other-keys) - (let* ((out (assoc-ref outputs "out")) - (libdir (string-append out "/lib/ocaml/site-lib"))) - (invoke "./configure" "-prefix" out - "-libdir" libdir)))) - (add-before 'build 'make-dunestrap - (lambda _ (invoke "make" "dunestrap"))) - (replace 'install - (lambda* (#:key outputs #:allow-other-keys) - (let* ((out (assoc-ref outputs "out")) - (libdir (string-append out "/lib/ocaml/site-lib"))) - (invoke "dune" "install" "--prefix" out - "--libdir" libdir - "coq-core" "coq-stdlib" "coq"))))))) + (list + #:package "coq-core,coq-stdlib,coq" + #:phases + #~(modify-phases %standard-phases + (add-before 'build 'configure + (lambda* (#:key outputs #:allow-other-keys) + (let* ((out (assoc-ref outputs "out")) + (coqlib (string-append out "/lib/ocaml/site-lib/coq/"))) + (invoke "./configure" "-prefix" out + "-libdir" coqlib)))) + (add-before 'build 'make-dunestrap + (lambda _ (invoke "make" "dunestrap"))) + (replace 'install + (lambda* (#:key outputs #:allow-other-keys) + (let* ((out (assoc-ref outputs "out")) + (libdir (string-append out "/lib/ocaml/site-lib"))) + (invoke "dune" "install" "--prefix" out + "--libdir" libdir "coq" "coq-core" "coq-stdlib"))))))) (inputs (list gmp ocaml-zarith)) (native-inputs diff --git a/gnu/packages/patches/coq-fix-envvars.patch b/gnu/packages/patches/coq-fix-envvars.patch deleted file mode 100644 index 6c48224c64..0000000000 --- a/gnu/packages/patches/coq-fix-envvars.patch +++ /dev/null @@ -1,53 +0,0 @@ -From 0e76cda958a4d3e4bcbb96e171c26b6b3478c6c2 Mon Sep 17 00:00:00 2001 -From: Julien Lepiller -Date: Thu, 10 Feb 2022 16:44:10 +0100 -Subject: [PATCH] Fix environment variable usage. - ---- - boot/env.ml | 26 +++++++++++++++++++------- - 1 file changed, 19 insertions(+), 7 deletions(-) - -diff --git a/boot/env.ml b/boot/env.ml -index e8521e7..d834a3a 100644 ---- a/boot/env.ml -+++ b/boot/env.ml -@@ -32,17 +32,29 @@ let fail_msg = - - let fail s = Format.eprintf "%s@\n%!" fail_msg; exit 1 - -+let path_to_list p = -+ let sep = if String.equal Sys.os_type "Win32" then ';' else ':' in -+ String.split_on_char sep p -+ - (* This code needs to be refactored, for now it is just what used to be in envvars *) - let guess_coqlib () = - Util.getenv_else "COQLIB" (fun () -> - let prelude = "theories/Init/Prelude.vo" in -- Util.check_file_else -- ~dir:Coq_config.coqlibsuffix -- ~file:prelude -- (fun () -> -- if Sys.file_exists (Filename.concat Coq_config.coqlib prelude) -- then Coq_config.coqlib -- else fail ())) -+ let coqlibpath = Util.getenv_else "COQLIBPATH" (fun () -> Coq_config.coqlibsuffix) in -+ let paths = path_to_list coqlibpath in -+ let valid_paths = -+ List.filter -+ (fun dir -> (Util.check_file_else ~dir:dir ~file:prelude (fun () -> "")) <> "") -+ paths in -+ match valid_paths with -+ | [] -> -+ if Sys.file_exists (Filename.concat Coq_config.coqlib prelude) -+ then Coq_config.coqlib -+ else -+ fail "cannot guess a path for Coq libraries; please use -coqlib option \ -+ or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) \ -+ If you intend to use Coq without a standard library, the -boot -noinit options must be used." -+ | p::_ -> p) - - (* Build layout uses coqlib = coqcorelib *) - let guess_coqcorelib lib = --- -2.34.0 -