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

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 34299 in the body.
You can then email your comments to 34299 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Dan Frumin <dfrumin <at> cs.ru.nl>
To: guix-patches <at> gnu.org
Cc: Dan Frumin <dfrumin <at> cs.ru.nl>
Subject: [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

Message #8 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: guix-patches <at> gnu.org
Subject: Re: [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 <dfrumin <at> 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!

Message #11 received at 34299 <at> debbugs.gnu.org (full text, mbox):

From: Dan Frumin <dfrumin <at> cs.ru.nl>
To: 34299 <at> debbugs.gnu.org
Subject: Re: [bug#34299] [PATCH] gnu: Add coq-autosubst
Date: Thu, 7 Feb 2019 14:46:24 +0100

[Message part 1 (text/plain, inline)]

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?

[0001-gnu-Add-coq-autosubst.patch (text/x-patch, attachment)]

Message #14 received at 34299 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: Dan Frumin <dfrumin <at> cs.ru.nl>
Cc: 34299 <at> debbugs.gnu.org
Subject: Re: [bug#34299] [PATCH] gnu: Add coq-autosubst
Date: Thu, 07 Feb 2019 14:53:21 +0100

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?

Message #19 received at 34299-done <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: 34299-done <at> debbugs.gnu.org
Subject: Re: [bug#34299] [PATCH] gnu: Add coq-autosubst
Date: Thu, 7 Feb 2019 22:35:38 +0100

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!

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.