| Message ID | 871s65ykf7.fsf@gmail.com |
|---|---|
| State | Accepted |
| Headers | show |
| Series | [bug#33865] gnu: Add dedukti. | expand |
| Context | Check | Description |
|---|---|---|
| cbaines/applying patch | fail | Apply failed |
Le Tue, 25 Dec 2018 11:16:13 +0100, Gabriel Hondet <gabrielhondet@gmail.com> a écrit : > * gnu/packages/ocaml.scm (dedukti): New variable. Nice! Thank you! > --- > gnu/packages/ocaml.scm | 55 > ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 > insertions(+) > > diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm > index 3b1ddcb5b..28e223e75 100644 > --- a/gnu/packages/ocaml.scm > +++ b/gnu/packages/ocaml.scm > @@ -4989,3 +4989,58 @@ 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 dedukti > + (package > + (name "dedukti") > + (version "2.6.0") > + (home-page "https://deducteam.github.io/") > + (source > + (origin > + (method git-fetch) > + (uri (git-reference > + (url "https://github.com/deducteam/dedukti.git") > + (commit (string-append "v" version)))) > + (file-name (git-file-name name version)) > + (sha256 > + (base32 > + "0frl3diff033i4fmq304b8wbsdnc9mvlhmwd7a3zd699ng2lzbxb")))) > + (inputs > + `(("ocaml" ,ocaml) > + ("menhir" ,ocaml-menhir))) > + (native-inputs > + `(("ocamlbuild" ,ocamlbuild) > + ("ocamlfind" ,ocaml-findlib) > + ("which" ,which))) > + (build-system gnu-build-system) I wonder why you didn't use the ocaml-build-system... > + (arguments > + `(#:phases > + (modify-phases %standard-phases > + (replace 'configure > + ;; Set ocamlfind environment vars > + (lambda _ > + (let ((out (assoc-ref %outputs "out")) > + (libpath "/lib/ocaml/site-lib")) > + (begin > + (setenv "OCAMLFIND_DESTDIR" (string-append out > libpath)) > + (mkdir-p (string-append out libpath "/dedukti")) > + (setenv "PREFIX" out) > + #t)))) It should automates all of this > + (replace 'build > + (lambda _ > + (invoke "make"))) > + (replace 'check > + (lambda _ > + (invoke "make" "tests"))) > + ;; (delete 'check) Be carefull not to let this kind of thing slip through ;) > + (add-before 'install 'set-binpath > + ;; Change binary path in the makefile > + (lambda _ > + (let ((out (assoc-ref %outputs "out"))) > + (substitute* "GNUmakefile" > + (("BINDIR = (.*)$") > + (string-append "BINDIR = " out "/bin"))))))))) > + (synopsis "Implementation of the ΛΠ-calculus modulo rewriting") I don't think this synpsis is understandable to everyone. Could you use instead a more general sentence that give an impression of what ΛΠ-calculus modulo rewriting is? > + (description "Dedukti is a logical framework based on the > +ΛΠ-calculus modulo in which many theories and logics can be > expressed.") Or if you can't, please explain it with a sentence or two in the description ;) > + (license license:cecill-c))) Other than that, looks good to me. I'll have to test it once you answer my questions, and if it works, I'll push the patch for you. Thanks again!
diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 3b1ddcb5b..28e223e75 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -4989,3 +4989,58 @@ 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 dedukti + (package + (name "dedukti") + (version "2.6.0") + (home-page "https://deducteam.github.io/") + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/deducteam/dedukti.git") + (commit (string-append "v" version)))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "0frl3diff033i4fmq304b8wbsdnc9mvlhmwd7a3zd699ng2lzbxb")))) + (inputs + `(("ocaml" ,ocaml) + ("menhir" ,ocaml-menhir))) + (native-inputs + `(("ocamlbuild" ,ocamlbuild) + ("ocamlfind" ,ocaml-findlib) + ("which" ,which))) + (build-system gnu-build-system) + (arguments + `(#:phases + (modify-phases %standard-phases + (replace 'configure + ;; Set ocamlfind environment vars + (lambda _ + (let ((out (assoc-ref %outputs "out")) + (libpath "/lib/ocaml/site-lib")) + (begin + (setenv "OCAMLFIND_DESTDIR" (string-append out libpath)) + (mkdir-p (string-append out libpath "/dedukti")) + (setenv "PREFIX" out) + #t)))) + (replace 'build + (lambda _ + (invoke "make"))) + (replace 'check + (lambda _ + (invoke "make" "tests"))) + ;; (delete 'check) + (add-before 'install 'set-binpath + ;; Change binary path in the makefile + (lambda _ + (let ((out (assoc-ref %outputs "out"))) + (substitute* "GNUmakefile" + (("BINDIR = (.*)$") + (string-append "BINDIR = " out "/bin"))))))))) + (synopsis "Implementation of the ΛΠ-calculus modulo rewriting") + (description "Dedukti is a logical framework based on the +ΛΠ-calculus modulo in which many theories and logics can be expressed.") + (license license:cecill-c)))