[bug#72730] [PATCH 0/2] coq: Update to 8.18.0.

[bug#72730] [PATCH 0/2] coq: Update to 8.18.0.

[Jean-Pierre De Jesus DIAZ]

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

[bug#72730] [PATCH 1/2] gnu: coq: Propagate ocaml-zarith.

[Jean-Pierre De Jesus DIAZ]

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

[bug#72730] [PATCH 2/2] gnu: coq: Update to 8.18.0.

[Jean-Pierre De Jesus DIAZ]

* 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

bug#72730: [PATCH 2/2] gnu: coq: Update to 8.18.0.

[Z572]

[-- Attachment #1: Type: text/plain, Size: 2699 bytes --]

Jean-Pierre De Jesus DIAZ <jean@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.

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 832 bytes --]

[bug#72730] [PATCH 1/2] gnu: coq: Propagate ocaml-zarith.

[Z572]

[-- Attachment #1: Type: text/plain, Size: 2989 bytes --]

Jean-Pierre De Jesus DIAZ <jean@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="

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 832 bytes --]