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

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

[Dan Frumin]

---
 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

[Julien Lepiller]

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!

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

[Dan Frumin]

[-- Attachment #1: Type: text/plain, Size: 640 bytes --]

Hi Julien!


 > 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.

This is the latest commit in the branch that compiles with the latest version of Coq.
Unfortunately the files on the "releases" page are outdated.


 > Please remove these comments :)

 > We now use (invoke ...) instead of (zero? (system* ...)).


Thanks, I've updated it!

By the way, I did not subscribe to the guix-pactches.
Is there a way to receive email on this particular issue from the bug tracker, without subscribing to the mailing list in full?


[-- Attachment #2: 0001-gnu-Add-coq-autosubst.patch --]
[-- Type: text/x-patch, Size: 2855 bytes --]

From 924a078455d6c73022da22523e018e33af3ee334 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Sun, 3 Feb 2019 16:14:12 +0100
Subject: [PATCH] gnu: Add coq-autosubst

---
 gnu/packages/coq.scm | 44 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 51dd5dedc..9c6d9f238 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -444,3 +444,47 @@ 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")
+                      (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/"))
+               (invoke "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

[Julien Lepiller]

Le 2019-02-07 14:46, Dan Frumin a écrit :
> Hi Julien!
> 
> 
>> 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.
> 
> This is the latest commit in the branch that compiles with the latest
> version of Coq.
> Unfortunately the files on the "releases" page are outdated.
> 
> 
>> Please remove these comments :)
> 
>> We now use (invoke ...) instead of (zero? (system* ...)).
> 
> 
> Thanks, I've updated it!

Thanks! I'll take a look at your package definition and push later 
today.

> 
> By the way, I did not subscribe to the guix-pactches.
> Is there a way to receive email on this particular issue from the bug
> tracker, without subscribing to the mailing list in full?

I don't think there is, unfortunately. I usually reply to the sender as
well as to the bug tracker though. Did I forget it in my previous reply?

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

[Julien Lepiller]

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!