From 4b941ab3d5dea321e1fd96dd21faf346258e2d80 Mon Sep 17 00:00:00 2001 From: pukkamustard Date: Wed, 10 Jan 2024 08:43:10 +0100 Subject: gnu: coq: Update to 8.17.1. * gnu/packages/coq.scm (coq): Update to 8.17.1 and merge with coq-core and coq-stdlib. [arguments] Merge with coq-core and coq-stdlib. Add pre-build phases and add a custom install phase. Remove unnecessary test-target. [source](patches): Remove. [native-search-paths]: Remove COQLIBPATH and COQCORELIB. (coq-core): Remove variable. (coq-stdlib): Remove variable. (coq-ide)[propagated-inputs]: Add zlib. (coq-mathcomp-bigenough)[propagated-inputs]: Remove coq-core. (coq-mathcomp-finmap)[inputs]: Remove coq-stdlib. (coq-equations): Update to 1.3-8.17. * gnu/packages/patches/coq-fix-envvars.patch: Delete file. * gnu/local.mk (dist_patch_DATA): Adjust accordingly. Co-authored-by: Josselin Poiret Signed-off-by: Julien Lepiller Change-Id: I0a0d9f7a6e06dd19ce1b66051334476d85f4f195 --- gnu/packages/patches/coq-fix-envvars.patch | 53 ------------------------------ 1 file changed, 53 deletions(-) delete mode 100644 gnu/packages/patches/coq-fix-envvars.patch (limited to 'gnu/packages/patches') 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 - -- cgit v1.2.3