From d95a982cdd898790d247f013440f08a448265e3f Mon Sep 17 00:00:00 2001 From: Julien Lepiller Date: Sun, 28 Nov 2021 16:42:56 +0100 Subject: gnu: coq: Update to 8.14.0. * gnu/packages/coq.scm (coq): Update to 8.14.0. (coq-bignums): Update to 8.14.0. (coq-equations): Update to 1.3. * gnu/packages/patches/coq-fix-envvars.patch: New file. * gnu/local.mk (dist_patch_DATA): Add it. --- gnu/packages/patches/coq-fix-envvars.patch | 139 +++++++++++++++++++++++++++++ 1 file changed, 139 insertions(+) create mode 100644 gnu/packages/patches/coq-fix-envvars.patch (limited to 'gnu/packages/patches/coq-fix-envvars.patch') diff --git a/gnu/packages/patches/coq-fix-envvars.patch b/gnu/packages/patches/coq-fix-envvars.patch new file mode 100644 index 0000000000..deecf5ce74 --- /dev/null +++ b/gnu/packages/patches/coq-fix-envvars.patch @@ -0,0 +1,139 @@ +From ebe09fcac72b21d17c4e8fe6edc1b6076a4ae97c Mon Sep 17 00:00:00 2001 +From: Julien Lepiller +Date: Sun, 21 Nov 2021 00:38:03 +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(-) + +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 () -> + let prelude = "theories/Init/Prelude.vo" in +- check_file_else ~dir:Coq_config.coqlibsuffix ~file:prelude +- (fun () -> +- if Sys.file_exists (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 ++ let paths = path_to_list coqlibpath in ++ let valid_paths = ++ List.filter ++ (fun dir -> (check_file_else ~dir:dir ~file:prelude (fun () -> "")) <> "") ++ paths in ++ match valid_paths with ++ | [] -> ++ if Sys.file_exists (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) + + 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 +-- +2.33.1 -- cgit v1.2.3