05/06: gnu: coq: Update to 8.15.0.

[guix-commits]

roptat pushed a commit to branch master
in repository guix.

commit 5179f4525d0859794b0d75ee1792d0f731d1f9c4
Author: Julien Lepiller <julien@lepiller.eu>
AuthorDate: Fri Feb 11 08:42:22 2022 +0100

    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 <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
+