--- Begin Message ---
|
Subject: |
[PATCH] gnu: Add coq-autosubst |
|
Date: |
Sun, 3 Feb 2019 16:24:26 +0100 |
---
gnu/packages/coq.scm | 45 ++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 45 insertions(+)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 51dd5dedc..ba1bfd93b 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -444,3 +444,48 @@ provides BigN, BigZ, BigQ that used to be part of Coq
standard library.")
simplifying the proofs of inequalities on expressions of real numbers for the
Coq proof assistant.")
(license license:cecill-c)))
+
+(define-public coq-autosubst
+ (let ((branch "coq86-devel")
+ (commit "d0d73557979796b3d4be7aac72135581c33f26f7"))
+ (package
+ (name "coq-autosubst")
+ (synopsis "A Coq library for parallel de Bruijn substitutions")
+ (version (git-version "1" branch commit))
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "git://github.com/uds-psl/autosubst.git")
+ ;; (branch branch)
+ (commit commit)))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32
"1852xb5cwkjw3dlc0lp2sakwa40bjzw37qmwz4bn3vqazg1hnh6r"))))
+ (build-system gnu-build-system)
+ (native-inputs
+ `(("coq" ,coq)))
+ (arguments
+ `(#:tests? #f
+ #:phases
+ (modify-phases %standard-phases
+ (delete 'configure)
+ (replace 'install
+ (lambda* (#:key outputs #:allow-other-keys)
+ (setenv "COQLIB" (string-append (assoc-ref outputs "out")
"/lib/coq/"))
+ (zero? (system* "make"
+ (string-append "COQLIB=" (assoc-ref outputs
"out")
+ "/lib/coq/")
+ "install")))))))
+ (description "Formalizing syntactic theories with variable binders is
+not easy. We present Autosubst, 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
+synthesizes the parallel substitution operation and automatically proves the
+basic lemmas about substitutions. Our core contribution is an automation
+tactic that solves equations involving terms and substitutions. This makes the
+usage of substitution lemmas unnecessary. The tactic is based on our current
+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.")
+ (home-page "https://www.ps.uni-saarland.de/autosubst/";)
+ (license bsd-3))))
--
2.17.1
--- End Message ---
--- Begin Message ---
|
Subject: |
Re: [bug#34299] [PATCH] gnu: Add coq-autosubst |
|
Date: |
Thu, 7 Feb 2019 22:35:38 +0100 |
pushed with some changes as 7d60df330aa165982abd31c8483651788fdf49b9:
I've added a copyright line for you at the top of the file.
I've added (guix git-download) to the list of imported modules.
I've replace bsd-3 with license:bsd-3.
I've modified the synopsis so it doesn't start with "A".
I've modified the description so it doesn't say "we".
I've moved some fields around so they look more like other packages.
Thank you again for the patch!
--- End Message ---