| Message ID | 20190203152426.5750-1-dfrumin@cs.ru.nl |
|---|---|
| State | Accepted |
| Headers | show |
| Series | [bug#34299] gnu: Add coq-autosubst | expand |
| Context | Check | Description |
|---|---|---|
| cbaines/applying patch | success | Successfully applied |
Hi Dan, thanks for the patch! Some notes below: Le Sun, 3 Feb 2019 16:24:26 +0100, Dan Frumin <dfrumin@cs.ru.nl> a écrit : > --- > 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")) So, why this commit and this branch in particular? It seems that there are some releases on github, and we tend to prefer using a released version of packages. > + (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) Please remove these comments :) > + (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"))))))) We now use (invoke ...) instead of (zero? (system* ...)). > + (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)))) Thank you!
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!
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))))