From 5179f4525d0859794b0d75ee1792d0f731d1f9c4 Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Fri, 11 Feb 2022 08:42:22 +0100 Subject: gnu: coq: Update to 8.15.0. * gnu/packages/coq.scm (coq): Update to 8.15.0. (coq-equations): Update to 1.3-8.15. * gnu/packages/patches/coq-fix-envvars.patch: Adapt to new version. --- gnu/packages/coq.scm | 8 +- gnu/packages/patches/coq-fix-envvars.patch | 148 ++++++----------------------- 2 files changed, 35 insertions(+), 121 deletions(-) diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm index bdd57cd47c..13c0a2f9db 100644 --- a/gnu/packages/coq.scm +++ b/gnu/packages/coq.scm @@ -52,7 +52,7 @@ (define-public coq-core (package (name "coq-core") - (version "8.14.1") + (version "8.15.0") (source (origin (method git-fetch) @@ -62,7 +62,7 @@ (file-name (git-file-name name version)) (sha256 (base32 - "0q634fmrh5ivpxy7ammdiqdh9xp72ji2726vcz1bd55ln0d08z40")) + "0473mmc4wv8zbbcbvqqn0z9gz9y8gf4w2q6j6h50lx0jphpg2n8z")) (patches (search-patches "coq-fix-envvars.patch")))) (native-search-paths (list (search-path-specification @@ -546,11 +546,11 @@ uses Ltac to synthesize the substitution operation.") (method git-fetch) (uri (git-reference (url "https://github.com/mattam82/Coq-Equations") - (commit (string-append "v" version "-8.14")))) + (commit (string-append "v" version "-8.15")))) (file-name (git-file-name name version)) (sha256 (base32 - "19bj9nncd1r9g4273h5qx35gs3i4bw5z9bhjni24b413hyj55hkv")))) + "1vfcfpsp9zyj0sw0cwibk76nj6n0r6gwh8m1aa3lbvc0b1kbm32k")))) (build-system gnu-build-system) (native-inputs (list ocaml coq camlp5)) diff --git a/gnu/packages/patches/coq-fix-envvars.patch b/gnu/packages/patches/coq-fix-envvars.patch index deecf5ce74..6c48224c64 100644 --- a/gnu/packages/patches/coq-fix-envvars.patch +++ b/gnu/packages/patches/coq-fix-envvars.patch @@ -1,63 +1,44 @@ -From ebe09fcac72b21d17c4e8fe6edc1b6076a4ae97c Mon Sep 17 00:00:00 2001 +From 0e76cda958a4d3e4bcbb96e171c26b6b3478c6c2 Mon Sep 17 00:00:00 2001 From: Julien Lepiller -Date: Sun, 21 Nov 2021 00:38:03 +0100 +Date: Thu, 10 Feb 2022 16:44:10 +0100 Subject: [PATCH] Fix environment variable usage. --- - checker/checker.ml | 2 ++ - lib/envars.ml | 26 ++++++++++++++++---------- - sysinit/coqargs.ml | 3 ++- - sysinit/coqloadpath.ml | 3 ++- - sysinit/coqloadpath.mli | 2 +- - tools/coqdep.ml | 2 +- - 6 files changed, 24 insertions(+), 14 deletions(-) + boot/env.ml | 26 +++++++++++++++++++------- + 1 file changed, 19 insertions(+), 7 deletions(-) -diff --git a/checker/checker.ml b/checker/checker.ml -index f55ed9e8d6..3b797729ed 100644 ---- a/checker/checker.ml -+++ b/checker/checker.ml -@@ -104,6 +104,7 @@ let set_include d p = - (* Initializes the LoadPath *) - let init_load_path () = - let coqlib = Envars.coqlib () in -+ let coqcorelib = Envars.coqcorelib () in - let user_contrib = coqlib/"user-contrib" in - let xdg_dirs = Envars.xdg_dirs in - let coqpath = Envars.coqpath in -@@ -111,6 +112,7 @@ let init_load_path () = - CPath.choose_existing - [ CPath.make [ coqlib ; "plugins" ] - ; CPath.make [ coqlib ; ".."; "coq-core"; "plugins" ] -+ ; CPath.make [ coqcorelib ; "plugins" ] - ] |> function - | None -> - CErrors.user_err (Pp.str "Cannot find plugins directory") -diff --git a/lib/envars.ml b/lib/envars.ml -index 750bd60e71..c7affbd437 100644 ---- a/lib/envars.ml -+++ b/lib/envars.ml -@@ -127,15 +127,21 @@ let check_file_else ~dir ~file oth = - let guess_coqlib fail = - getenv_else "COQLIB" (fun () -> +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 -- check_file_else ~dir:Coq_config.coqlibsuffix ~file:prelude +- Util.check_file_else +- ~dir:Coq_config.coqlibsuffix +- ~file:prelude - (fun () -> -- if Sys.file_exists (Coq_config.coqlib / prelude) +- 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.") -- ) -+ let coqlibpath = getenv_else "COQLIBPATH" (fun () -> Coq_config.coqlibsuffix) in +- 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 -> (check_file_else ~dir:dir ~file:prelude (fun () -> "")) <> "") ++ (fun dir -> (Util.check_file_else ~dir:dir ~file:prelude (fun () -> "")) <> "") + paths in + match valid_paths with + | [] -> -+ if Sys.file_exists (Coq_config.coqlib / prelude) ++ 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 \ @@ -65,75 +46,8 @@ index 750bd60e71..c7affbd437 100644 + If you intend to use Coq without a standard library, the -boot -noinit options must be used." + | p::_ -> p) - let coqlib_ref : string option ref = ref None - let set_user_coqlib path = coqlib_ref := Some path -@@ -208,7 +214,7 @@ let xdg_dirs ~warn = - let print_config ?(prefix_var_name="") f coq_src_subdirs = - let open Printf in - fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ()); -- fprintf f "%sCOQCORELIB=%s/\n" prefix_var_name (coqlib () / "../coq-core/"); -+ fprintf f "%sCOQCORELIB=%s/\n" prefix_var_name (coqcorelib ()); - fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ()); - fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ()); - fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; -diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml -index 00f70a5fea..8325623a63 100644 ---- a/sysinit/coqargs.ml -+++ b/sysinit/coqargs.ml -@@ -453,7 +453,8 @@ let build_load_path opts = - if opts.pre.boot then [],[] - else - let coqlib = Envars.coqlib () in -- Coqloadpath.init_load_path ~coqlib in -+ let coqcorelib = Envars.coqcorelib () in -+ Coqloadpath.init_load_path ~coqlib ~coqcorelib in - ml_path @ opts.pre.ml_includes , - vo_path @ opts.pre.vo_includes - -diff --git a/sysinit/coqloadpath.ml b/sysinit/coqloadpath.ml -index 95ae5da3de..a58cfe6928 100644 ---- a/sysinit/coqloadpath.ml -+++ b/sysinit/coqloadpath.ml -@@ -35,7 +35,7 @@ let build_userlib_path ~unix_path = - else [], [] - - (* LoadPath for Coq user libraries *) --let init_load_path ~coqlib = -+let init_load_path ~coqlib ~coqcorelib = - - let open Loadpath in - let user_contrib = coqlib/"user-contrib" in -@@ -50,6 +50,7 @@ let init_load_path ~coqlib = - CPath.choose_existing - [ CPath.make [ coqlib ; "plugins" ] - ; CPath.make [ coqlib ; ".."; "coq-core"; "plugins" ] -+ ; CPath.make [ coqcorelib ; "plugins" ] - ] |> function - | None -> - CErrors.user_err (Pp.str "Cannot find plugins directory") -diff --git a/sysinit/coqloadpath.mli b/sysinit/coqloadpath.mli -index d853e9ea54..43c6dfa134 100644 ---- a/sysinit/coqloadpath.mli -+++ b/sysinit/coqloadpath.mli -@@ -12,5 +12,5 @@ - includes (in-order) Coq's standard library, Coq's [user-contrib] - folder, and directories specified in [COQPATH] and [XDG_DIRS] *) - val init_load_path -- : coqlib:CUnix.physical_path -+ : coqlib:CUnix.physical_path -> coqcorelib:CUnix.physical_path - -> CUnix.physical_path list * Loadpath.vo_path list -diff --git a/tools/coqdep.ml b/tools/coqdep.ml -index c1c87993e1..6c78e10866 100644 ---- a/tools/coqdep.ml -+++ b/tools/coqdep.ml -@@ -33,7 +33,7 @@ let coqdep () = - let coqlib = Envars.coqlib () in - let coq_plugins_dir = Filename.concat (Envars.coqcorelib ()) "plugins" in - if not (Sys.file_exists coq_plugins_dir) then -- CErrors.user_err Pp.(str "coqdep: cannot find plugins directory for coqlib: " ++ str coqlib ++ fnl ()); -+ CErrors.user_err Pp.(str "coqdep: cannot find plugins directory " ++ str coq_plugins_dir ++ str " for coqlib: " ++ str coqlib ++ fnl ()); - CD.add_rec_dir_import CD.add_coqlib_known (coqlib//"theories") ["Coq"]; - CD.add_rec_dir_import CD.add_coqlib_known (coq_plugins_dir) ["Coq"]; - let user = coqlib//"user-contrib" in + (* Build layout uses coqlib = coqcorelib *) + let guess_coqcorelib lib = -- -2.33.1 +2.34.0 + -- cgit v1.2.3