[PATCH 0/6] coq: Update various packages.

  • Done
  • quality assurance status badge
Details
3 participants
  • Andreas Enge
  • Arnaud Daby-Seesaram
  • Jean-Pierre De Jesus DIAZ
Owner
unassigned
Submitted by
Jean-Pierre De Jesus DIAZ
Severity
normal
J
J
Jean-Pierre De Jesus DIAZ wrote on 11 Jun 17:10 +0200
(address . guix-patches@gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
cover.1718118200.git.jean@foundation.xyz
This patch series update various Coq packages to newer versions as they
don't compile with Coq 8.19, so this is essentially a pre-requisite
patch set to update Coq.

There are other packages that will need to be updated at the same time
as Coq as they don't build with the current version (coq-bignums and
coq-equations).

I have a branch prepared to update Coq to 8.19:


But it isn't ready yet because it breaks why3 and all of it dependents,

And also the coq-semantics package fails to build with Coq 8.19, but it
seems that it hasn't been maintained lately.

So to not break those packages first I think it's best to at least merge
these updates in the meantime to make progress towards updating Coq.

Jean-Pierre De Jesus DIAZ (6):
gnu: coq-autosubst: Update to 1.8-0.6ba0acc.
gnu: coq-coquelicot: Update to 3.4.1.
gnu: coq-gappa: Update to 1.5.5.
gnu: coq-interval: Update to 4.10.0.
gnu: coq-mathcomp: Update to 1.19.0.
gnu: coq-stdpp: Update to 1.10.0.

gnu/packages/coq.scm | 76 +++++++++++++++++++++++---------------------
1 file changed, 40 insertions(+), 36 deletions(-)


