[bug#34299] [PATCH] gnu: Add coq-autosubst

[Julien Lepiller]

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!