From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([208.118.235.92]:37200) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gbkxP-0007lK-GL for guix-patches@gnu.org; Tue, 25 Dec 2018 06:33:08 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gbkxK-0001pn-Fr for guix-patches@gnu.org; Tue, 25 Dec 2018 06:33:07 -0500 Received: from debbugs.gnu.org ([208.118.235.43]:58815) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1gbkxK-0001pV-C7 for guix-patches@gnu.org; Tue, 25 Dec 2018 06:33:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1gbkxK-0003BZ-1v for guix-patches@gnu.org; Tue, 25 Dec 2018 06:33:02 -0500 Subject: [bug#33865] [PATCH] gnu: Add dedukti. Resent-Message-ID: Date: Tue, 25 Dec 2018 12:32:24 +0100 From: Julien Lepiller Message-ID: <20181225123219.3c10f4ad@lepiller.eu> In-Reply-To: <871s65ykf7.fsf@gmail.com> References: <871s65ykf7.fsf@gmail.com> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: Gabriel Hondet Cc: 33865@debbugs.gnu.org Le Tue, 25 Dec 2018 11:16:13 +0100, Gabriel Hondet a =C3=A9crit : > * gnu/packages/ocaml.scm (dedukti): New variable. Nice! Thank you! > --- > gnu/packages/ocaml.scm | 55 > ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 > insertions(+) >=20 > 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 =3D (.*)$") > + (string-append "BINDIR =3D " out "/bin"))))))))) > + (synopsis "Implementation of the =CE=9B=CE=A0-calculus modulo rewrit= ing") I don't think this synpsis is understandable to everyone. Could you use instead a more general sentence that give an impression of what =CE=9B=CE=A0-calculus modulo rewriting is? > + (description "Dedukti is a logical framework based on the > +=CE=9B=CE=A0-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!