GNU bug report logs - #35855
[PATCH] gnu: Add coq-stdpp.

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 35855 in the body.
You can then email your comments to 35855 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-stdpp.
Date: Wed, 22 May 2019 13:33:23 +0200

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

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 4f592622f5..15a7e791f9 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -25,6 +25,7 @@
   #:use-module (gnu packages boost)
   #:use-module (gnu packages emacs)
   #:use-module (gnu packages flex)
+  #:use-module (gnu packages gawk)
   #:use-module (gnu packages multiprecision)
   #:use-module (gnu packages ocaml)
   #:use-module (gnu packages perl)
@@ -535,3 +536,64 @@ compiles everything down to eliminators for inductive types, equality
 and accessibility, providing a definitional extension to the Coq
 kernel.")
     (license license:lgpl2.1)))
+
+(define-public coq-stdpp
+  (package
+    (name "coq-stdpp")
+    (version "1.2.0")
+    (synopsis "Alternative Coq standard library std++")
+    (source (origin
+              (method git-fetch)
+              (uri (git-reference
+                    (url "https://gitlab.mpi-sws.org/iris/stdpp.git")
+                    (commit (string-append "coq-stdpp-" version))))
+              (file-name (git-file-name name version))
+              (sha256
+               (base32 "11m7kqxsbxygk41v2wsi3npdzwin9fcnzc1gn0gq0rd57wnqk83i"))))
+    (build-system gnu-build-system)
+    (native-inputs
+     `(("grep" ,grep)  ;; need egrep for tests
+       ("gawk" ,gawk)
+       ;; need diff for tests
+       ("diffutils" ,diffutils)))
+    (inputs
+     `(("coq" ,coq)))
+    (arguments
+     `(#:tests? #f ;; the tests are being run automaticlly as part of `make all`
+       #: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 "This project contains an extended \"Standard Library\" for
+Coq called coq-std++.  The key features are:
+@itemize
+@item Great number of definitions and lemmas for common data structures such
+as lists, finite maps, finite sets, and finite multisets.
+
+@item Type classes for common notations (like ∅, ∪, and Haskell-style monad
+notations) so that these can be overloaded for different data structures.
+
+@item It uses type classes to keep track of common properties of types, like
+it having decidable equality or being countable or finite.
+
+@item Most data structures are represented in canonical ways so that Leibniz
+equality can be used as much as possible (for example, for maps we have m1 =
+m2 iff ∀ i, m1 !! i = m2 !! i).  On top of that, the library provides setoid
+instances for most types and operations.
+
+@item Various tactics for common tasks, like an ssreflect inspired done tactic
+for finishing trivial goals, a simple breadth-first solver naive_solver, an
+equality simplifier simplify_eq, a solver solve_proper for proving
+compatibility of functions with respect to relations, and a solver set_solver
+for goals involving set operations.
+
+@item The library is dependency- and axiom-free.
+@end itemize")
+    (home-page "https://gitlab.mpi-sws.org/iris/stdpp")
+    (license license:bsd-3)))
-- 
2.17.1

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

From: Ludovic Courtès <ludo <at> gnu.org>
To: Dan Frumin <dfrumin <at> cs.ru.nl>
Cc: 35855-done <at> debbugs.gnu.org
Subject: Re: [bug#35855] [PATCH] gnu: Add coq-stdpp.
Date: Fri, 24 May 2019 18:23:29 +0200

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

Hi Dan,

I took the liberty to apply the minor changes below and applied the
patch (grep, diffutils, etc. are implicit inputs of ‘gnu-build-system’,
so you don’t need to list them; as for ‘invoke’, it’s now the preferred
way to invoke programs.)

Thank you!

Ludo’.

[Message part 2 (text/x-patch, inline)]

diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index 15a7e791f9..6c48af4fc9 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -551,11 +551,6 @@ kernel.")
               (sha256
                (base32 "11m7kqxsbxygk41v2wsi3npdzwin9fcnzc1gn0gq0rd57wnqk83i"))))
     (build-system gnu-build-system)
-    (native-inputs
-     `(("grep" ,grep)  ;; need egrep for tests
-       ("gawk" ,gawk)
-       ;; need diff for tests
-       ("diffutils" ,diffutils)))
     (inputs
      `(("coq" ,coq)))
     (arguments
@@ -566,10 +561,10 @@ kernel.")
          (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")))))))
+             (invoke "make"
+                     (string-append "COQLIB=" (assoc-ref outputs "out")
+                                    "/lib/coq/")
+                     "install"))))))
     (description "This project contains an extended \"Standard Library\" for
 Coq called coq-std++.  The key features are:
 @itemize

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

From: Dan Frumin <dfrumin <at> cs.ru.nl>
To: Ludovic Courtès <ludo <at> gnu.org>
Cc: 35855-done <at> debbugs.gnu.org
Subject: Re: [bug#35855] [PATCH] gnu: Add coq-stdpp.
Date: Fri, 24 May 2019 19:11:07 +0200

Hi Ludovic,

Thanks for looking over my patch!

On 24-05-19 18:23, Ludovic Courtès wrote:
> Hi Dan,
> 
> I took the liberty to apply the minor changes below and applied the
> patch (grep, diffutils, etc. are implicit inputs of ‘gnu-build-system’,
> so you don’t need to list them;

Oh interesting. I recall that I had to add those programs explicitly as inputs as some point (otherwise I couldn't build it in `guix environment 
coq-stdpp`), but perhaps my memory is playing tricks on me.

> as for ‘invoke’, it’s now the preferred
> way to invoke programs.)
>

Oops, dunno why I missed that...


> Thank you!
> 
> Ludo’.
> 
> 
> diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
> index 15a7e791f9..6c48af4fc9 100644
> --- a/gnu/packages/coq.scm
> +++ b/gnu/packages/coq.scm
> @@ -551,11 +551,6 @@ kernel.")
>                 (sha256
>                  (base32 "11m7kqxsbxygk41v2wsi3npdzwin9fcnzc1gn0gq0rd57wnqk83i"))))
>       (build-system gnu-build-system)
> -    (native-inputs
> -     `(("grep" ,grep)  ;; need egrep for tests
> -       ("gawk" ,gawk)
> -       ;; need diff for tests
> -       ("diffutils" ,diffutils)))
>       (inputs
>        `(("coq" ,coq)))
>       (arguments
> @@ -566,10 +561,10 @@ kernel.")
>            (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")))))))
> +             (invoke "make"
> +                     (string-append "COQLIB=" (assoc-ref outputs "out")
> +                                    "/lib/coq/")
> +                     "install"))))))
>       (description "This project contains an extended \"Standard Library\" for
>   Coq called coq-std++.  The key features are:
>   @itemize
> 

Previous Next

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