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

  • Done
  • quality assurance status badge
Details
2 participants
  • Jean-Pierre De Jesus DIAZ
  • Z572
Owner
unassigned
Submitted by
Jean-Pierre De Jesus DIAZ
Severity
normal
J
J
Jean-Pierre De Jesus DIAZ wrote on 20 Aug 12:28 +0200
(address . guix-patches@gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
cover.1724149236.git.jean@foundation.xyz
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 20 Aug 12:31 +0200
[PATCH 1/2] gnu: coq: Propagate ocaml-zarith.
(address . 72730@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
f2a362489c4b8664e63b0e6aeb939d4c3c090249.1724149236.git.jean@foundation.xyz
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(-)

Toggle diff (64 lines)
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
J
J
Jean-Pierre De Jesus DIAZ wrote on 20 Aug 12:31 +0200
[PATCH 2/2] gnu: coq: Update to 8.18.0.
(address . 72730@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
be3cbaa29169188defaac67a8cb2c8e1b86e6b39.1724149236.git.jean@foundation.xyz
* 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(-)

Toggle diff (62 lines)
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
Z
Z
Z572 wrote on 12 Sep 08:32 +0200
(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
87wmjhcrgi.fsf@iscas.ac.cn
Jean-Pierre De Jesus DIAZ <jean@foundation.xyz> writes:

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

Toggle quote (67 lines)
>
> 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.
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEfr6klGDOXiwIdX/bO1qpk+Gi3/AFAmbiiv0ACgkQO1qpk+Gi
3/BcYg/+MY2X+Zvr2zADULU8osxx4SlwV2UuFJ4Nb2gjpMRHR00C0wtLn2bPt6pO
iuyiucpd7diGWqyWTUph/ql8CXgkq0sCCDat0soBCzcSeFEtS6ANuDRamK2ruty1
/uBN674dbd64symRLnS04HYaKJlhmPjCVfGh/baPi5P6GDYe1HqLEMzmMJcMZeiW
dZ5wZPW6h+GgXhm01q10VEQ0zvohCqfYlMliE0UC7eQ0wtzgvorL49dKv3pm/4P0
KFTP7rHpZ6+LVPAzPnBPK6cgYjbKy9bqcVNenlmZWlJio8Jgwqkcu2mxbsFPSttY
iSiPpfeXOpJzb1rHPsZKvOKDBJg2pdsFrto5u7CYe0DuuKt77HeMl/r6/m1YDZfc
TtgAqVFoXIi3D6UZHRJx9vxfKdE2LMunckdKCa1kLJejfywhoRYkm3yQGwBriPyD
dOT5xEKTfQ0hSR9P0XFzoPu5URGnrY23NAlK9F0IWB73aYF4AwMFgBFQTFQvoGC9
Y7aGJoCBsCecYiAbxS8gGPORGGScUBgmx28lYnTcNLj5EKelZdDRkpFvpMpsIEbU
+lE956/jYky6BHmO+uskwXKOdRohdQSvhd53Vwz0KczmKmkn35pYDYjwOZcF/+9L
l6ZGoEoJdlHgy11x1kYP79uSK02L6QkxqyqFp4KwLZvpSPUI4u0=
=8pXE
-----END PGP SIGNATURE-----

Closed
Z
Z
Z572 wrote on 12 Sep 08:34 +0200
Re: [bug#72730] [PATCH 1/2] gnu: coq: Propagate ocaml-zarith.
(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
87seu5crdq.fsf@iscas.ac.cn
Jean-Pierre De Jesus DIAZ <jean@foundation.xyz> writes:

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

Toggle quote (68 lines)
>
> 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="
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEfr6klGDOXiwIdX/bO1qpk+Gi3/AFAmbii2EACgkQO1qpk+Gi
3/Cw9RAArET/mMF/CK2ewH3CpBLnwjH+2UmlWs07k8oQElL/EzbvojwHPTQGMMuS
Nr3GiZ+1KCRG/Q6xrWyXiGSvBvAILdGdYj7PbDkUZMJT2wWkG7S31i9IedwZ3did
krLIzo4JSauOZ4fiG2yq6HxVrllJG//RuH8NAS33hFI2aSs1fLcaM/eosboraND/
dROf/2Sjr8FzDHqbFJsT6GirWhLIEggfOOAYCu0vGLWJ2jQaRcBNm2s5rZo5unUr
zjR2hkSIcC1mrhUcW6YBXWn7im7yPhSfAxh4COZhPycG4ss22MBIj0f5TeX+Oht3
BwWW94aQkwszQqnqb2S5a2+JMVIpuME+8f59xBchv/+vGRD4PTZ1/OhIlSNotB2H
AC+gIkn9sofSilNh64Sj08rulyv3Z/7POUZgjMbhjIFqFRX4PrUEi99bYpIrbdUJ
yHWA+uqk9JlwA9+8YGWfJB4IISQ/g9xYesWG9hxPC9QmJWiGTPYIzXeFs2BplIAx
kcTU7mYH1R0hZeuu1QKvXVWkw3JcAuatsqPUYrSEGbZVOv3xgNw8/fk9BxdR+MHG
I6NklryhWzS9N3v2G1X244wuB/DDQ3UqneC+xE02IW1I0qopRYj10CWlxeJ7l88v
pEFyDi+knbRhyIFryWBG3CzGXA7PztYYgWqfZuukjFbVIwj0Fhw=
=iJq0
-----END PGP SIGNATURE-----

?
Your comment

This issue is archived.

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

To respond to this issue using the mumi CLI, first switch to it
mumi current 72730
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