[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[bug#64249] [PATCH v9 06/34] gnu: Update coq-autosubst to 1.8.
From: |
Julien Lepiller |
Subject: |
[bug#64249] [PATCH v9 06/34] gnu: Update coq-autosubst to 1.8. |
Date: |
Wed, 10 Jan 2024 08:43:07 +0100 |
From: pukkamustard <pukkamustard@posteo.net>
* gnu/packages/coq.scm (coq-autosubst): Update to 1.8.
---
gnu/packages/coq.scm | 50 ++++++++++++++++++++------------------------
1 file changed, 23 insertions(+), 27 deletions(-)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 473ce014a6..bfd55306a4 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -542,35 +542,31 @@ (define-public coq-interval
(license license:cecill-c)))
(define-public coq-autosubst
- ;; Latest commit on that branch, where work on supporting coq 8.6 and
- ;; more recent versions of coq happen.
- (let ((branch "coq86-devel")
- (commit "fa6ef30664511ffa659cbcf3c962715cbee03572"))
- (package
- (name "coq-autosubst")
- (version (git-version "1" branch commit))
- (source (origin
- (method git-fetch)
- (uri (git-reference
- (url "git://github.com/uds-psl/autosubst")
- (commit commit)))
- (file-name (git-file-name name version))
- (sha256
- (base32
"1cl0bp96bk6lplbl7n5c703vd3gvbs5mvf2qrf8q333kkqd7jqq4"))))
- (build-system gnu-build-system)
- (arguments
- `(#:tests? #f
+ (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
+ #: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
@@ -581,7 +577,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.41.0
- [bug#64249] [PATCH v9 01/34] gnu: ocaml: Update to 4.14.1., Julien Lepiller, 2024/01/10
- [bug#64249] [PATCH v9 02/34] gnu: Update coq-flocq to 4.1.1., Julien Lepiller, 2024/01/10
- [bug#64249] [PATCH v9 03/34] gnu: Update coq-gappa to 1.5.3., Julien Lepiller, 2024/01/10
- [bug#64249] [PATCH v9 04/34] gnu: Update coq-coquelicot to 3.4.0., Julien Lepiller, 2024/01/10
- [bug#64249] [PATCH v9 05/34] gnu: Update coq-mathcomp to 1.17.0., Julien Lepiller, 2024/01/10
- [bug#64249] [PATCH v9 06/34] gnu: Update coq-autosubst to 1.8.,
Julien Lepiller <=
- [bug#64249] [PATCH v9 09/34] gnu: coq: Update to 8.17.1., Julien Lepiller, 2024/01/10
- [bug#64249] [PATCH v9 10/34] gnu: dune-bootstrap: Update to 3.11.0., Julien Lepiller, 2024/01/10
- [bug#64249] [PATCH v9 12/34] gnu: ocaml-alcotest: Update to 1.7.0., Julien Lepiller, 2024/01/10
- [bug#64249] [PATCH v9 07/34] gnu: Update coq-stdpp to 1.8.0., Julien Lepiller, 2024/01/10
- [bug#64249] [PATCH v9 11/34] gnu: opam: Split build into smaller sub-packages., Julien Lepiller, 2024/01/10
- [bug#64249] [PATCH v9 17/34] gnu: ocaml-ppx-bin-prot: Update to 0.16.0., Julien Lepiller, 2024/01/10
- [bug#64249] [PATCH v9 08/34] gnu: Update coq-interval to 4.8.0., Julien Lepiller, 2024/01/10
- [bug#64249] [PATCH v9 13/34] gnu: ocaml-sexplib: Update to 0.16.0., Julien Lepiller, 2024/01/10
- [bug#64249] [PATCH v9 15/34] gnu: Add ocaml-ppx-stable-witness., Julien Lepiller, 2024/01/10
- [bug#64249] [PATCH v9 20/34] gnu: Add ocaml-ppx-deriving-yojson., Julien Lepiller, 2024/01/10