[PATCH] gnu: coq: Update to 8.14.0.

Done

Details

2 participants

Julien Lepiller
zimoun

Owner: unassigned

Submitted by: Julien Lepiller

Severity: normal

Julien Lepiller wrote on 28 Nov 2021 17:44

Recipients:(address . guix-patches@gnu.org)

Message-ID:20211128174408.747bccba@tachikoma.lepiller.eu

Hi Guix!

this small series updates coq to its latest version.

Julien Lepiller wrote on 28 Nov 2021 18:27

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

Recipients:(address . 52164@debbugs.gnu.org)

Message-ID:854d751e7d512c66acb72225120168e5ee16d6a2.1638120398.git.julien@lepiller.eu

---

gnu/packages/coq.scm | 4 ++--

1 file changed, 2 insertions(+), 2 deletions(-)

Toggle diff (24 lines)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

Julien Lepiller wrote on 28 Nov 2021 18:27

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

Recipients:(address . 52164@debbugs.gnu.org)

Message-ID:2e3b3fe2ed163577a854f10b9a1c8531eabcadf6.1638120398.git.julien@lepiller.eu

* gnu/packages/coq.scm (proof-general): Update to latest commit.

---

gnu/packages/coq.scm | 8 ++++----

1 file changed, 4 insertions(+), 4 deletions(-)

Toggle diff (28 lines)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

Julien Lepiller wrote on 28 Nov 2021 18:27

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

Recipients:(address . 52164@debbugs.gnu.org)

Message-ID:d62a5a234b89db4331c5bda48efa725fea18e97a.1638120398.git.julien@lepiller.eu

* 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

Toggle diff (296 lines)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

zimoun wrote on 29 Nov 2021 10:06

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

Recipients:(name . Julien Lepiller)(address . julien@lepiller.eu)(address . 52164@debbugs.gnu.org)

Message-ID:865ysbl4am.fsf_-_@gmail.com

On dim., 28 nov. 2021 at 18:27, Julien Lepiller <julien@lepiller.eu> wrote:

Toggle quote (5 lines)

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

zimoun wrote on 29 Nov 2021 10:42

Recipients:(name . Julien Lepiller)(address . julien@lepiller.eu)(address . 52164@debbugs.gnu.org)

Message-ID:8635nfl2m6.fsf_-_@gmail.com

Hi,

On dim., 28 nov. 2021 at 18:27, Julien Lepiller <julien@lepiller.eu> wrote:

Toggle quote (12 lines)> * 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

[...]

Toggle quote (3 lines)

> -(define-public coq

> +(define-public coq-core

[...]

Toggle quote (4 lines)

> - `(("which" ,which)))

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

> + ("which" ,which)))

This ’which’ could be removed. :-)

Toggle quote (25 lines)> +(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?

Toggle quote (6 lines)

> (define-public coq-bignums

> (package

> (name "coq-bignums")

> - (version "8.13.0")

> + (version "8.14.0")

This…

Toggle quote (6 lines)

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

Toggle quote (20 lines)> 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

zimoun wrote on 29 Nov 2021 10:05

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

Recipients:(name . Julien Lepiller)(address . julien@lepiller.eu)(address . 52164@debbugs.gnu.org)

Message-ID:868rx7l4bg.fsf_-_@gmail.com

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:

Toggle quote (26 lines)> ---
>  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)

Julien Lepiller wrote on 29 Nov 2021 13:29

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

Recipients:(name . zimoun)(address . zimon.toutoune@gmail.com)(address . 52164@debbugs.gnu.org)

Message-ID:592223CF-588B-44EF-A35F-9E9FDB3E4865@lepiller.eu

Le 29 novembre 2021 04:42:25 GMT-05:00, zimoun <zimon.toutoune@gmail.com> a écrit�:

Toggle quote (56 lines)>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.

Toggle quote (22 lines)>
>
>>  (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.

Toggle quote (30 lines)>
>
>> 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

zimoun wrote on 29 Nov 2021 14:21

Recipients:(name . Julien Lepiller)(address . julien@lepiller.eu)(address . 52164@debbugs.gnu.org)

Message-ID:CAJ3okZ23f-Vsm2fSJobjt3zLn+Wfy3YshfzKw4FtSLvQ2-YCzw@mail.gmail.com

Hi Julien,

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

Toggle quote (4 lines)

> >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. :-)

Toggle quote (22 lines)> >>  (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

Julien Lepiller wrote on 29 Nov 2021 14:39

Recipients:(name . zimoun)(address . zimon.toutoune@gmail.com)(address . 52164@debbugs.gnu.org)

Message-ID:89F34741-9EFC-4C19-8167-3B990D90533F@lepiller.eu

Toggle quote (5 lines)

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

Toggle quote (11 lines)>
>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.

Toggle quote (4 lines)

>Cheers,

>simon

zimoun wrote on 29 Nov 2021 15:13

Recipients:(name . Julien Lepiller)(address . julien@lepiller.eu)(address . 52164@debbugs.gnu.org)

Message-ID:CAJ3okZ31+VdRSe=z4nBcCQk7NXuwozK82Jnd2H-Nbk5p_-E=sg@mail.gmail.com

Re,

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

Toggle quote (2 lines)

> 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

zimoun wrote on 3 May 2022 14:35

Recipients:(name . Julien Lepiller)(address . julien@lepiller.eu)(address . 52164-done@debbugs.gnu.org)

Message-ID:864k26iyju.fsf@gmail.com

Hi Julien,

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

Toggle quote (2 lines)

> 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

Closed

Your comment

This issue is archived.

To comment on this conversation send an email to 52164@debbugs.gnu.org

To respond to this issue using the mumi CLI, first switch to it

mumi current 52164

Then, you may apply the latest patchset in this issue (with sign off)

mumi am -- -s

Or, compose a reply to this issue

mumi compose

Or, send patches to this issue

mumi send-email *.patch

is:open	open issues
is:done	closed issues
submitter:<who>	search issue submitter
author:<who>	search by message author
date:yesterday..now	search by issue date
mdate:3m..2d	search by message date