From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([208.118.235.92]:56378) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gbjsb-0005mJ-KW for guix-patches@gnu.org; Tue, 25 Dec 2018 05:24:06 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gbjsY-00038j-Ge for guix-patches@gnu.org; Tue, 25 Dec 2018 05:24:05 -0500 Received: from debbugs.gnu.org ([208.118.235.43]:34835) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1gbjsY-00037z-DW for guix-patches@gnu.org; Tue, 25 Dec 2018 05:24:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1gbjsY-0001UN-5h for guix-patches@gnu.org; Tue, 25 Dec 2018 05:24:02 -0500 Subject: [bug#33865] [PATCH] gnu: Add dedukti. Resent-Message-ID: Received: from eggs.gnu.org ([208.118.235.92]:56257) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gbjs5-0005jk-SF for guix-patches@gnu.org; Tue, 25 Dec 2018 05:23:34 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gbjs2-00027V-OK for guix-patches@gnu.org; Tue, 25 Dec 2018 05:23:33 -0500 Received: from mail-wm1-x329.google.com ([2a00:1450:4864:20::329]:33188) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1gbjs1-00022g-Fn for guix-patches@gnu.org; Tue, 25 Dec 2018 05:23:29 -0500 Received: by mail-wm1-x329.google.com with SMTP id r24so20543961wmh.0 for ; Tue, 25 Dec 2018 02:23:28 -0800 (PST) Received: from glht-x240.gmail.com ([92.184.108.35]) by smtp.gmail.com with ESMTPSA id x20sm35253513wme.6.2018.12.25.02.23.26 for (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Tue, 25 Dec 2018 02:23:26 -0800 (PST) From: Gabriel Hondet Date: Tue, 25 Dec 2018 11:16:13 +0100 Message-ID: <871s65ykf7.fsf@gmail.com> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha256; protocol="application/pgp-signature" 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: 33865@debbugs.gnu.org --=-=-= Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable * gnu/packages/ocaml.scm (dedukti): New variable. =2D-- 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 =2D-- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -4989,3 +4989,58 @@ provides BigN, BigZ, BigQ that used to be part of Co= q 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 =3D (.*)$") + (string-append "BINDIR =3D " out "/bin"))))))))) + (synopsis "Implementation of the =CE=9B=CE=A0-calculus modulo rewritin= g") + (description "Dedukti is a logical framework based on the +=CE=9B=CE=A0-calculus modulo in which many theories and logics can be expr= essed.") + (license license:cecill-c))) =2D-=20 2.20.1 --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEE5ercJXBcjd3P1FcAMbyBBfZZ1CUFAlwiBRwACgkQMbyBBfZZ 1CUfrRAAoFhfPNQnIPgMG4ajAte/bhALhqdeLxswjQKHjcMRNpcZObnC73npPUGo MjGO9yIWmnsl+TIb9LzK9S+248XVzka+RMI4giePbn3GsAuYPZgJW59DbwdVLeP5 jkiQFh+D66wuKbM/EUL1D1ARBaMcrSVCL5CBTBFkoOhsg+j9xWEwhNXEeExYXggy YZK6juwUd3if9bPwNaue+0VmnaD5Ulvsyl1ovqhywEveOmpbO1xa9Ee0LRJScB32 1d7dvkcymSnQOixISfCgRIFjsHRxUXoU6YGVclWCcjlO2xJ27T1T6bZsO/DTjX1/ 72/hyen8h2y8UpUmQ2uzgZfydPog//xkQAxUh+idaNKBiLl4z77+XQ7w20lHl8jx sTwJP1Y6TJUOz/DKXYXfMbuTHI3aIt3213zyiX5R3MiWz5mUJzRhHr2Bxkgsq1Hr ZSH2PW6r9qBhvqP//Fu0PUsDyiT721D/MlcMbe1WkD+VVHUDdPCG3JqH2oyWr/Al bmBzjbPfCP9ILCByy8qpG8WV5Aou5rrwRRrJX2DkmUMzTCKBoeVnU0PlVg1VSKzR k/t+SJ4I1N9pzX30rgXtvFD7R4vzK+xM80b3MhDQ8G+vkBueWoVrpUCfcr40QWcn VMfRmKK5hSpv1rht1FRwdM4beFfTuYWuoHWRXjUQt4EeuJ/mEhM= =2xtu -----END PGP SIGNATURE----- --=-=-=--