diff options
| author | Jean-Pierre De Jesus DIAZ <jean@foundation.xyz> | 2024-06-17 14:25:35 +0200 |
|---|---|---|
| committer | Andreas Enge <andreas@enge.fr> | 2024-06-23 11:48:40 +0200 |
| commit | bf1e063be350c611022c1430f3a7f1f42005de7f (patch) | |
| tree | 00a36fc94466a71e8cf7adcef6db6d3b81d86ba9 /gnu/packages | |
| parent | 11c403ec0554be0e1c888ec6f8147a232e09adbd (diff) | |
| download | guix-bf1e063be350c611022c1430f3a7f1f42005de7f.tar guix-bf1e063be350c611022c1430f3a7f1f42005de7f.tar.gz | |
gnu: coq-autosubst: Fix Coq 8.19 compatibility.
* 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
Signed-off-by: Andreas Enge <andreas@enge.fr>
Diffstat (limited to 'gnu/packages')
| -rw-r--r-- | gnu/packages/coq.scm | 4 | ||||
| -rw-r--r-- | gnu/packages/patches/coq-autosubst-1.8-remove-deprecated-files.patch | 43 |
2 files changed, 46 insertions, 1 deletions
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 @@ Coq proof assistant.") (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. |