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.
This commit is contained in:
Julien Lepiller
parent
6b6474fec7
commit
5179f4525d
@ -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))
|
||||
|
||||
@ -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 <julien@lepiller.eu>
|
||||
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
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user