GNU bug report logs - #72730
[PATCH 0/2] coq: Update to 8.18.0.

Previous Next

Package: guix-patches;

Reported by: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>

Date: Tue, 20 Aug 2024 10:30:02 UTC

Severity: normal

Tags: patch

Done: Z572 <zhengjunjie <at> iscas.ac.cn>

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 72730 in the body.
You can then email your comments to 72730 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 julien <at> lepiller.eu, pukkamustard <at> posteo.net, guix-patches <at> gnu.org:
bug#72730; Package guix-patches. (Tue, 20 Aug 2024 10:30:02 GMT) Full text and rfc822 format available.
Acknowledgement sent to Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>:
New bug report received and forwarded. Copy sent to julien <at> lepiller.eu, pukkamustard <at> posteo.net, guix-patches <at> gnu.org. (Tue, 20 Aug 2024 10:30:02 GMT) Full text and rfc822 format available.

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

From: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
To: guix-patches <at> gnu.org
Cc: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Subject: [PATCH 0/2] coq: Update to 8.18.0.
Date: Tue, 20 Aug 2024 12:28:55 +0200

This updates Coq to 8.18.0 and some Coq plugins to build on the newer
version.  Updated to this one as 8.17 is already showing its age, Coq
8.19 still breaks Why 3, so that's the reason for 8.18, Why 3 already
has some fixes for 8.19 so when released we can update to 8.19 (or 8.20
that is soon to be released).

Jean-Pierre De Jesus DIAZ (2):
  gnu: coq: Propagate ocaml-zarith.
  gnu: coq: Update to 8.18.0.

 gnu/packages/coq.scm | 29 ++++++++++++++---------------
 1 file changed, 14 insertions(+), 15 deletions(-)


base-commit: 91b69f154db218834de002dcd013a8f47170e684
-- 
2.45.2
Information forwarded to julien <at> lepiller.eu, pukkamustard <at> posteo.net, guix-patches <at> gnu.org:
bug#72730; Package guix-patches. (Tue, 20 Aug 2024 10:34:01 GMT) Full text and rfc822 format available.

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

From: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
To: 72730 <at> debbugs.gnu.org
Cc: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Subject: [PATCH 1/2] gnu: coq: Propagate ocaml-zarith.
Date: Tue, 20 Aug 2024 12:31:18 +0200

Otherwise each Coq plugin needs to specify it.

* gnu/packages/coq.scm (coq) <inputs>: Move ocaml-zarith from here...
<propagated-inptus>: ... to here.
(coq-gappa) <inputs>: Remove ocaml-zarith.
(coq-bignums) <inputs>: Likewise.
(coq-interval) <inputs>: Likewise.
(coq-equations) <inputs>: Likewise.

Change-Id: I63cab11032cc6d4673efc9fdcf14be2929bda05e
---
 gnu/packages/coq.scm | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 4857426613..be95d16991 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -91,8 +91,10 @@ (define-public coq
                      (libdir (string-append out "/lib/ocaml/site-lib")))
                 (invoke "dune" "install" "--prefix" out
                         "--libdir" libdir "coq" "coq-core" "coq-stdlib")))))))
