Package: guix-patches;
Reported by: pukkamustard <pukkamustard <at> posteo.net>
Date: Fri, 23 Jun 2023 13:45:02 UTC
Severity: normal
Tags: patch
Done: Julien Lepiller <julien <at> lepiller.eu>
Bug is archived. No further changes may be made.
View this message in rfc822 format
From: Josselin Poiret <dev <at> jpoiret.xyz> To: pukkamustard <pukkamustard <at> posteo.net>, 64249 <at> debbugs.gnu.org Cc: Julien Lepiller <julien <at> lepiller.eu>, Josselin Poiret <dev <at> jpoiret.xyz>, Julien Lepiller <julien <at> lepiller.eu>, pukkamustard <pukkamustard <at> posteo.net> Subject: [bug#64249] [PATCH] fixup! gnu: coq: Update to 8.17.1. Date: Tue, 12 Sep 2023 13:31:06 +0200
From: Josselin Poiret <dev <at> jpoiret.xyz>
---
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
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 <julien <at> lepiller.eu>
-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
-
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
--
2.41.0
GNU bug tracking system
Copyright (C) 1999 Darren O. Benham,
1997,2003 nCipher Corporation Ltd,
1994-97 Ian Jackson.