GNU bug report logs - #71492
[PATCH 0/6] coq: Update various packages.

Previous Next

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

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

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/6] coq: Update various packages.
Date: Tue, 11 Jun 2024 17:10:02 +0200

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:

<https://github.com/Foundation-Devices/guix-mirror/tree/coq/update-8.19>

But it isn't ready yet because it breaks why3 and all of it dependents,
see: <https://gitlab.inria.fr/why3/why3/-/merge_requests/1077>.

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

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

From: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
To: 71492 <at> debbugs.gnu.org
Cc: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Subject: [PATCH 1/6] gnu: coq-autosubst: Update to 1.8-0.6ba0acc.
Date: Wed, 12 Jun 2024 10:57:08 +0200

* 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(-)

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

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

From: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
To: 71492 <at> debbugs.gnu.org
Cc: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Subject: [PATCH 2/6] gnu: coq-coquelicot: Update to 3.4.1.
Date: Wed, 12 Jun 2024 10:57:09 +0200

* 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(-)

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

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

From: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
To: 71492 <at> debbugs.gnu.org
Cc: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Subject: [PATCH 3/6] gnu: coq-gappa: Update to 1.5.5.
Date: Wed, 12 Jun 2024 10:57:10 +0200

* 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(-)

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

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

From: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
To: 71492 <at> debbugs.gnu.org
Cc: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Subject: [PATCH 4/6] gnu: coq-interval: Update to 4.10.0.
Date: Wed, 12 Jun 2024 10:57:11 +0200

* 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(-)

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

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

From: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
To: 71492 <at> debbugs.gnu.org
Cc: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Subject: [PATCH 5/6] gnu: coq-mathcomp: Update to 1.19.0.
Date: Wed, 12 Jun 2024 10:57:12 +0200

* 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(-)

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

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

From: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
To: 71492 <at> debbugs.gnu.org
Cc: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Subject: [PATCH 6/6] gnu: coq-stdpp: Update to 1.10.0.
Date: Wed, 12 Jun 2024 10:57:13 +0200

* 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(-)

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

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

From: Arnaud Daby-Seesaram <ds-ac <at> nanein.fr>
To: 71492 <at> debbugs.gnu.org
Subject: Re: [bug#71492] [PATCH 0/6] coq: Update various packages.
Date: Wed, 12 Jun 2024 21:17:51 +0200

[Message part 1 (text/plain, inline)]

user guix
usertag 71492 + reviewed-looks-good
thanks

Guix QA review form submission:


Items marked as checked: Package builds, Commit messages

[signature.asc (application/pgp-signature, inline)]

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

From: Andreas Enge <andreas <at> enge.fr>
To: 71492 <at> debbugs.gnu.org
Subject: New release?
Date: Fri, 14 Jun 2024 20:17:42 +0200

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

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

From: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
To: 71492 <at> debbugs.gnu.org
Cc: Jean-Pierre De Jesus DIAZ <jean <at> foundation.xyz>
Subject: [PATCH v2] gnu: coq-autosubst: Fix Coq 8.19 compatibility.
Date: Mon, 17 Jun 2024 14:25:35 +0200

* 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

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 <at> 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

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

From: Jean-Pierre De Jesus Diaz <jean <at> foundation.xyz>
To: 71492 <at> debbugs.gnu.org
Cc: andreas <at> enge.fr
Subject: Re: New release?
Date: Mon, 17 Jun 2024 12:30:26 +0000

Hello,

>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

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

From: Andreas Enge <andreas <at> enge.fr>
To: Jean-Pierre De Jesus Diaz <jean <at> foundation.xyz>
Cc: 71492-done <at> debbugs.gnu.org
Subject: Re: New release?
Date: Sun, 23 Jun 2024 11:50:23 +0200

Hello,

Am Mon, Jun 17, 2024 at 12:30:26PM +0000 schrieb Jean-Pierre De Jesus Diaz:
> 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

Previous Next

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