[bug#52164] [PATCH] gnu: coq: Update to 8.14.0.

[bug#52164] [PATCH] gnu: coq: Update to 8.14.0.

[Julien Lepiller]

Hi Guix!

this small series updates coq to its latest version.

[bug#52164] [PATCH 1/3] gnu: ocaml-semantics: Update to 8.14.0.

[Julien Lepiller]

---
 gnu/packages/coq.scm | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index a27ec53ecb..e3c4190ac3 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -576,7 +576,7 @@ (define-public coq-equations
 (define-public coq-semantics
   (package
     (name "coq-semantics")
-    (version "8.13.0")
+    (version "8.14.0")
     (source
       (origin
         (method git-fetch)
@@ -591,7 +591,7 @@ (define-public coq-semantics
         (file-name (git-file-name name version))
         (sha256
          (base32
-          "0m5si9dsv96z92gy4xaqz8mzyz8zp7j1sp542l0wzsp5xgyfpc7i"))))
+          "0ldrp86bfcjpzsb08p45sgs3aczjzr1gksy5dsf7pxapg05pc7ac"))))
     (build-system gnu-build-system)
     (native-inputs
      `(("coq" ,coq)
-- 
2.33.1

[bug#52164] [PATCH 1/3] gnu: ocaml-semantics: Update to 8.14.0.

[zimoun]

Hi Julien,

Maybe something had been twisted.

 1. Missing changelog.

 2. Incorrect package name in commit oneline: coq-semantics and not
    ocaml-semantics.

Cheers,
simon


On dim., 28 nov. 2021 at 18:27, Julien Lepiller <julien@lepiller.eu> wrote:
> ---
>  gnu/packages/coq.scm | 4 ++--
>  1 file changed, 2 insertions(+), 2 deletions(-)
>
> diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
> index a27ec53ecb..e3c4190ac3 100644
> --- a/gnu/packages/coq.scm
> +++ b/gnu/packages/coq.scm
> @@ -576,7 +576,7 @@ (define-public coq-equations
>  (define-public coq-semantics
>    (package
>      (name "coq-semantics")
> -    (version "8.13.0")
> +    (version "8.14.0")
>      (source
>        (origin
>          (method git-fetch)
> @@ -591,7 +591,7 @@ (define-public coq-semantics
>          (file-name (git-file-name name version))
>          (sha256
>           (base32
> -          "0m5si9dsv96z92gy4xaqz8mzyz8zp7j1sp542l0wzsp5xgyfpc7i"))))
> +          "0ldrp86bfcjpzsb08p45sgs3aczjzr1gksy5dsf7pxapg05pc7ac"))))
>      (build-system gnu-build-system)
>      (native-inputs
>       `(("coq" ,coq)

[bug#52164] [PATCH 2/3] gnu: proof-general: Update to latest commit.

[Julien Lepiller]

* gnu/packages/coq.scm (proof-general): Update to latest commit.
---
 gnu/packages/coq.scm | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index e3c4190ac3..2045901aed 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -119,9 +119,9 @@ (define-public coq-ide
 (define-public proof-general
   ;; The latest release is from 2016 and there has been more than 450 commits
   ;; since then.
-  ;; Commit from 2021-06-07.
-  (let ((commit "bc86736abb728ec0d28abc90ef0adae21d29a66a")
-        (revision "0"))
+  ;; Commit from 2021-11-25.
+  (let ((commit "1b1083e86e0cddc20ff2f1a6b25c7a7eee2edf02")
+        (revision "1"))
     (package
       (name "proof-general")
       (version (git-version "4.4" revision commit))
@@ -133,7 +133,7 @@ (define-public proof-general
                 (file-name (git-file-name name version))
                 (sha256
                  (base32
-                  "00cga3n9nj2xa3ivb0fdkkdx3k11fp4879y188738631yd1x2lsa"))))
+                  "1pnysczhscapgwmvf6ix7f31lf3hnh8h977bfll1m7jlxl9b9c0j"))))
       (build-system gnu-build-system)
       (native-inputs
        `(("emacs" ,emacs-minimal)
-- 
2.33.1

[bug#52164] [PATCH] gnu: coq: Update to 8.14.0.

[zimoun]

On dim., 28 nov. 2021 at 18:27, Julien Lepiller <julien@lepiller.eu> wrote:
> * gnu/packages/coq.scm (proof-general): Update to latest commit.
> ---
>  gnu/packages/coq.scm | 8 ++++----
>  1 file changed, 4 insertions(+), 4 deletions(-)

LGTM.

Cheers,
simon

[bug#52164] [PATCH 3/3] gnu: coq: Update to 8.14.0.

[Julien Lepiller]

* 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/local.mk                               |   1 +
 gnu/packages/coq.scm                       |  65 +++++++---
 gnu/packages/patches/coq-fix-envvars.patch | 139 +++++++++++++++++++++
 3 files changed, 188 insertions(+), 17 deletions(-)
 create mode 100644 gnu/packages/patches/coq-fix-envvars.patch

diff --git a/gnu/local.mk b/gnu/local.mk
index efe153faf2..b26907a211 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 2045901aed..b6a5ff357c 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -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)
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
-- 
2.33.1

[bug#52164] [PATCH] gnu: coq: Update to 8.14.0.

[zimoun]

Hi,

On dim., 28 nov. 2021 at 18:27, Julien Lepiller <julien@lepiller.eu> wrote:
> * 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/local.mk                               |   1 +
>  gnu/packages/coq.scm                       |  65 +++++++---
>  gnu/packages/patches/coq-fix-envvars.patch | 139 +++++++++++++++++++++
>  3 files changed, 188 insertions(+), 17 deletions(-)
>  create mode 100644 gnu/packages/patches/coq-fix-envvars.patch

[...]

> -(define-public coq
> +(define-public coq-core

[...]

> -     `(("which" ,which)))
> +     `(("ocaml-ounit2" ,ocaml-ounit2)
> +       ("which" ,which)))

This ’which’ could be removed. :-)


> +(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 '())))

With this approach, 3 builds.  Is it required by kind-of Coq bootstrap?


>  (define-public coq-bignums
>    (package
>      (name "coq-bignums")
> -    (version "8.13.0")
> +    (version "8.14.0")

This…

>  (define-public coq-equations
>    (package
>      (name "coq-equations")
> -    (version "1.2.4")
> +    (version "1.3")

and this… Cannot they be upgraded by a separated commit?

They will probably be broken with Coq 8.13 but if their upgrade is right
after and pushed with the same batch, it is transparent and the
atomicity appears to me better.


> 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(-)

This fix LGTM.


Otherwise, LTGM.


Cheers,
simon

[bug#52164] [PATCH] gnu: coq: Update to 8.14.0.

[Julien Lepiller]

Le 29 novembre 2021 04:42:25 GMT-05:00, zimoun <zimon.toutoune@gmail.com> a écrit :
>Hi,
>
>On dim., 28 nov. 2021 at 18:27, Julien Lepiller <julien@lepiller.eu> wrote:
>> * 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/local.mk                               |   1 +
>>  gnu/packages/coq.scm                       |  65 +++++++---
>>  gnu/packages/patches/coq-fix-envvars.patch | 139 +++++++++++++++++++++
>>  3 files changed, 188 insertions(+), 17 deletions(-)
>>  create mode 100644 gnu/packages/patches/coq-fix-envvars.patch
>
>[...]
>
>> -(define-public coq
>> +(define-public coq-core
>
>[...]
>
>> -     `(("which" ,which)))
>> +     `(("ocaml-ounit2" ,ocaml-ounit2)
>> +       ("which" ,which)))
>
>This ’which’ could be removed. :-)
>
>
>> +(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 '())))
>
>With this approach, 3 builds.  Is it required by kind-of Coq bootstrap?

Coq now uses dune, and it is split into core, stdlib anl coq. I prefer to build one dune package in each guix package, rather than everything, especially since we want to separate coq-ide.

>
>
>>  (define-public coq-bignums
>>    (package
>>      (name "coq-bignums")
>> -    (version "8.13.0")
>> +    (version "8.14.0")
>
>This…
>
>>  (define-public coq-equations
>>    (package
>>      (name "coq-equations")
>> -    (version "1.2.4")
>> +    (version "1.3")
>
>and this… Cannot they be upgraded by a separated commit?
>
>They will probably be broken with Coq 8.13 but if their upgrade is right
>after and pushed with the same batch, it is transparent and the
>atomicity appears to me better.

They're broken with coq 8.13, and the previous version is also broken with coq 8.14. This is why I was able to update coq semantics independently but not these two.

>
>
>> 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(-)
>
>This fix LGTM.
>
>
>Otherwise, LTGM.
>
>
>Cheers,
>simon

[bug#52164] [PATCH] gnu: coq: Update to 8.14.0.

[zimoun]

Hi Julien,

On Mon, 29 Nov 2021 at 13:30, Julien Lepiller <julien@lepiller.eu> wrote:

> >With this approach, 3 builds.  Is it required by kind-of Coq bootstrap?
>
> Coq now uses dune, and it is split into core, stdlib anl coq. I prefer to build one dune package in each guix package, rather than everything, especially since we want to separate coq-ide.

Thanks for the explanations.  So LGTM. :-)


> >>  (define-public coq-bignums
> >>    (package
> >>      (name "coq-bignums")
> >> -    (version "8.13.0")
> >> +    (version "8.14.0")
> >
> >This…
> >
> >>  (define-public coq-equations
> >>    (package
> >>      (name "coq-equations")
> >> -    (version "1.2.4")
> >> +    (version "1.3")
> >
> >and this… Cannot they be upgraded by a separated commit?
> >
> >They will probably be broken with Coq 8.13 but if their upgrade is right
> >after and pushed with the same batch, it is transparent and the
> >atomicity appears to me better.
>
> They're broken with coq 8.13, and the previous version is also broken with coq 8.14. This is why I was able to update coq semantics independently but not these two.

Hum, the breakage of coq-bignums or coq-equations is recent.  Because
using 65234d0 from Nov. 2nd, they are substituable; using coq@8.13.2.
Or do you mean that coq-binums@8.13 is broken with coq@8.14?

In all cases, it appears to me clearer to have:

 1. update coq
 2. update coq-bignums
 3. update coq-equations

i.e., update the "compiler" and fix then the breakage introduced by
this "compiler" upgrade, e.g., upgrade other packages.  We are always
doing like that, no?


Cheers,
simon

[bug#52164] [PATCH] gnu: coq: Update to 8.14.0.

[Julien Lepiller]

>
>Hum, the breakage of coq-bignums or coq-equations is recent.  Because
>using 65234d0 from Nov. 2nd, they are substituable; using coq@8.13.2.
>Or do you mean that coq-binums@8.13 is broken with coq@8.14?

I meant to say bignums 8.13 is broken with coq 8.14, and bignums 8.14 is broken with coq 8.13.

>
>In all cases, it appears to me clearer to have:
>
> 1. update coq
> 2. update coq-bignums
> 3. update coq-equations
>
>i.e., update the "compiler" and fix then the breakage introduced by
>this "compiler" upgrade, e.g., upgrade other packages.  We are always
>doing like that, no?

I've always updated dependents first whenever possible (without breaking anything), then the compiler, then the rest that needs the new compiler. However, I've always been careful not to introduce breakage with a commit, even if it's inside a series. I think that's the policiy, but I'm not sure if it overrides the one-change per commit policy.

>
>
>Cheers,
>simon

[bug#52164] [PATCH] gnu: coq: Update to 8.14.0.

[zimoun]

Re,

On Mon, 29 Nov 2021 at 14:39, Julien Lepiller <julien@lepiller.eu> wrote:

> I've always updated dependents first whenever possible (without breaking anything), then the compiler, then the rest that needs the new compiler. However, I've always been careful not to introduce breakage with a commit, even if it's inside a series. I think that's the policiy, but I'm not sure if it overrides the one-change per commit policy.

Me neither. :-)
Anyway, all LGTM except wrong commit message for coq-semantics.

Cheers,
simon

bug#52164: [PATCH] gnu: coq: Update to 8.14.0.

[zimoun]

Hi Julien,

On Sun, 28 Nov 2021 at 17:44, Julien Lepiller <julien@lepiller.eu> wrote:

> this small series updates coq to its latest version.

This series [1] updated Coq at 8.14 and the current Coq is 8.15.

1: <https://issues.guix.gnu.org/issue/52164>

So closing!

Cheers,
simon