base-commit: 520d85bad4c0207df85273c72d59e9e7d7416538
--
2.45.1
J
J
Jean-Pierre De Jesus DIAZ wrote on 12 Jun 10:57 +0200
[PATCH 1/6] gnu: coq-autosubst: Update to 1.8-0.6ba0acc.
(address . 71492@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
4c09da5d4c9caff71566b129dc60d59023c06b32.1718118200.git.jean@foundation.xyz
* gnu/packages/coq.scm (coq-autosubst): Update to 1.8-0.6ba0acc.

Change-Id: Ib705c92b5605c6b679224f471ff12c018842c006
---
gnu/packages/coq.scm | 56 ++++++++++++++++++++++++--------------------
1 file changed, 30 insertions(+), 26 deletions(-)

Toggle diff (76 lines)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 11d6b034f1..81f99bd368 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -518,31 +518,35 @@ (define-public coq-interval
(license license:cecill-c)))
(define-public coq-autosubst
- (package
- (name "coq-autosubst")
- (version "1.8")
- (source (origin
- (method git-fetch)
- (uri (git-reference
- (url "https://github.com/coq-community/autosubst")
- (commit (string-append "v" version))))
- (file-name (git-file-name name version))
- (sha256
- (base32 "0qk72r6cqxwhqqkl2kmryhw365w3l2016qii1q1sk3md7zq46jcz"))))
- (build-system gnu-build-system)
- (arguments
- `(#:tests? #f
- #:make-flags (list (string-append "COQLIBINSTALL="
- (assoc-ref %outputs "out")
- "/lib/coq/user-contrib"))
- #:phases
- (modify-phases %standard-phases
- (delete 'configure))))
- (native-inputs
- (list coq))
- (home-page "https://www.ps.uni-saarland.de/autosubst/")
- (synopsis "Coq library for parallel de Bruijn substitutions")
- (description "Formalizing syntactic theories with variable binders is
+ ;; Latest tag does not build with Coq >=8.19, recent commits contain a fix
+ ;; of the problem.
+ (let ((revision "0")
+ (commit "6ba0acccef68c75f6cca8928706c726754d69791"))
+ (package
+ (name "coq-autosubst")
+ (version (git-version "1.8" revision commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/coq-community/autosubst")
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "0k62ygj3zqcs17nhyalcxgwbs8as3f9kdxx6b6a0d44j0iqqnw0l"))))
+ (build-system gnu-build-system)
+ (arguments
+ `(#:tests? #f
+ #:make-flags (list (string-append "COQLIBINSTALL="
+ (assoc-ref %outputs "out")
+ "/lib/coq/user-contrib"))
+ #:phases
+ (modify-phases %standard-phases
+ (delete 'configure))))
+ (native-inputs
+ (list coq))
+ (home-page "https://www.ps.uni-saarland.de/autosubst/")
+ (synopsis "Coq library for parallel de Bruijn substitutions")
+ (description "Formalizing syntactic theories with variable binders is
not easy. Autosubst is a library for the Coq proof assistant to
automate this process. Given an inductive definition of syntactic objects in
de Bruijn representation augmented with binding annotations, Autosubst
@@ -553,7 +557,7 @@ (define-public coq-autosubst
work on a decision procedure for the equational theory of an extension of the
sigma-calculus by Abadi et al. The library is completely written in Coq and
uses Ltac to synthesize the substitution operation.")
- (license license:bsd-3)))
+ (license license:bsd-3))))
(define-public coq-equations
(package
--
2.45.1
J
J
Jean-Pierre De Jesus DIAZ wrote on 12 Jun 10:57 +0200
[PATCH 2/6] gnu: coq-coquelicot: Update to 3.4.1.
(address . 71492@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
f3b7d6d39cbd92ba5e747a1c0dfe46c479d5dc61.1718118200.git.jean@foundation.xyz
* gnu/packages/coq.scm (coq-coquelicot): Update to 3.4.1.

Change-Id: I9330c7d98b881c051f4f03dfdf7f1be9e3f26aa6
---
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 81f99bd368..4b2efb017f 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -388,7 +388,7 @@ (define-public coq-mathcomp
(define-public coq-coquelicot
(package
(name "coq-coquelicot")
- (version "3.4.0")
+ (version "3.4.1")
(source
(origin
(method git-fetch)
@@ -398,7 +398,7 @@ (define-public coq-coquelicot
(file-name (git-file-name name version))
(sha256
(base32
- "1f6zim6hnm6zrij964vas6rfbxh5p147qsxxmmbxm7gyb85hhy45"))))
+ "1y22dqdklh3c8rbhar0d7mzaj84q6zyfik7namx5q4ma76s2rx73"))))
(build-system gnu-build-system)
(native-inputs
(list autoconf automake ocaml which coq))
--
2.45.1
J
J
Jean-Pierre De Jesus DIAZ wrote on 12 Jun 10:57 +0200
[PATCH 3/6] gnu: coq-gappa: Update to 1.5.5.
(address . 71492@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
21519d1b5c85ff8ea3eec86b4e59cda794b53408.1718118200.git.jean@foundation.xyz
* gnu/packages/coq.scm (coq-gappa): Update to 1.5.5.

Change-Id: Iaf0077a8081d7ba30aeb1bded3bc36570df88283
---
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 4b2efb017f..97e797e2de 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -291,7 +291,7 @@ (define-public coq-for-coqtail
(define-public coq-gappa
(package
(name "coq-gappa")
- (version "1.5.3")
+ (version "1.5.5")
(source
(origin
(method git-fetch)
@@ -301,7 +301,7 @@ (define-public coq-gappa
(file-name (git-file-name name version))
(sha256
(base32
- "1dzkb2sfglhik2ymw8p65khl163xxjsaqji9agnnkvlk5r6589v6"))))
+ "0w780wk10khzfx6d633dyzx9q0hvqgimqbzc3irjzvsbpvb0zm5c"))))
(build-system gnu-build-system)
(native-inputs
(list autoconf
--
2.45.1
J
J
Jean-Pierre De Jesus DIAZ wrote on 12 Jun 10:57 +0200
[PATCH 4/6] gnu: coq-interval: Update to 4.10.0.
(address . 71492@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
04948e867e3b0d26fc443e2302ad2344d5e4b28c.1718118200.git.jean@foundation.xyz
* gnu/packages/coq.scm (coq-interval): Update to 4.10.0.

Change-Id: If5be16804fefdca04b52a91cf3f52484c486fea8
---
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 97e797e2de..30c5a09665 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -471,7 +471,7 @@ (define-public coq-bignums
(define-public coq-interval
(package
(name "coq-interval")
- (version "4.8.0")
+ (version "4.10.0")
(source
(origin
(method git-fetch)
@@ -481,7 +481,7 @@ (define-public coq-interval
(file-name (git-file-name name version))
(sha256
(base32
- "0m3icx77p99ld9qfl3xjq62q572pyi4m77i1kc3whvipvg7834rh"))))
+ "039c29hc8mzp2is6zh9fps36k03hlvx6zz08h03vj6dhjgr7njz8"))))
(build-system gnu-build-system)
(native-inputs
(list autoconf automake ocaml which coq))
--
2.45.1
J
J
Jean-Pierre De Jesus DIAZ wrote on 12 Jun 10:57 +0200
[PATCH 5/6] gnu: coq-mathcomp: Update to 1.19.0.
(address . 71492@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
a14ec966f0ecaf48d4a6d4814cb66b0a62df99bd.1718118200.git.jean@foundation.xyz
* gnu/packages/coq.scm (coq-mathcomp): Update to 1.19.0.

Change-Id: Icf72f91c09aa0504d7175d437a1cf75020751335
---
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 30c5a09665..18fc116bd6 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -351,7 +351,7 @@ (define-public coq-gappa
(define-public coq-mathcomp
(package
(name "coq-mathcomp")
- (version "1.17.0")
+ (version "1.19.0")
(source
(origin
(method git-fetch)
@@ -360,7 +360,7 @@ (define-public coq-mathcomp
(commit (string-append "mathcomp-" version))))
(file-name (git-file-name name version))
(sha256
- (base32 "06i6kw5p2024n6h9mf8bvwn54il1a4z2h4qrgc8y0iq8hkvx4fnd"))))
+ (base32 "0dij9zl2ag083dzgrv2j16ks2kkn2xxwnk1wr5956zw1y7ynrzb3"))))
(build-system gnu-build-system)
(native-inputs
(list ocaml which coq))
--
2.45.1
J
J
Jean-Pierre De Jesus DIAZ wrote on 12 Jun 10:57 +0200
[PATCH 6/6] gnu: coq-stdpp: Update to 1.10.0.
(address . 71492@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
3a85975c3b193cbcbba65109fa0bae6538e54379.1718118200.git.jean@foundation.xyz
* gnu/packages/coq.scm (coq-stdpp): Update to 1.10.0.

Change-Id: Icea37b785c03196baa88a92ced3ac9dc25079546
---
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 18fc116bd6..0fa0753826 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -649,7 +649,7 @@ (define-public coq-semantics
(define-public coq-stdpp
(package
(name "coq-stdpp")
- (version "1.8.0")
+ (version "1.10.0")
(synopsis "Alternative Coq standard library std++")
(source (origin
(method git-fetch)
@@ -659,7 +659,7 @@ (define-public coq-stdpp
(file-name (git-file-name name version))
(sha256
(base32
- "0xawh3xkh76yhs689zw52k55cbzga2gyzl4g1a3pgg6yy420chjn"))))
+ "0lnvdfn4qq2lyabiq4ikb5ya46f4jp59dynyprnhki0ay9xagz3d"))))
(build-system gnu-build-system)
(inputs
(list coq))
--
2.45.1
A
A
Arnaud Daby-Seesaram wrote on 12 Jun 21:17 +0200
Re: [bug#71492] [PATCH 0/6] coq: Update various packages.
(address . 71492@debbugs.gnu.org)
87le3aezs0.fsf@nanein.fr
user guix
usertag 71492 + reviewed-looks-good
thanks

Guix QA review form submission:


Items marked as checked: Package builds, Commit messages
-----BEGIN PGP SIGNATURE-----

iQJEBAEBCgAuFiEEMgqfJ4U0fby1t860ojLKXoMTiAwFAmZp9GAQHGRzLWFjQG5h
bmVpbi5mcgAKCRCiMspegxOIDIw6D/9SHz5NtFf5Cu9kKIZj9VKHScGL5t/ZwfC9
euyZOYMmIfWUAQH4Jmt3hkgCHP89rIxomJTvYmrjQuizkQym6bekeng9CbSd/kYg
mmCGPWbpTcLQTQArj0scd0lW/tK41cvcQHdbd8YQWlg51imlG6OgJXnWJul0pppH
beuQJpgQQhadGJGKV9DblNvtgRue2jkrmzi9RHbpal7RnmDd/QVSoFmzqM0S4qCv
HVumCyqslfl01Eto0TIFRY+NEZCLjGoUsOKrc9vV64LDEXaQ0brzkQ8w1HDGwPlP
VPS6cmjrF/F7vsdz6PWn4hZtKMH40GuMveBQ7nidvZT0yGJm2KtO82B6Aa/9lTrJ
fVBmuLKMZgHdqLp/01UwvhzSwq+bRZC84r7vuR88iZtdvMK5wa4ptzWylWwi8xGF
vk8ntJ0kUtHV542+yibzPkD2HKyVWjQNmn+Efv9v4wVJYQOhQhNcThlw++MSHLCn
yCQI0r7mNQ9xIENWIxHlEb1xPkG/4NyD6OhEeSx0WZ21bS+JTC09F7B0diI8riXe
AY9b3zvA3h9fJL/FWB0jGDWp3xA1Nnf3gMU5C/pplWL6NVmU9iCsGZ1+pmU+0b2p
+xcGxFyUGXbaw4O2yGZX4HJ1v8RauU2d3/I+uTQxJZOeDw9/DkpT/GmOdVXBv7qW
vYDj5Q8zbQ==
=93ax
-----END PGP SIGNATURE-----

A
A
Andreas Enge wrote on 14 Jun 20:17 +0200
New release?
(address . 71492@debbugs.gnu.org)
ZmyJRkwXEDMbJkqs@jurong
Hello,

thanks for the patches and the review!

So far I have pushed all patches but coq-autosubst, since I feel a bit
uneasy about non-released versions. Even more so since this is not the
only required change for Coq 8.19. In general we prefer to only add the fix
with a patch; this can often be the relevant commit from git.

Or maybe you could ask for a new release on their communication channels?

Andreas
J
J
Jean-Pierre De Jesus DIAZ wrote on 17 Jun 14:25 +0200
[PATCH v2] gnu: coq-autosubst: Fix Coq 8.19 compatibility.
(address . 71492@debbugs.gnu.org)(name . Jean-Pierre De Jesus DIAZ)(address . jean@foundation.xyz)
241e20259f230e3e7d080fe209830957af0a5f8e.1718627005.git.jean@foundation.xyz
* gnu/packages/patches/coq-autosubst-1.8-remove-deprecated-files.patch: New patch.
* gnu/local.mk (dist_patch_DATA): Register patch.
* gnu/packages/coq.scm (coq-autosubst)<source>: Use Coq 8.19
compatibility patch.

Change-Id: Ib705c92b5605c6b679224f471ff12c018842c006
---
gnu/local.mk | 1 +
gnu/packages/coq.scm | 4 +-
...utosubst-1.8-remove-deprecated-files.patch | 43 +++++++++++++++++++
3 files changed, 47 insertions(+), 1 deletion(-)
create mode 100644 gnu/packages/patches/coq-autosubst-1.8-remove-deprecated-files.patch

Toggle diff (80 lines)
diff --git a/gnu/local.mk b/gnu/local.mk
index 83b7402b09..f591317610 100644
--- a/gnu/local.mk
+++ b/gnu/local.mk
@@ -1081,6 +1081,7 @@ dist_patch_DATA = \
%D%/packages/patches/converseen-hide-updates-checks.patch \
%D%/packages/patches/converseen-hide-non-free-pointers.patch \
%D%/packages/patches/cool-retro-term-wctype.patch \
+ %D%/packages/patches/coq-autosubst-1.8-remove-deprecated-files.patch \
%D%/packages/patches/coreutils-gnulib-tests.patch \
%D%/packages/patches/cppcheck-disable-char-signedness-test.patch \
%D%/packages/patches/cppdap-add-CPPDAP_USE_EXTERNAL_GTEST_PACKAGE.patch\
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index f0c09bdef9..7a8a49208a 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -528,7 +528,9 @@ (define-public coq-autosubst
(commit (string-append "v" version))))
(file-name (git-file-name name version))
(sha256
- (base32 "0qk72r6cqxwhqqkl2kmryhw365w3l2016qii1q1sk3md7zq46jcz"))))
+ (base32 "0qk72r6cqxwhqqkl2kmryhw365w3l2016qii1q1sk3md7zq46jcz"))
+ (patches
+ (search-patches "coq-autosubst-1.8-remove-deprecated-files.patch"))))
(build-system gnu-build-system)
(arguments
`(#:tests? #f
diff --git a/gnu/packages/patches/coq-autosubst-1.8-remove-deprecated-files.patch b/gnu/packages/patches/coq-autosubst-1.8-remove-deprecated-files.patch
new file mode 100644
index 0000000000..cc76672798
--- /dev/null
+++ b/gnu/packages/patches/coq-autosubst-1.8-remove-deprecated-files.patch
@@ -0,0 +1,43 @@
+This patch compatibility problems with Coq 8.19.
+
+It was taken from the master branch of coq-autosubst as there is only
+this change since version 1.8 of autosubst and they haven't released a
+newer version yet.
+
+To recreate this patch:
+
+wget https://github.com/coq-community/autosubst/commit/97eea491813b691c6187d53d92ae6020874a82a3.patch \
+ -O coq-autosubst-1.8-remove-deprecated-files.patch
+
+From 97eea491813b691c6187d53d92ae6020874a82a3 Mon Sep 17 00:00:00 2001
+From: Pierre Rousselin <rousselin@math.univ-paris13.fr>
+Date: Sun, 15 Oct 2023 14:34:31 +0200
+Subject: [PATCH] Remove deprecated files in Coq.Arith
+
+This is necessary for Coq/Coq:#18164
+---
+ theories/Autosubst_Basics.v | 4 ++--
+ 1 file changed, 2 insertions(+), 2 deletions(-)
+
+diff --git a/theories/Autosubst_Basics.v b/theories/Autosubst_Basics.v
+index 477c87c..1940c3b 100644
+--- a/theories/Autosubst_Basics.v
++++ b/theories/Autosubst_Basics.v
+@@ -5,7 +5,7 @@
+ *)
+
+ Require Import Coq.Program.Tactics.
+-Require Import Coq.Arith.Plus List FunctionalExtensionality.
++Require Import Coq.Arith.PeanoNat List FunctionalExtensionality.
+
+ (** Annotate "a" with additional information. *)
+ Definition annot {A B} (a : A) (b : B) : A := a.
+@@ -240,7 +240,7 @@ Lemma plusSn n m : S n + m = S (n + m). reflexivity. Qed.
+ Lemma plusnS n m : n + S m = S (n + m). symmetry. apply plus_n_Sm. Qed.
+ Lemma plusOn n : O + n = n. reflexivity. Qed.
+ Lemma plusnO n : n + O = n. symmetry. apply plus_n_O. Qed.
+-Lemma plusA n m k : n + (m + k) = (n + m) + k. apply plus_assoc. Qed.
++Lemma plusA n m k : n + (m + k) = (n + m) + k. apply Nat.add_assoc. Qed.
+
+ Lemma scons_eta f n : f n .: (+S n) >>> f = (+n) >>> f.
+ Proof.

base-commit: f9ed5788fda9288301550c641820d422e9ad1602
--
2.45.1
J
J
Jean-Pierre De Jesus Diaz wrote on 17 Jun 14:30 +0200
Re: New release?
(address . 71492@debbugs.gnu.org)(address . andreas@enge.fr)
CAG1gdUp_OWw-BwcwBNT6D0Zgz3cuN8R1S38LFK5bNg+hOy4amg@mail.gmail.com
Hello,

Toggle quote (5 lines)
>So far I have pushed all patches but coq-autosubst, since I feel a bit
>uneasy about non-released versions. Even more so since this is not the
>only required change for Coq 8.19. In general we prefer to only add the fix
>with a patch; this can often be the relevant commit from git.

Thanks for merging the patches, I've sent a new one to this issue to change
the coq-autosubst package to use a patch instead of an unreleased version
since that's the only commit that has happened since v1.8 and it is quite
small.

I'll ask if they can release a new version in the meantime so that we can
remove the patch in the future.

Cheers,

Jean-Pierre
A
A
Andreas Enge wrote on 23 Jun 11:50 +0200
(name . Jean-Pierre De Jesus Diaz)(address . jean@foundation.xyz)(address . 71492-done@debbugs.gnu.org)
Znfv37dy6l9UmfBt@jurong
Hello,

Am Mon, Jun 17, 2024 at 12:30:26PM +0000 schrieb Jean-Pierre De Jesus Diaz:
Toggle quote (7 lines)
> Thanks for merging the patches, I've sent a new one to this issue to change
> the coq-autosubst package to use a patch instead of an unreleased version
> since that's the only commit that has happened since v1.8 and it is quite
> small.
> I'll ask if they can release a new version in the meantime so that we can
> remove the patch in the future.

thanks, excellent, I have pushed this commit.

I am closing this bug now and let you open a new one once more Coq related
patches are ready.

Andreas
Closed
?
Your comment

Commenting via the web interface is currently disabled.

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

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