GNU bug report logs - #52164
[PATCH] gnu: coq: Update to 8.14.0.

Previous Next

Package: guix-patches;

Reported by: Julien Lepiller <julien <at> lepiller.eu>

Date: Sun, 28 Nov 2021 16:45:02 UTC

Severity: normal

Tags: patch

Done: zimoun <zimon.toutoune <at> gmail.com>

Bug is archived. No further changes may be made.

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 52164 in the body.
You can then email your comments to 52164 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

View this report as an mbox folder, status mbox, maintainer mbox


Report forwarded to guix-patches <at> gnu.org:
bug#52164; Package guix-patches. (Sun, 28 Nov 2021 16:45:02 GMT) Full text and rfc822 format available.

Acknowledgement sent to Julien Lepiller <julien <at> lepiller.eu>:
New bug report received and forwarded. Copy sent to guix-patches <at> gnu.org. (Sun, 28 Nov 2021 16:45:02 GMT) Full text and rfc822 format available.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: guix-patches <at> gnu.org
Subject: [PATCH] gnu: coq: Update to 8.14.0.
Date: Sun, 28 Nov 2021 17:44:26 +0100
Hi Guix!

this small series updates coq to its latest version.




Information forwarded to guix-patches <at> gnu.org:
bug#52164; Package guix-patches. (Sun, 28 Nov 2021 17:28:02 GMT) Full text and rfc822 format available.

Message #8 received at 52164 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: 52164 <at> debbugs.gnu.org
Subject: [PATCH 1/3] gnu: ocaml-semantics: Update to 8.14.0.
Date: Sun, 28 Nov 2021 18:27:09 +0100
---
 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





Information forwarded to guix-patches <at> gnu.org:
bug#52164; Package guix-patches. (Sun, 28 Nov 2021 17:28:02 GMT) Full text and rfc822 format available.

Message #11 received at 52164 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: 52164 <at> debbugs.gnu.org
Subject: [PATCH 2/3] gnu: proof-general: Update to latest commit.
Date: Sun, 28 Nov 2021 18:27:10 +0100
* 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





Information forwarded to guix-patches <at> gnu.org:
bug#52164; Package guix-patches. (Sun, 28 Nov 2021 17:28:03 GMT) Full text and rfc822 format available.

Message #14 received at 52164 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: 52164 <at> debbugs.gnu.org
Subject: [PATCH 3/3] gnu: coq: Update to 8.14.0.
Date: Sun, 28 Nov 2021 18:27:11 +0100
* 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 <at> 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





Information forwarded to guix-patches <at> gnu.org:
bug#52164; Package guix-patches. (Mon, 29 Nov 2021 09:43:01 GMT) Full text and rfc822 format available.

Message #17 received at 52164 <at> debbugs.gnu.org (full text, mbox):

From: zimoun <zimon.toutoune <at> gmail.com>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 52164 <at> debbugs.gnu.org
Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0.
Date: Mon, 29 Nov 2021 10:06:09 +0100
On dim., 28 nov. 2021 at 18:27, Julien Lepiller <julien <at> 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




Information forwarded to guix-patches <at> gnu.org:
bug#52164; Package guix-patches. (Mon, 29 Nov 2021 09:44:02 GMT) Full text and rfc822 format available.

Message #20 received at 52164 <at> debbugs.gnu.org (full text, mbox):

From: zimoun <zimon.toutoune <at> gmail.com>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 52164 <at> debbugs.gnu.org
Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0.
Date: Mon, 29 Nov 2021 10:42:25 +0100
Hi,

On dim., 28 nov. 2021 at 18:27, Julien Lepiller <julien <at> 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 <at> 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




Information forwarded to guix-patches <at> gnu.org:
bug#52164; Package guix-patches. (Mon, 29 Nov 2021 09:44:02 GMT) Full text and rfc822 format available.

Message #23 received at 52164 <at> debbugs.gnu.org (full text, mbox):

