[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[bug#34299] [PATCH] gnu: Add coq-autosubst
From: |
Dan Frumin |
Subject: |
[bug#34299] [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
- [bug#34299] [PATCH] gnu: Add coq-autosubst,
Dan Frumin <=