From: Dan Frumin <dfrumin@cs.ru.nl>
To: 34466@debbugs.gnu.org
Subject: [bug#34466] Fwd: Re: [bug#34466] [PATCH] gnu: Add coq-equations.
Date: Wed, 13 Feb 2019 12:36:59 +0100 [thread overview]
Message-ID: <e463eb9d-009f-5d9e-831a-a3ae8eb6dbac@cs.ru.nl> (raw)
In-Reply-To: <7a093050-4495-7650-7b9b-2abf73a2efc7@cs.ru.nl>
[-- Attachment #1: Type: text/plain, Size: 5025 bytes --]
(sorry, sending this again because I forgot to CC the bugtracker)
Hi Julien.
Thank you for your thorough comments, I really appreciate it!
I hope that the quality of my patches increase in time so please bear with me for a bit :)
On 13-02-19 12:04, Julien Lepiller wrote:
> Le 2019-02-13 11:40, Dan Frumin a écrit :
>> ---
>> gnu/packages/coq.scm | 40 ++++++++++++++++++++++++++++++++++++++++
>> 1 file changed, 40 insertions(+)
>>
>> diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
>> index fa02f85cd..494c3404b 100644
>> --- a/gnu/packages/coq.scm
>> +++ b/gnu/packages/coq.scm
>> @@ -500,3 +500,43 @@ 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.")
>> (license license:bsd-3))))
>
> Hi Dan, thanks for this patch! I have some comments below to help improve the
> quality of future patches, as well as two questions you need to answer before
> I can push that patch.
>
>> +
>> +(define-public coq-equations
>> + (package
>> + (name "coq-equations")
>> + (synopsis "Equations - a function definition plugin")
>
> Could you put this just before the description field, so this package definition
> looks more like the rest of guix? A better synopsis would be "Function definiton
> plugin for coq" I think.
I've reordered the fields to match the rest of the package definitions in guix.
>
>> + (version "1.2-beta")
>
> Why a beta version? We try to stick to stable releases in Guix. Please add a
> comment explaining the reason.
>
Oh, I just wanted to use the latest released version. I can replace it with the version 1.1 while I wait for the non-beta 1.2 releas.
>> + (source (origin
>> + (method url-fetch)
>> + (uri (string-append
>> + "https://github.com/mattam82/Coq-Equations/archive/v"
>> + version "-8.8.tar.gz"))
>> + (file-name (string-append name "-v" version "8.8.tar.gz"))
>
> We cannot use auto-generated tarballs from github, because we found that
> they sometimes get regenerated in an unreproducible way, so it breaks the
> checksum test. You can use this instead:
>
> (method git-fetch)
> (uri (git-reference
> (url "https://githu.com/mattam82/Coq-Equations.git")
> (commit (string-append "v" version "-8.8"))))
>
> and update the sha256 accordingly. As an added bonus, this means that we
> can always fetch from the software heritage in case the repo disappears
> one day :)
I was not aware of that. How can I get the sha256 hash in this case? Normally I would do `guix download <url>`.
>
>> + (sha256
>> + (base32
>> "1j7yarhddk2c2l4b6h8g5n0xz5vfy1bqmgh832g01di5gjwshy3f"))))
>> + (build-system gnu-build-system)
>> + (native-inputs
>> + `(("findlib" ,ocaml)
>
> ocaml doesn't provide findlib directly, ocaml-findlib does. What do you
> want to do here?
Sorry, I think I was confused here. I've corrected this in the updated patch.
>
>> + ("coq" ,coq)
>> + ("camlp5" ,camlp5)))
>> + (arguments
>> + `(#:test-target "test-suite"
>> + #:phases
>> + (modify-phases %standard-phases
>> + (replace 'configure
>> + (lambda* (#:key outputs #:allow-other-keys)
>> + (invoke "coq_makefile" "-f" "_CoqProject" "-o" "Makefile")))
>> + (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"))))))
>
> Please make sure that these two phases both return #t.
I thought that `invoke' automatically checks that the return code is correct?
>
>> + (description "Equations provides a notation for writing programs
>> +by dependent pattern-matching and (well-founded) recursion in Coq. It
>> +compiles everything down to eliminators for inductive types, equality
>> +and accessibility, providing a definitional extension to the Coq
>> +kernel.")
>
> Please make sure that each sentence is separated by two spaces.
> `guix lint coq-equations` should be able to tell you about it.
>
>> + (home-page "https://mattam82.github.io/Coq-Equations/")
>> + (license license:lgpl2.1)))
>
> Thanks again! I really only need an answer for the beta version and
> ocaml/findlib questions. I can take care of the rest, but I would
> appreciate it if you could do it yourself ;)
[-- Attachment #2: 0001-gnu-Add-coq-equations.patch --]
[-- Type: text/x-patch, Size: 2407 bytes --]
From ebbb6e1cb1f667f33cc4e4320fdb91edf33264dc Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 13 Feb 2019 12:34:40 +0100
Subject: [PATCH] gnu: Add coq-equations.
---
gnu/packages/coq.scm | 40 ++++++++++++++++++++++++++++++++++++++++
1 file changed, 40 insertions(+)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index fa02f85cd..b7eadc2fd 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -500,3 +500,43 @@ 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.")
(license license:bsd-3))))
+
+(define-public coq-equations
+ (package
+ (name "coq-equations")
+ (version "1.1")
+ (source (origin
+ (method git-fetch)
+ (uri (git-reference
+ (url "https://github.com/mattam82/Coq-Equations.git")
+ (commit (string-append "v" version "-8.8"))))
+ (file-name (git-file-name name version))
+ (sha256
+ (base32 "129rxsdsf88vjcw0xhm74yax1hmnk6f8n9ksg0hcyyjq1ijddiwa"))))
+ (build-system gnu-build-system)
+ (native-inputs
+ `(("ocaml" ,ocaml)
+ ("coq" ,coq)
+ ("camlp5" ,camlp5)))
+ (arguments
+ `(#:test-target "test-suite"
+ #:phases
+ (modify-phases %standard-phases
+ (replace 'configure
+ (lambda* (#:key outputs #:allow-other-keys)
+ (invoke "coq_makefile" "-f" "_CoqProject" "-o" "Makefile")))
+ (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"))))))
+ (home-page "https://mattam82.github.io/Coq-Equations/")
+ (synopsis "Function definition plugin for Coq")
+ (description "Equations provides a notation for writing programs
+by dependent pattern-matching and (well-founded) recursion in Coq. It
+compiles everything down to eliminators for inductive types, equality
+and accessibility, providing a definitional extension to the Coq
+kernel.")
+ (license license:lgpl2.1)))
--
2.17.1
next prev parent reply other threads:[~2019-02-13 11:38 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-02-13 10:40 [bug#34466] [PATCH] gnu: Add coq-equations Dan Frumin
2019-02-13 11:04 ` Julien Lepiller
2019-02-13 11:35 ` Dan Frumin
2019-02-13 11:36 ` Dan Frumin [this message]
2019-02-13 12:19 ` [bug#34466] Fwd: " Julien Lepiller
2019-02-13 12:39 ` Danny Milosavljevic
2019-02-13 12:45 ` Julien Lepiller
2019-02-13 13:23 ` Danny Milosavljevic
2019-02-13 21:22 ` bug#34466: " Julien Lepiller
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
List information: https://guix.gnu.org/
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=e463eb9d-009f-5d9e-831a-a3ae8eb6dbac@cs.ru.nl \
--to=dfrumin@cs.ru.nl \
--cc=34466@debbugs.gnu.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
Code repositories for project(s) associated with this public inbox
https://git.savannah.gnu.org/cgit/guix.git
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).