[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[bug#34299] [PATCH] gnu: Add coq-autosubst
From: |
Julien Lepiller |
Subject: |
[bug#34299] [PATCH] gnu: Add coq-autosubst |
Date: |
Mon, 4 Feb 2019 22:19:56 +0100 |
Hi Dan, thanks for the patch! Some notes below:
Le Sun, 3 Feb 2019 16:24:26 +0100,
Dan Frumin <address@hidden> 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!