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.

3 files changed, 187 insertions, 16 deletions

diff --git a/gnu/local.mk b/gnu/local.mk
index b1eb41d4fc..a5c0486c94 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -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		\
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 8d967241f5..cf0c67f214 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -49,10 +49,10 @@
   #: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 @@
        (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 @@ It is developed using Objective Caml and Camlp5.")
     ;; 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 @@ theorems between the two libraries.")
 (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 @@ theorems between the two libraries.")
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "1n66i7hd9222b2ks606mak7m4f0dgy02xgygjskmmav6h7g2sx7y"))))
+                "0jsgdvj0ddhkls32krprp34r64y1rb5mwxl34fgaxk2k4664yq06"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("ocaml" ,ocaml)
@@ -537,16 +568,16 @@ uses Ltac to synthesize the substitution operation.")
 (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)
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 <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