From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([208.118.235.92]:48338) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gbogj-0000V8-FN for guix-patches@gnu.org; Tue, 25 Dec 2018 10:32:10 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gbogf-00082s-K1 for guix-patches@gnu.org; Tue, 25 Dec 2018 10:32:09 -0500 Received: from debbugs.gnu.org ([208.118.235.43]:57130) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1gbogc-00081C-Fv for guix-patches@gnu.org; Tue, 25 Dec 2018 10:32:03 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1gbogc-00031o-8t for guix-patches@gnu.org; Tue, 25 Dec 2018 10:32:02 -0500 Subject: [bug#33865] [PATCH] gnu: Add dedukti. Resent-Message-ID: References: <871s65ykf7.fsf@gmail.com> <20181225123219.3c10f4ad@lepiller.eu> From: Gabriel Hondet In-reply-to: <20181225123219.3c10f4ad@lepiller.eu> Date: Tue, 25 Dec 2018 16:31:10 +0100 Message-ID: <87y38dwrlt.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: Julien Lepiller Cc: 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 | 58 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 58 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 3b1ddcb5b..8962a7339 100644 =2D-- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -4989,3 +4989,61 @@ 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))) + (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"))) + (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 "Proof-checker for the =CE=BB=CE=A0-calculus modulo theory, = an extension of +the =CE=BB-calculus") + (description "Dedukti is a proof-checker for the =CE=BB=CE=A0-calculus= modulo +theory. The =CE=BB=CE=A0-calculus is an extension of the simply typed =CE= =BB-calculus with +dependent types. The =CE=BB=CE=A0-calculus modulo theory is itself an ext= ension of the +=CE=BB=CE=A0-calculus where the context contains variable declaration as w= ell as rewrite +rules. This system is not designed to develop proofs, but to check proofs +developed in other systems. In particular, it enjoys a minimalistic synta= x.") + (license license:cecill-c))) =2D-=20 2.20.1 On Tue 25 Dec 2018 at 12:32 Julien Lepiller wrote: > I wonder why you didn't use the ocaml-build-system... I'm not an expert yet regarding the different build systems, but the current package essentially relies on a ~make~ and ~make install~ process, and is not linked with oasis or dune things (and using ocaml-build-system failed as well, but perhaps I should investigate more). > 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 ;) I hope the new one is clearer... --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEE5ercJXBcjd3P1FcAMbyBBfZZ1CUFAlwiTT4ACgkQMbyBBfZZ 1CXLwA/+NYedwZNafW0Fo2n8NtdbvhV71YVs4L9pkhTcutCwMvjc6qxAtBC72XcJ EGfx7hWe456P1uTf36xSWWuZ0NfMWlShddnOciQedDizJsek5OxJoKDD2iTk96G+ lv5lQkj4pRWXLwsQbhi5qJjr51zEaiv+4kPvx/AuU1TKjfpv8ukWRjklVGqfBKLV dDIXcVMVnCTCQbTTcsQ8EFk+RD9knWfN+vCo3h/gqsCFRvrlgUzK6B4vHwNuwQ9F nGJJkfOjy2kz2jQUUaO7rnw9uqIk137IFAIr1tYy+I+9356AMCJe82db4PVy61n7 zVn/szPukBf2bvMeI5ePIvAHfLWsrAxg2rP39Nk/YKDJoevNQT4qvg3VPe6fKLMh zh8i57ZFWyffiLUijrYLxYPymSG5MZqNUK2iRAqCayiaraZ+ZC8AT92BbEIOSHaa TilfVVCj/jolXjspqF2OXYln7IjeYv6mvIT60vHkN9XIuY0uxlW2F7p1lh6wMlw3 GfayEdtyXMrunjysmljeh5OijUvCjB0TFtEbJu9wK7+6tIp5m+GjEF//zHEx1kr9 Lui3XIQuTiEA1UyfJNJoS1J8Qq1W0DyeB5wcu1dyT6QdypARheZYp1R+EumCWKiW itXVS04xROPeh0uDd/ELifEi3rVx1THf+j2AvFnuLt1aWk1G8LU= =xFDL -----END PGP SIGNATURE----- --=-=-=--