From: zimoun <zimon.toutoune <at> gmail.com>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 52164 <at> debbugs.gnu.org
Subject: [PATCH 1/3] gnu: ocaml-semantics: Update to 8.14.0.
Date: Mon, 29 Nov 2021 10:05:39 +0100
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 <at> 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)




Information forwarded to guix-patches <at> gnu.org:
bug#52164; Package guix-patches. (Mon, 29 Nov 2021 12:31:02 GMT) Full text and rfc822 format available.

Message #26 received at 52164 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: zimoun <zimon.toutoune <at> gmail.com>
Cc: 52164 <at> debbugs.gnu.org
Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0.
Date: Mon, 29 Nov 2021 07:29:51 -0500

Le 29 novembre 2021 04:42:25 GMT-05:00, zimoun <zimon.toutoune <at> gmail.com> a écrit :
>Hi,
>
>On dim., 28 nov. 2021 at 18:27, Julien Lepiller <julien <at> 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 <at> 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




Information forwarded to guix-patches <at> gnu.org:
bug#52164; Package guix-patches. (Mon, 29 Nov 2021 13:22:01 GMT) Full text and rfc822 format available.

Message #29 received at 52164 <at> debbugs.gnu.org (full text, mbox):

From: zimoun <zimon.toutoune <at> gmail.com>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 52164 <at> debbugs.gnu.org
Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0.
Date: Mon, 29 Nov 2021 14:21:16 +0100
Hi Julien,

On Mon, 29 Nov 2021 at 13:30, Julien Lepiller <julien <at> 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 <at> 8.13.2.
Or do you mean that coq-binums <at> 8.13 is broken with coq <at> 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




Information forwarded to guix-patches <at> gnu.org:
bug#52164; Package guix-patches. (Mon, 29 Nov 2021 13:40:02 GMT) Full text and rfc822 format available.

Message #32 received at 52164 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: zimoun <zimon.toutoune <at> gmail.com>
Cc: 52164 <at> debbugs.gnu.org
Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0.
Date: Mon, 29 Nov 2021 08:39:23 -0500


>
>Hum, the breakage of coq-bignums or coq-equations is recent.  Because
>using 65234d0 from Nov. 2nd, they are substituable; using coq <at> 8.13.2.
>Or do you mean that coq-binums <at> 8.13 is broken with coq <at> 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




Information forwarded to guix-patches <at> gnu.org:
bug#52164; Package guix-patches. (Mon, 29 Nov 2021 14:15:01 GMT) Full text and rfc822 format available.

Message #35 received at 52164 <at> debbugs.gnu.org (full text, mbox):

From: zimoun <zimon.toutoune <at> gmail.com>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 52164 <at> debbugs.gnu.org
Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0.
Date: Mon, 29 Nov 2021 15:13:47 +0100
Re,

On Mon, 29 Nov 2021 at 14:39, Julien Lepiller <julien <at> 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




Reply sent to zimoun <zimon.toutoune <at> gmail.com>:
You have taken responsibility. (Tue, 03 May 2022 12:38:02 GMT) Full text and rfc822 format available.

Notification sent to Julien Lepiller <julien <at> lepiller.eu>:
bug acknowledged by developer. (Tue, 03 May 2022 12:38:02 GMT) Full text and rfc822 format available.

Message #40 received at 52164-done <at> debbugs.gnu.org (full text, mbox):

From: zimoun <zimon.toutoune <at> gmail.com>
To: Julien Lepiller <julien <at> lepiller.eu>
Cc: 52164-done <at> debbugs.gnu.org
Subject: Re: bug#52164: [PATCH] gnu: coq: Update to 8.14.0.
Date: Tue, 03 May 2022 14:35:33 +0200
Hi Julien,

On Sun, 28 Nov 2021 at 17:44, Julien Lepiller <julien <at> 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




bug archived. Request was from Debbugs Internal Request <help-debbugs <at> gnu.org> to internal_control <at> debbugs.gnu.org. (Wed, 01 Jun 2022 11:24:06 GMT) Full text and rfc822 format available.

This bug report was last modified 1 year and 301 days ago.

Previous Next


GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.