@@ -951,6 +951,7 @@ dist_patch_DATA = \
%D%/packages/patches/collectd-5.11.0-noinstallvar.patch \
%D%/packages/patches/combinatorial-blas-awpm.patch \
%D%/packages/patches/combinatorial-blas-io-fix.patch \
+ %D%/packages/patches/coq-fix-envvars.patch \
%D%/packages/patches/coreutils-ls.patch \
%D%/packages/patches/cpuinfo-system-libraries.patch \
%D%/packages/patches/crawl-upgrade-saves.patch \
@@ -49,10 +49,10 @@ (define-module (gnu packages coq)
#:use-module (guix utils)
#:use-module ((srfi srfi-1) #:hide (zip)))
-(define-public coq
+(define-public coq-core
(package
- (name "coq")
- (version "8.13.2")
+ (name "coq-core")
+ (version "8.14.0")
(source
(origin
(method git-fetch)
@@ -62,25 +62,31 @@ (define-public coq
(file-name (git-file-name name version))
(sha256
(base32
- "15r0cm3p9dlsxbg0lf05njjp1xi1y74vxvq6drxjykax67x95l8a"))))
+ "0iachapmdwvwwlvkrb2yxhqqrgzs70zyr1c9v1jdb1awx3bp68hf"))
+ (patches (search-patches "coq-fix-envvars.patch"))))
(native-search-paths
(list (search-path-specification
(variable "COQPATH")
- (files (list "lib/coq/user-contrib")))
+ (files (list "lib/ocaml/site-lib/coq/user-contrib"
+ "lib/coq/user-contrib")))
(search-path-specification
- (variable "COQLIB")
- (files (list "lib/ocaml/site-lib/coq"))
+ (variable "COQLIBPATH")
+ (files (list "lib/ocaml/site-lib/coq")))
+ (search-path-specification
+ (variable "COQCORELIB")
+ (files (list "lib/ocaml/site-lib/coq-core"))
(separator #f))))
(build-system dune-build-system)
(inputs
`(("gmp" ,gmp)
("ocaml-zarith" ,ocaml-zarith)))
(native-inputs
- `(("which" ,which)))
+ `(("ocaml-ounit2" ,ocaml-ounit2)
+ ("which" ,which)))
(arguments
- `(#:package "coq"
- #:test-target "test-suite"))
- (properties '((upstream-name . "coq"))) ; for inherited packages
+ `(#:package "coq-core"
+ #:test-target "."))
+ (properties '((upstream-name . "coq"))) ; also for inherited packages
(home-page "https://coq.inria.fr")
(synopsis "Proof assistant for higher-order logic")
(description
@@ -91,6 +97,31 @@ (define-public coq
;; Some of the documentation is distributed under opl1.0+.
(license (list license:lgpl2.1 license:opl1.0+))))
+(define-public coq-stdlib
+ (package
+ (inherit coq-core)
+ (name "coq-stdlib")
+ (arguments
+ `(#:package "coq-stdlib"
+ #:test-target "."))
+ (inputs
+ `(("coq-core" ,coq-core)
+ ("gmp" ,gmp)
+ ("ocaml-zarith" ,ocaml-zarith)))
+ (native-inputs '())))
+
+(define-public coq
+ (package
+ (inherit coq-core)
+ (name "coq")
+ (arguments
+ `(#:package "coq"
+ #:test-target "."))
+ (propagated-inputs
+ `(("coq-core" ,coq-core)
+ ("coq-stdlib" ,coq-stdlib)))
+ (native-inputs '())))
+
(define-public coq-ide-server
(package
(inherit coq)
@@ -410,7 +441,7 @@ (define-public coq-coquelicot
(define-public coq-bignums
(package
(name "coq-bignums")
- (version "8.13.0")
+ (version "8.14.0")
(source (origin
(method git-fetch)
(uri (git-reference
@@ -419,7 +450,7 @@ (define-public coq-bignums
(file-name (git-file-name name version))
(sha256
(base32
- "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y"))))
+ "0jsgdvj0ddhkls32krprp34r64y1rb5mwxl34fgaxk2k4664yq06"))))
(build-system gnu-build-system)
(native-inputs
`(("ocaml" ,ocaml)
@@ -471,7 +502,7 @@ (define-public coq-interval
(arguments
`(#:configure-flags
(list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out")
- "/lib/coq/user-contrib"))
+ "/lib/ocaml/site-lib/coq/user-contrib"))
#:phases
(modify-phases %standard-phases
(add-before 'configure 'fix-remake
@@ -537,16 +568,16 @@ (define-public coq-autosubst
(define-public coq-equations
(package
(name "coq-equations")
- (version "1.2.4")
+ (version "1.3")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/mattam82/Coq-Equations")
- (commit (string-append "v" version "-8.13"))))
+ (commit (string-append "v" version "-8.14"))))
(file-name (git-file-name name version))
(sha256
(base32
- "0i014lshsdflzw6h0qxra9d2f0q82vffxv2f29awbb9ad0p4rq4q"))))
+ "19bj9nncd1r9g4273h5qx35gs3i4bw5z9bhjni24b413hyj55hkv"))))
(build-system gnu-build-system)
(native-inputs
`(("ocaml" ,ocaml)
new file mode 100644
@@ -0,0 +1,139 @@
+From ebe09fcac72b21d17c4e8fe6edc1b6076a4ae97c Mon Sep 17 00:00:00 2001
+From: Julien Lepiller <julien@lepiller.eu>
+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