Message ID | e463eb9d-009f-5d9e-831a-a3ae8eb6dbac@cs.ru.nl |
---|---|
State | Accepted |
Headers | show |
Series | [bug#34466] Fwd: Re: [bug#34466] [PATCH] gnu: Add coq-equations. | expand |
Context | Check | Description |
---|---|---|
cbaines/applying patch | fail | Apply failed |
Le 2019-02-13 12:36, Dan Frumin a écrit : > (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: >> >> 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>`. you can always try to build the package, which will fail and tell you what the correct hash was. I forgot, the filename should be: (file-name (git-file-name name version)) >> >> Please make sure that these two phases both return #t. > > I thought that `invoke' automatically checks that the return code is > correct? It does, and when the code is not correct, it throws an exception. When it is correct, it returns #<unspecified>, so we need to explicitly return #t. Thank you! I'll try to build the package and take care of the rest before pushing your patch later today.
Hi Julien,
> When [invoke's child return status] is correct, [invoke] returns #<unspecified>, so we need to explicitly return #t.
That's not true. invoke returns #t in the successful case--I designed it that way mostly to get rid of the many vestigal #t's in phases.
(I hope that in a future version of guix, the necessity of using #t to end phases will be gone entirely)
Le 2019-02-13 13:39, Danny Milosavljevic a écrit : > Hi Julien, > >> When [invoke's child return status] is correct, [invoke] returns >> #<unspecified>, so we need to explicitly return #t. > > That's not true. invoke returns #t in the successful case--I designed > it that way mostly to get rid of the many vestigal #t's in phases. > > (I hope that in a future version of guix, the necessity of using #t to > end phases will be gone entirely) Ah, thanks for the info! So I guess we don't need to end any phase with #t in that package definition, correct?
On Wed, 13 Feb 2019 13:45:43 +0100 Julien Lepiller <julien@lepiller.eu> wrote: > Ah, thanks for the info! So I guess we don't need to end any phase with > #t > in that package definition, correct? Correct.
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