diff mbox series

[bug#34299] gnu: Add coq-autosubst

Message ID 0d4af4f2-2ebc-6134-acc2-9d6727ef49e0@cs.ru.nl
State Accepted
Headers show
Series [bug#34299] gnu: Add coq-autosubst | expand

Checks

Context Check Description
cbaines/applying patch fail Apply failed

Commit Message

Dan Frumin Feb. 7, 2019, 1:46 p.m. UTC 
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?

Comments

Julien Lepiller Feb. 7, 2019, 1:53 p.m. UTC | #1 
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?
diff mbox series

Patch

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