| Message ID | 20190213104024.1963-1-dfrumin@cs.ru.nl |
|---|---|
| State | Accepted |
| Headers | show |
| Series | [bug#34466] gnu: Add coq-equations. | expand |
| Context | Check | Description |
|---|---|---|
| cbaines/applying patch | fail | Apply failed |
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. > + (version "1.2-beta") Why a beta version? We try to stick to stable releases in Guix. Please add a comment explaining the reason. > + (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 :) > + (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? > + ("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. > + (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 ;)
Pushed as ec23bae682ab144179fad8d5ed6c2545d85384ad, thank you!
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)))) + +(define-public coq-equations + (package + (name "coq-equations") + (synopsis "Equations - a function definition plugin") + (version "1.2-beta") + (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")) + (sha256 + (base32 "1j7yarhddk2c2l4b6h8g5n0xz5vfy1bqmgh832g01di5gjwshy3f")))) + (build-system gnu-build-system) + (native-inputs + `(("findlib" ,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")))))) + (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.") + (home-page "https://mattam82.github.io/Coq-Equations/") + (license license:lgpl2.1)))