* [bug#71492] [PATCH 0/6] coq: Update various packages.
@ 2024-06-11 15:10 Jean-Pierre De Jesus DIAZ
2024-06-12 8:57 ` [bug#71492] [PATCH 1/6] gnu: coq-autosubst: Update to 1.8-0.6ba0acc Jean-Pierre De Jesus DIAZ
` (9 more replies)
0 siblings, 10 replies; 12+ messages in thread
From: Jean-Pierre De Jesus DIAZ @ 2024-06-11 15:10 UTC (permalink / raw)
To: 71492; +Cc: Jean-Pierre De Jesus DIAZ, Julien Lepiller, pukkamustard
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
^ permalink raw reply [flat|nested] 12+ messages in thread
* [bug#71492] [PATCH 1/6] gnu: coq-autosubst: Update to 1.8-0.6ba0acc.
2024-06-11 15:10 [bug#71492] [PATCH 0/6] coq: Update various packages Jean-Pierre De Jesus DIAZ
@ 2024-06-12 8:57 ` Jean-Pierre De Jesus DIAZ
2024-06-12 8:57 ` [bug#71492] [PATCH 2/6] gnu: coq-coquelicot: Update to 3.4.1 Jean-Pierre De Jesus DIAZ
` (8 subsequent siblings)
9 siblings, 0 replies; 12+ messages in thread
From: Jean-Pierre De Jesus DIAZ @ 2024-06-12 8:57 UTC (permalink / raw)
To: 71492; +Cc: Jean-Pierre De Jesus DIAZ, Julien Lepiller, pukkamustard
* 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
^ permalink raw reply related [flat|nested] 12+ messages in thread
* [bug#71492] [PATCH 2/6] gnu: coq-coquelicot: Update to 3.4.1.
2024-06-11 15:10 [bug#71492] [PATCH 0/6] coq: Update various packages Jean-Pierre De Jesus DIAZ
2024-06-12 8:57 ` [bug#71492] [PATCH 1/6] gnu: coq-autosubst: Update to 1.8-0.6ba0acc Jean-Pierre De Jesus DIAZ
@ 2024-06-12 8:57 ` Jean-Pierre De Jesus DIAZ
2024-06-12 8:57 ` [bug#71492] [PATCH 3/6] gnu: coq-gappa: Update to 1.5.5 Jean-Pierre De Jesus DIAZ
` (7 subsequent siblings)
9 siblings, 0 replies; 12+ messages in thread
From: Jean-Pierre De Jesus DIAZ @ 2024-06-12 8:57 UTC (permalink / raw)
To: 71492; +Cc: Jean-Pierre De Jesus DIAZ, Julien Lepiller, pukkamustard
* 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
^ permalink raw reply related [flat|nested] 12+ messages in thread
* [bug#71492] [PATCH 3/6] gnu: coq-gappa: Update to 1.5.5.
2024-06-11 15:10 [bug#71492] [PATCH 0/6] coq: Update various packages Jean-Pierre De Jesus DIAZ
2024-06-12 8:57 ` [bug#71492] [PATCH 1/6] gnu: coq-autosubst: Update to 1.8-0.6ba0acc Jean-Pierre De Jesus DIAZ
2024-06-12 8:57 ` [bug#71492] [PATCH 2/6] gnu: coq-coquelicot: Update to 3.4.1 Jean-Pierre De Jesus DIAZ
@ 2024-06-12 8:57 ` Jean-Pierre De Jesus DIAZ
2024-06-12 8:57 ` [bug#71492] [PATCH 4/6] gnu: coq-interval: Update to 4.10.0 Jean-Pierre De Jesus DIAZ
` (6 subsequent siblings)
9 siblings, 0 replies; 12+ messages in thread
From: Jean-Pierre De Jesus DIAZ @ 2024-06-12 8:57 UTC (permalink / raw)
To: 71492; +Cc: Jean-Pierre De Jesus DIAZ, Julien Lepiller, pukkamustard
* 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
^ permalink raw reply related [flat|nested] 12+ messages in thread
* [bug#71492] [PATCH 4/6] gnu: coq-interval: Update to 4.10.0.
2024-06-11 15:10 [bug#71492] [PATCH 0/6] coq: Update various packages Jean-Pierre De Jesus DIAZ
` (2 preceding siblings ...)
2024-06-12 8:57 ` [bug#71492] [PATCH 3/6] gnu: coq-gappa: Update to 1.5.5 Jean-Pierre De Jesus DIAZ
@ 2024-06-12 8:57 ` Jean-Pierre De Jesus DIAZ
2024-06-12 8:57 ` [bug#71492] [PATCH 5/6] gnu: coq-mathcomp: Update to 1.19.0 Jean-Pierre De Jesus DIAZ
` (5 subsequent siblings)
9 siblings, 0 replies; 12+ messages in thread
From: Jean-Pierre De Jesus DIAZ @ 2024-06-12 8:57 UTC (permalink / raw)
To: 71492; +Cc: Jean-Pierre De Jesus DIAZ, Julien Lepiller, pukkamustard
* 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
^ permalink raw reply related [flat|nested] 12+ messages in thread
* [bug#71492] [PATCH 5/6] gnu: coq-mathcomp: Update to 1.19.0.
2024-06-11 15:10 [bug#71492] [PATCH 0/6] coq: Update various packages Jean-Pierre De Jesus DIAZ
` (3 preceding siblings ...)
2024-06-12 8:57 ` [bug#71492] [PATCH 4/6] gnu: coq-interval: Update to 4.10.0 Jean-Pierre De Jesus DIAZ
@ 2024-06-12 8:57 ` Jean-Pierre De Jesus DIAZ
2024-06-12 8:57 ` [bug#71492] [PATCH 6/6] gnu: coq-stdpp: Update to 1.10.0 Jean-Pierre De Jesus DIAZ
` (4 subsequent siblings)
9 siblings, 0 replies; 12+ messages in thread
From: Jean-Pierre De Jesus DIAZ @ 2024-06-12 8:57 UTC (permalink / raw)
To: 71492; +Cc: Jean-Pierre De Jesus DIAZ, Julien Lepiller, pukkamustard
* 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
^ permalink raw reply related [flat|nested] 12+ messages in thread
* [bug#71492] [PATCH 6/6] gnu: coq-stdpp: Update to 1.10.0.
2024-06-11 15:10 [bug#71492] [PATCH 0/6] coq: Update various packages Jean-Pierre De Jesus DIAZ
` (4 preceding siblings ...)
2024-06-12 8:57 ` [bug#71492] [PATCH 5/6] gnu: coq-mathcomp: Update to 1.19.0 Jean-Pierre De Jesus DIAZ
@ 2024-06-12 8:57 ` Jean-Pierre De Jesus DIAZ
2024-06-12 19:17 ` [bug#71492] [PATCH 0/6] coq: Update various packages Arnaud Daby-Seesaram via Guix-patches via
` (3 subsequent siblings)
9 siblings, 0 replies; 12+ messages in thread
From: Jean-Pierre De Jesus DIAZ @ 2024-06-12 8:57 UTC (permalink / raw)
To: 71492; +Cc: Jean-Pierre De Jesus DIAZ, Julien Lepiller, pukkamustard
* 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
^ permalink raw reply related [flat|nested] 12+ messages in thread
* [bug#71492] [PATCH 0/6] coq: Update various packages.
2024-06-11 15:10 [bug#71492] [PATCH 0/6] coq: Update various packages Jean-Pierre De Jesus DIAZ
` (5 preceding siblings ...)
2024-06-12 8:57 ` [bug#71492] [PATCH 6/6] gnu: coq-stdpp: Update to 1.10.0 Jean-Pierre De Jesus DIAZ
@ 2024-06-12 19:17 ` Arnaud Daby-Seesaram via Guix-patches via
2024-06-14 18:17 ` [bug#71492] New release? Andreas Enge
` (2 subsequent siblings)
9 siblings, 0 replies; 12+ messages in thread
From: Arnaud Daby-Seesaram via Guix-patches via @ 2024-06-12 19:17 UTC (permalink / raw)
To: 71492
[-- 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 --]
^ permalink raw reply [flat|nested] 12+ messages in thread
* [bug#71492] New release?
2024-06-11 15:10 [bug#71492] [PATCH 0/6] coq: Update various packages Jean-Pierre De Jesus DIAZ
` (6 preceding siblings ...)
2024-06-12 19:17 ` [bug#71492] [PATCH 0/6] coq: Update various packages Arnaud Daby-Seesaram via Guix-patches via
@ 2024-06-14 18:17 ` Andreas Enge
2024-06-17 12:25 ` [bug#71492] [PATCH v2] gnu: coq-autosubst: Fix Coq 8.19 compatibility Jean-Pierre De Jesus DIAZ
2024-06-17 12:30 ` [bug#71492] New release? Jean-Pierre De Jesus Diaz
9 siblings, 0 replies; 12+ messages in thread
From: Andreas Enge @ 2024-06-14 18:17 UTC (permalink / raw)
To: 71492
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
^ permalink raw reply [flat|nested] 12+ messages in thread
* [bug#71492] [PATCH v2] gnu: coq-autosubst: Fix Coq 8.19 compatibility.
2024-06-11 15:10 [bug#71492] [PATCH 0/6] coq: Update various packages Jean-Pierre De Jesus DIAZ
` (7 preceding siblings ...)
2024-06-14 18:17 ` [bug#71492] New release? Andreas Enge
@ 2024-06-17 12:25 ` Jean-Pierre De Jesus DIAZ
2024-06-17 12:30 ` [bug#71492] New release? Jean-Pierre De Jesus Diaz
9 siblings, 0 replies; 12+ messages in thread
From: Jean-Pierre De Jesus DIAZ @ 2024-06-17 12:25 UTC (permalink / raw)
To: 71492; +Cc: Jean-Pierre De Jesus DIAZ, Julien Lepiller, pukkamustard
* 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
^ permalink raw reply related [flat|nested] 12+ messages in thread
* [bug#71492] New release?
2024-06-11 15:10 [bug#71492] [PATCH 0/6] coq: Update various packages Jean-Pierre De Jesus DIAZ
` (8 preceding siblings ...)
2024-06-17 12:25 ` [bug#71492] [PATCH v2] gnu: coq-autosubst: Fix Coq 8.19 compatibility Jean-Pierre De Jesus DIAZ
@ 2024-06-17 12:30 ` Jean-Pierre De Jesus Diaz
2024-06-23 9:50 ` bug#71492: " Andreas Enge
9 siblings, 1 reply; 12+ messages in thread
From: Jean-Pierre De Jesus Diaz @ 2024-06-17 12:30 UTC (permalink / raw)
To: 71492; +Cc: andreas
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
^ permalink raw reply [flat|nested] 12+ messages in thread
* bug#71492: New release?
2024-06-17 12:30 ` [bug#71492] New release? Jean-Pierre De Jesus Diaz
@ 2024-06-23 9:50 ` Andreas Enge
0 siblings, 0 replies; 12+ messages in thread
From: Andreas Enge @ 2024-06-23 9:50 UTC (permalink / raw)
To: Jean-Pierre De Jesus Diaz; +Cc: 71492-done
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
^ permalink raw reply [flat|nested] 12+ messages in thread
end of thread, other threads:[~2024-06-23 9:52 UTC | newest]
Thread overview: 12+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2024-06-11 15:10 [bug#71492] [PATCH 0/6] coq: Update various packages Jean-Pierre De Jesus DIAZ
2024-06-12 8:57 ` [bug#71492] [PATCH 1/6] gnu: coq-autosubst: Update to 1.8-0.6ba0acc Jean-Pierre De Jesus DIAZ
2024-06-12 8:57 ` [bug#71492] [PATCH 2/6] gnu: coq-coquelicot: Update to 3.4.1 Jean-Pierre De Jesus DIAZ
2024-06-12 8:57 ` [bug#71492] [PATCH 3/6] gnu: coq-gappa: Update to 1.5.5 Jean-Pierre De Jesus DIAZ
2024-06-12 8:57 ` [bug#71492] [PATCH 4/6] gnu: coq-interval: Update to 4.10.0 Jean-Pierre De Jesus DIAZ
2024-06-12 8:57 ` [bug#71492] [PATCH 5/6] gnu: coq-mathcomp: Update to 1.19.0 Jean-Pierre De Jesus DIAZ
2024-06-12 8:57 ` [bug#71492] [PATCH 6/6] gnu: coq-stdpp: Update to 1.10.0 Jean-Pierre De Jesus DIAZ
2024-06-12 19:17 ` [bug#71492] [PATCH 0/6] coq: Update various packages Arnaud Daby-Seesaram via Guix-patches via
2024-06-14 18:17 ` [bug#71492] New release? Andreas Enge
2024-06-17 12:25 ` [bug#71492] [PATCH v2] gnu: coq-autosubst: Fix Coq 8.19 compatibility Jean-Pierre De Jesus DIAZ
2024-06-17 12:30 ` [bug#71492] New release? Jean-Pierre De Jesus Diaz
2024-06-23 9:50 ` bug#71492: " Andreas Enge
Code repositories for project(s) associated with this external index
https://git.savannah.gnu.org/cgit/guix.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.