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 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. ption value='author'>author
path: root/gnu/packages.scm
AgeCommit message (Expand)Author
2024-12-12packages: Optimize ‘all-packages’....On my laptop, wall-clock time for (all-packages) goes from 27s to 1s. * gnu/packages.scm (all-packages): Use a hash table to remember visited packages instead of calling ‘delete-duplicates’ on the final list. Change-Id: I4aae804656b56ef2095993e91f0572a5891f41
2019-10-23cve: Rewrite to read the JSON feed instead of the XML feed....The XML feed was discontinued on Oct. 16th, 2019: <https://nvd.nist.gov/General/News/XML-Vulnerability-Feed-Retirement-Phase-3> * guix/cve.scm (string->date*): New procedure. (<cve-item>, <cve>, <cve-reference>): New record types. (cpe-match->cve-configuration, configuration-data->cve-configurations) (json->cve-items, version-matches?): New procedures. (yearly-feed-uri): Change URL to refer to JSON feed. (cpe->product-alist, %parse-vulnerability-feed) (xml->vulnerabilities): Remove. (cve-configuration->package-list, merge-package-lists) (cve-item->vulnerability, json->vulnerabilities): New procedures. (write-cache): Use 'json->vulnerabilities' instead of 'xml->vulnerabilities', and remove 'parameterize'. (vulnerabilities->lookup-proc): Use 'version-matches?' when VERSION is true. * tests/cve.scm (%sample): Use 'tests/cve-sample.json'. (%expected-vulnerabilities): Rewrite accordingly. ("json->cve-items", "cve-item-published-date") ("json->vulnerabilities"): New tests. ("xml->vulnerabilities"): Remove. ("vulnerabilities->lookup-proc"): Adjust to new vulnerabilities. * tests/cve-sample.json: New file. * tests/cve-sample.xml: Remove. * Makefile.am (EXTRA_DIST): Adjust accordingly. * doc/guix.texi (Invoking guix lint): Update nist.gov URLs. Ludovic Courtès