+    (propagated-inputs
+     (list ocaml-zarith))
     (inputs
-     (list gmp ocaml-zarith))
+     (list gmp))
     (native-inputs
      (list ocaml-ounit2 which))
     (properties '((upstream-name . "coq"))) ; also for inherited packages
@@ -114,7 +116,7 @@ (define-public coq-ide-server
      `(#:tests? #f
        #:package "coqide-server"))
     (inputs
-     (list coq gmp ocaml-zarith))))
+     (list coq gmp))))
 
 (define-public coq-ide
   (package
@@ -319,7 +321,7 @@ (define-public coq-gappa
            bison
            flex))
     (inputs
-     (list gmp mpfr ocaml-zarith boost))
+     (list gmp mpfr boost))
     (propagated-inputs
      (list coq-flocq))
     (arguments
@@ -457,7 +459,7 @@ (define-public coq-bignums
     (native-inputs
      (list ocaml coq))
     (inputs
-     (list camlp5 ocaml-zarith))
+     (list camlp5))
     (arguments
      `(#:tests? #f ; No test target.
        #:make-flags
@@ -495,8 +497,7 @@ (define-public coq-interval
      `(("flocq" ,coq-flocq)
        ("bignums" ,coq-bignums)
        ("coquelicot" ,coq-coquelicot)
-       ("mathcomp" ,coq-mathcomp)
-       ("ocaml-zarith" ,ocaml-zarith)))
+       ("mathcomp" ,coq-mathcomp)))
     (arguments
      `(#:configure-flags
        (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out")
@@ -579,8 +580,6 @@ (define-public coq-equations
     (build-system gnu-build-system)
     (native-inputs
      (list ocaml coq camlp5))
-    (inputs
-     (list ocaml-zarith))
     (arguments
      `(#:test-target "test-suite"
        #:make-flags (list (string-append "COQLIBINSTALL="
-- 
2.45.2
Information forwarded to julien <at> lepiller.eu, pukkamustard <at> posteo.net, guix-patches <at> gnu.org:
bug#72730; Package guix-patches. (Tue, 20 Aug 2024 10:34:02 GMT) Full text and rfc822 format available.

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

From: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
To: 72730 <at> debbugs.gnu.org
Cc: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Subject: [PATCH 2/2] gnu: coq: Update to 8.18.0.
Date: Tue, 20 Aug 2024 12:31:19 +0200

* gnu/packages/coq.scm (coq): Update to 8.18.0.
(coq-bignums): Update to 9.0.0+coq8.18.
(coq-equations): Update to 1.3-8.18.

Change-Id: I644a4538538a23d736fca2fab541c2cd2fb1f472
---
 gnu/packages/coq.scm | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index be95d16991..02d2600546 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -56,7 +56,7 @@ (define-module (gnu packages coq)
 (define-public coq
   (package
     (name "coq")
-    (version "8.17.1")
+    (version "8.18.0")
     (source
      (origin
        (method git-fetch)
@@ -66,7 +66,7 @@ (define-public coq
        (file-name (git-file-name name version))
        (sha256
         (base32
-         "0gg6hizq0i08lk741b579cbswhy6qvkh6inc3d3i5a2af98psq63"))))
+         "1qy71gdr4s2l6847b4nwns6akib2f7l725zb01m7zc26n6mrrh1m"))))
     (native-search-paths
      (list (search-path-specification
             (variable "COQPATH")
@@ -445,16 +445,16 @@ (define-public coq-coquelicot
 (define-public coq-bignums
   (package
     (name "coq-bignums")
-    (version "8.16.0")
+    (version "9.0.0+coq8.18")
     (source (origin
               (method git-fetch)
               (uri (git-reference
                      (url "https://github.com/coq/bignums")
-                     (commit (string-append "V" version))))
+                     (commit (string-append "v" version))))
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "07ndnm7pndmai3a2bkcmwjfjzfaqyq19c5an15hmhgmd0rdy4z8c"))))
+                "1vw1a498fhyrpm884rlm3r4lw4mg4l6b9xj8w4y875sacg88kdxw"))))
     (build-system gnu-build-system)
     (native-inputs
      (list ocaml coq))
@@ -567,7 +567,7 @@ (define-public coq-autosubst
 (define-public coq-equations
   (package
     (name "coq-equations")
-    (version "1.3-8.17")
+    (version "1.3-8.18")
     (source (origin
               (method git-fetch)
               (uri (git-reference
@@ -576,7 +576,7 @@ (define-public coq-equations
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "0g68h4c1ijpphixvl9wkd7sibds38v4236dpvvh194j5ii42vnn8"))))
+                "1akxf2vafwyz6fi1djlc3g8mwxrjv0a99x4b08jwrbwxypv4xiph"))))
     (build-system gnu-build-system)
     (native-inputs
      (list ocaml coq camlp5))
-- 
2.45.2
Reply sent to Z572 <zhengjunjie <at> iscas.ac.cn>:
You have taken responsibility. (Thu, 12 Sep 2024 06:33:01 GMT) Full text and rfc822 format available.
Notification sent to Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>:
bug acknowledged by developer. (Thu, 12 Sep 2024 06:33:01 GMT) Full text and rfc822 format available.

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

From: Z572 <zhengjunjie <at> iscas.ac.cn>
To: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Cc: 72730-done <at> debbugs.gnu.org, pukkamustard <pukkamustard <at> posteo.net>,
 Julien Lepiller <julien <at> lepiller.eu>
Subject: Re: [bug#72730] [PATCH 2/2] gnu: coq: Update to 8.18.0.
Date: Thu, 12 Sep 2024 14:32:29 +0800

[Message part 1 (text/plain, inline)]
Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz> writes:

> * gnu/packages/coq.scm (coq): Update to 8.18.0.
> (coq-bignums): Update to 9.0.0+coq8.18.
> (coq-equations): Update to 1.3-8.18.

i split to 3 patch. and make coq-bignums coq-equations use g-expression.

>
> Change-Id: I644a4538538a23d736fca2fab541c2cd2fb1f472
> ---
>  gnu/packages/coq.scm | 14 +++++++-------
>  1 file changed, 7 insertions(+), 7 deletions(-)
>
> diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
> index be95d16991..02d2600546 100644
> --- a/gnu/packages/coq.scm
> +++ b/gnu/packages/coq.scm
> @@ -56,7 +56,7 @@ (define-module (gnu packages coq)
>  (define-public coq
>    (package
>      (name "coq")
> -    (version "8.17.1")
> +    (version "8.18.0")
>      (source
>       (origin
>         (method git-fetch)
> @@ -66,7 +66,7 @@ (define-public coq
>         (file-name (git-file-name name version))
>         (sha256
>          (base32
> -         "0gg6hizq0i08lk741b579cbswhy6qvkh6inc3d3i5a2af98psq63"))))
> +         "1qy71gdr4s2l6847b4nwns6akib2f7l725zb01m7zc26n6mrrh1m"))))
>      (native-search-paths
>       (list (search-path-specification
>              (variable "COQPATH")
> @@ -445,16 +445,16 @@ (define-public coq-coquelicot
>  (define-public coq-bignums
>    (package
>      (name "coq-bignums")
> -    (version "8.16.0")
> +    (version "9.0.0+coq8.18")
>      (source (origin
>                (method git-fetch)
>                (uri (git-reference
>                       (url "https://github.com/coq/bignums")
> -                     (commit (string-append "V" version))))
> +                     (commit (string-append "v" version))))
>                (file-name (git-file-name name version))
>                (sha256
>                 (base32
> -                "07ndnm7pndmai3a2bkcmwjfjzfaqyq19c5an15hmhgmd0rdy4z8c"))))
> +                "1vw1a498fhyrpm884rlm3r4lw4mg4l6b9xj8w4y875sacg88kdxw"))))
>      (build-system gnu-build-system)
>      (native-inputs
>       (list ocaml coq))
> @@ -567,7 +567,7 @@ (define-public coq-autosubst
>  (define-public coq-equations
>    (package
>      (name "coq-equations")
> -    (version "1.3-8.17")
> +    (version "1.3-8.18")
>      (source (origin
>                (method git-fetch)
>                (uri (git-reference
> @@ -576,7 +576,7 @@ (define-public coq-equations
>                (file-name (git-file-name name version))
>                (sha256
>                 (base32
> -                "0g68h4c1ijpphixvl9wkd7sibds38v4236dpvvh194j5ii42vnn8"))))
> +                "1akxf2vafwyz6fi1djlc3g8mwxrjv0a99x4b08jwrbwxypv4xiph"))))
>      (build-system gnu-build-system)
>      (native-inputs
>       (list ocaml coq camlp5))

push, close.

[signature.asc (application/pgp-signature, inline)]
Information forwarded to guix-patches <at> gnu.org:
bug#72730; Package guix-patches. (Thu, 12 Sep 2024 06:35:02 GMT) Full text and rfc822 format available.

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

From: Z572 <zhengjunjie <at> iscas.ac.cn>
To: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Cc: 72730 <at> debbugs.gnu.org, pukkamustard <pukkamustard <at> posteo.net>,
 Julien Lepiller <julien <at> lepiller.eu>
Subject: Re: [bug#72730] [PATCH 1/2] gnu: coq: Propagate ocaml-zarith.
Date: Thu, 12 Sep 2024 14:34:09 +0800

[Message part 1 (text/plain, inline)]
Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz> writes:

> Otherwise each Coq plugin needs to specify it.
>
> * gnu/packages/coq.scm (coq) <inputs>: Move ocaml-zarith from here...
> <propagated-inptus>: ... to here.
> (coq-gappa) <inputs>: Remove ocaml-zarith.
> (coq-bignums) <inputs>: Likewise.
> (coq-interval) <inputs>: Likewise.
> (coq-equations) <inputs>: Likewise.

adjust to

* gnu/packages/coq.scm (coq)[inputs]: Move ocaml-zarith from here...
[propagated-inptus]: ... to here.
(coq-gappa)[inputs]: Remove ocaml-zarith.
(coq-bignums)[inputs]: Likewise.
(coq-interval)[inputs]: Likewise.
(coq-equations)[inputs]: Likewise.

>
> Change-Id: I63cab11032cc6d4673efc9fdcf14be2929bda05e
> ---
>  gnu/packages/coq.scm | 15 +++++++--------
>  1 file changed, 7 insertions(+), 8 deletions(-)
>
> diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
> index 4857426613..be95d16991 100644
> --- a/gnu/packages/coq.scm
> +++ b/gnu/packages/coq.scm
> @@ -91,8 +91,10 @@ (define-public coq
>                       (libdir (string-append out "/lib/ocaml/site-lib")))
>                  (invoke "dune" "install" "--prefix" out
>                          "--libdir" libdir "coq" "coq-core" "coq-stdlib")))))))
> +    (propagated-inputs
> +     (list ocaml-zarith))
>      (inputs
> -     (list gmp ocaml-zarith))
> +     (list gmp))
>      (native-inputs
>       (list ocaml-ounit2 which))
>      (properties '((upstream-name . "coq"))) ; also for inherited packages
> @@ -114,7 +116,7 @@ (define-public coq-ide-server
>       `(#:tests? #f
>         #:package "coqide-server"))
>      (inputs
> -     (list coq gmp ocaml-zarith))))
> +     (list coq gmp))))
>  
>  (define-public coq-ide
>    (package
> @@ -319,7 +321,7 @@ (define-public coq-gappa
>             bison
>             flex))
>      (inputs
> -     (list gmp mpfr ocaml-zarith boost))
> +     (list gmp mpfr boost))
>      (propagated-inputs
>       (list coq-flocq))
>      (arguments
> @@ -457,7 +459,7 @@ (define-public coq-bignums
>      (native-inputs
>       (list ocaml coq))
>      (inputs
> -     (list camlp5 ocaml-zarith))
> +     (list camlp5))
>      (arguments
>       `(#:tests? #f ; No test target.
>         #:make-flags
> @@ -495,8 +497,7 @@ (define-public coq-interval
>       `(("flocq" ,coq-flocq)
>         ("bignums" ,coq-bignums)
>         ("coquelicot" ,coq-coquelicot)
> -       ("mathcomp" ,coq-mathcomp)
> -       ("ocaml-zarith" ,ocaml-zarith)))
> +       ("mathcomp" ,coq-mathcomp)))
>      (arguments
>       `(#:configure-flags
>         (list (string-append "COQUSERCONTRIB=" (assoc-ref %outputs "out")
> @@ -579,8 +580,6 @@ (define-public coq-equations
>      (build-system gnu-build-system)
>      (native-inputs
>       (list ocaml coq camlp5))
> -    (inputs
> -     (list ocaml-zarith))
>      (arguments
>       `(#:test-target "test-suite"
>         #:make-flags (list (string-append "COQLIBINSTALL="

[signature.asc (application/pgp-signature, inline)]
bug archived. Request was from Debbugs Internal Request <help-debbugs <at> gnu.org> to internal_control <at> debbugs.gnu.org. (Thu, 10 Oct 2024 11:24:07 GMT) Full text and rfc822 format available.
This bug report was last modified 250 days ago.

Previous Next

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