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

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

[Jean-Pierre De Jesus DIAZ]

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

[bug#71492] [PATCH 1/6] gnu: coq-autosubst: Update to 1.8-0.6ba0acc.

[Jean-Pierre De Jesus DIAZ]

* 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

[bug#71492] [PATCH 2/6] gnu: coq-coquelicot: Update to 3.4.1.

[Jean-Pierre De Jesus DIAZ]

* 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

[bug#71492] [PATCH 3/6] gnu: coq-gappa: Update to 1.5.5.

[Jean-Pierre De Jesus DIAZ]

* 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

[bug#71492] [PATCH 4/6] gnu: coq-interval: Update to 4.10.0.

[Jean-Pierre De Jesus DIAZ]

* 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

[bug#71492] [PATCH 5/6] gnu: coq-mathcomp: Update to 1.19.0.

[Jean-Pierre De Jesus DIAZ]

* 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

[bug#71492] [PATCH 6/6] gnu: coq-stdpp: Update to 1.10.0.

[Jean-Pierre De Jesus DIAZ]

* 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

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

[Arnaud Daby-Seesaram via Guix-patches via]

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

user guix
usertag 71492 + reviewed-looks-good
thanks

Guix QA review form submission:


Items marked as checked: Package builds, Commit messages

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

[bug#71492] New release?

[Andreas Enge]

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

[bug#71492] [PATCH v2] gnu: coq-autosubst: Fix Coq 8.19 compatibility.

[Jean-Pierre De Jesus DIAZ]

* 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@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

[bug#71492] New release?

[Jean-Pierre De Jesus Diaz]

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

bug#71492: New release?

[Andreas Enge]

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