From unknown Sat Jun 21 03:03:19 2025 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.509 (Entity 5.509) Content-Type: text/plain; charset=utf-8 From: bug#33865 <33865@debbugs.gnu.org> To: bug#33865 <33865@debbugs.gnu.org> Subject: Status: [PATCH] gnu: Add dedukti. Reply-To: bug#33865 <33865@debbugs.gnu.org> Date: Sat, 21 Jun 2025 10:03:19 +0000 retitle 33865 [PATCH] gnu: Add dedukti. reassign 33865 guix-patches submitter 33865 Gabriel Hondet severity 33865 normal tag 33865 patch thanks From debbugs-submit-bounces@debbugs.gnu.org Tue Dec 25 05:23:42 2018 Received: (at submit) by debbugs.gnu.org; 25 Dec 2018 10:23:42 +0000 Received: from localhost ([127.0.0.1]:35724 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gbjsD-0001Tn-Gf for submit@debbugs.gnu.org; Tue, 25 Dec 2018 05:23:42 -0500 Received: from eggs.gnu.org ([208.118.235.92]:48245) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gbjsC-0001TY-3N for submit@debbugs.gnu.org; Tue, 25 Dec 2018 05:23:40 -0500 Received: from lists.gnu.org ([208.118.235.17]:43912) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1gbjs6-0002Ga-Sf for submit@debbugs.gnu.org; Tue, 25 Dec 2018 05:23:34 -0500 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 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: X-Spam-Status: No, score=0.8 required=5.0 tests=BAYES_50,FREEMAIL_FROM autolearn=disabled version=3.3.2 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) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=user-agent:from:to:subject:date:message-id:mime-version; bh=uR3UXCIWgC4bfrTRXZipCqes3NcCMcE/9l6QChZmQiw=; b=lZSZqy0iVSNtNbTaev0ynsXxEL2OFKFX0m5kdk2CVkC8KThGfxak+clRXpDZWYrEgY Xp2pKJT3QYXAXOJAbAtwWAdOMf8sHkBqY1p6ZjmYvKQi1Bi+jQRXHuQzVxzvYUAxbMGj wjfNbWzTW7l9chiZal0Vxhc7W8kDq1HZ1sZ0NpLChQdDjL4Q/2ePsR80FQANJH4o0fIb lssO7sByehBZ6isKzL+GKGSIcGWFoQA1MUuY5qS2AwH0Nw0Zk+fk2YWku/4GF3rtYYE3 aUv0H04KfX6SyQEwJ6ukG516JW70e/67MFG2E269FmnEFMM9hZFU3Onxp5+peEQ0/K41 bCmA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:user-agent:from:to:subject:date:message-id :mime-version; bh=uR3UXCIWgC4bfrTRXZipCqes3NcCMcE/9l6QChZmQiw=; b=WdpVTJiAEjKb42ekBVElkZYt1suyLTKbjvz1gt32wgqByFhUcgXwddAI6S/850rXXA 1PKW9aO0wnDQhTShf7EvrODLMBejC6fbhxVlWyOZ4UO+AOm70Uh0by4D/ZxEd/E1Jp2I nYd2Ry21QvkSYqzcPjlQMy7U+iXvwRfIxMMw/EvxbpD8HuX70HVNvNkhn/VUPLemZPqx VDc9SF7M7k09NeTSYykNANGNdJfjEWZZPcuNN7obfmwY7om1Pr9Dtobfx1Ct9hVrTz4H x+ucLlNzneCHv0eLHYhbPcWnbBox4dKtUaDyktbB42xf9A3crpOSZivwbFeVHVEAsaIG JLDA== X-Gm-Message-State: AA+aEWadPO+/OW79nMV0qN/tocDadMODg+FLezSrUOcFiDRcYrDgUagZ ijS9kXuvGoQOlRJaYkdJM45XUwdR X-Google-Smtp-Source: AFSGD/WGuW5cPJz1n6Kfre2ssmoE6VrEdlGBai6cgxcHbq1JSQfDPpfyLLYbmlSEmtiogu0XjpujYw== X-Received: by 2002:a1c:27c6:: with SMTP id n189mr14568032wmn.108.1545733407409; Tue, 25 Dec 2018 02:23:27 -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) User-agent: mu4e 1.0; emacs 26.1 From: Gabriel Hondet To: guix-patches@gnu.org Subject: [PATCH] gnu: Add dedukti. 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" X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-Received-From: 2a00:1450:4864:20::329 X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-Spam-Score: -4.0 (----) X-Debbugs-Envelope-To: submit X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -5.0 (-----) --=-=-= 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----- --=-=-=-- From debbugs-submit-bounces@debbugs.gnu.org Tue Dec 25 06:32:36 2018 Received: (at 33865) by debbugs.gnu.org; 25 Dec 2018 11:32:36 +0000 Received: from localhost ([127.0.0.1]:35734 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gbkwu-0003Aq-3A for submit@debbugs.gnu.org; Tue, 25 Dec 2018 06:32:36 -0500 Received: from lepiller.eu ([89.234.186.109]:45760) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gbkws-0003Ag-9L for 33865@debbugs.gnu.org; Tue, 25 Dec 2018 06:32:34 -0500 Received: from localhost (41.189.242.67 [41.189.242.67]) by lepiller.eu (OpenSMTPD) with ESMTPSA id 4119c33f (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO); Tue, 25 Dec 2018 11:29:16 +0000 (UTC) Date: Tue, 25 Dec 2018 12:32:24 +0100 From: Julien Lepiller To: Gabriel Hondet Subject: Re: [bug#33865] [PATCH] gnu: Add dedukti. Message-ID: <20181225123219.3c10f4ad@lepiller.eu> In-Reply-To: <871s65ykf7.fsf@gmail.com> References: <871s65ykf7.fsf@gmail.com> X-Mailer: Claws Mail 3.17.1 (GTK+ 2.24.32; x86_64-unknown-linux-gnu) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 33865 Cc: 33865@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) 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! From debbugs-submit-bounces@debbugs.gnu.org Tue Dec 25 10:31:23 2018 Received: (at 33865) by debbugs.gnu.org; 25 Dec 2018 15:31:23 +0000 Received: from localhost ([127.0.0.1]:36365 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gbofy-00030o-JU for submit@debbugs.gnu.org; Tue, 25 Dec 2018 10:31:22 -0500 Received: from mail-wr1-f51.google.com ([209.85.221.51]:36296) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gbofw-00030b-4L for 33865@debbugs.gnu.org; Tue, 25 Dec 2018 10:31:20 -0500 Received: by mail-wr1-f51.google.com with SMTP id u4so13828041wrp.3 for <33865@debbugs.gnu.org>; Tue, 25 Dec 2018 07:31:20 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=references:user-agent:from:to:cc:subject:in-reply-to:date :message-id:mime-version; bh=z1ArTPAO9Xbr2KTPJ5CaXFCeLH7IzyzZ8a6UWYtjvc8=; b=uztbc5WD/ZLpg+NY8NlPrDBAf2bnQfmZvEqYQznWI6XD6kTN+CxGV8GANEFD6S+4eq gAkfEifgUM3kSYdqi69T4rYHkoHJ86s57R0BeM67GBLp8MiyumhTXivLNd7fPnTyZ6LK iE4zksT0epBKTD9PoTFaNMDX091rCZaxpguWjoT3Yrj2zCYSUYoLZsPBgckoD4fHxKEc qOIGjjhPc0TquOuSOHQEYO1hLj+buK4ibypLY1iKUumWxFfHET8m/um1gT75ELcYPNTo KSVU7SlOfYidArxUM211NdkDrmO6HlN4q7EZqEi7W0A5s3Hz22B6jjO8s/62VeSLraFr v9uw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:references:user-agent:from:to:cc:subject :in-reply-to:date:message-id:mime-version; bh=z1ArTPAO9Xbr2KTPJ5CaXFCeLH7IzyzZ8a6UWYtjvc8=; b=fBKu4qOuILxljwnDIdYdo2BWzXnHY8lA8jbmddVFr9igHN+TjjdzxSfsW7KqYq5qke 1E3t454sbgXuzQNrfFj06B3kQqcImEj5CjxWxc47ItkwhTil+M3f9yTHRGwWVOH9FY7X b91wdKb4sjrEE3YzvJOKr7Pi3RGfwAnY7+dLw+kghtAiXNwMwZF8hNHBEpPQ0VivmjnT KHzm7Q+5RTOjqazRZaeJfVMBY3IeE0lasz0Pk5dRmuNGs/49904LsvfIyqrUCwTFmz7V C54En6XXUFAjd0kFi4cZIIZf1cCUnPE/34lNyQmKfRclViF/GcsZgs4QhqvKVxphMio7 8Cwg== X-Gm-Message-State: AJcUukfVw9q9h/BLfOEmrnO/LDK2wQanSwcOfmDaBf+Sm10jH8BpbFZv 8tepiJlxhe4MRM2kMKZbq5Xnq+yD X-Google-Smtp-Source: ALg8bN7jjoo246/1wje48LAiNrCTA9mDPMei1ZFjPIg/5k0uoM+DD7JO5W/EzuN/UAOaoaK0VsLTLw== X-Received: by 2002:adf:b3c3:: with SMTP id x3mr15621228wrd.294.1545751874009; Tue, 25 Dec 2018 07:31:14 -0800 (PST) Received: from glht-x240.gmail.com ([80.12.58.201]) by smtp.gmail.com with ESMTPSA id o5sm40714041wmg.25.2018.12.25.07.31.11 (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Tue, 25 Dec 2018 07:31:12 -0800 (PST) References: <871s65ykf7.fsf@gmail.com> <20181225123219.3c10f4ad@lepiller.eu> User-agent: mu4e 1.0; emacs 26.1 From: Gabriel Hondet To: Julien Lepiller Subject: Re: [bug#33865] [PATCH] gnu: Add dedukti. 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" X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 33865 Cc: 33865@debbugs.gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) --=-=-= 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----- --=-=-=-- From debbugs-submit-bounces@debbugs.gnu.org Tue Dec 25 12:50:14 2018 Received: (at 33865-done) by debbugs.gnu.org; 25 Dec 2018 17:50:14 +0000 Received: from localhost ([127.0.0.1]:36409 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gbqqM-0006Vh-Lg for submit@debbugs.gnu.org; Tue, 25 Dec 2018 12:50:14 -0500 Received: from lepiller.eu ([89.234.186.109]:45768) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gbqqL-0006VZ-57 for 33865-done@debbugs.gnu.org; Tue, 25 Dec 2018 12:50:13 -0500 Received: from localhost (41.189.242.67 [41.189.242.67]) by lepiller.eu (OpenSMTPD) with ESMTPSA id 32eb6da6 (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO) for <33865-done@debbugs.gnu.org>; Tue, 25 Dec 2018 17:46:56 +0000 (UTC) Date: Tue, 25 Dec 2018 18:50:05 +0100 From: Julien Lepiller To: 33865-done@debbugs.gnu.org Subject: Re: [bug#33865] [PATCH] gnu: Add dedukti. Message-ID: <20181225185005.2177deb3@lepiller.eu> In-Reply-To: <87y38dwrlt.fsf@gmail.com> References: <871s65ykf7.fsf@gmail.com> <20181225123219.3c10f4ad@lepiller.eu> <87y38dwrlt.fsf@gmail.com> X-Mailer: Claws Mail 3.17.1 (GTK+ 2.24.32; x86_64-unknown-linux-gnu) MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; boundary="Sig_/VBo=MB79FBb0DnNammDLyBG"; protocol="application/pgp-signature" X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 33865-done X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) --Sig_/VBo=MB79FBb0DnNammDLyBG Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: quoted-printable Pushed as 5895696e4c28938d9201e4527d3a007dd8b47e32. I've slightly modified your patch to add a copyright line for yourself and use the ocaml-build-system. --Sig_/VBo=MB79FBb0DnNammDLyBG Content-Type: application/pgp-signature Content-Description: Signature digitale OpenPGP -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEEtfrmKFtBNyiyoPrtQxEfRSAIagwFAlwibc0ACgkQQxEfRSAI agzdeg/8DtWpAXlWAYmX8LW1ydK2Cap7REgDa5nrr3TH3mcYtvdNYBjoAKWQAT2c j8GbKqCDxUHt3ZRAC67Zs9LnuWQhe/jMyntcl1yoqDm9Bv/a0oIwiF04KtmZJ/mZ 02otgC2QGqGl9nd8LTqxeYEhEVg0zUshMzhsT0YmY7HGHUuYZ2MLLh5gW351HmpA 55Mtz6RFjpxgalxCqEHj9lKRCj5NJ+fyBeQespYvFKfVv4XfJ3eIqD3IJLQKsTWg GImvLmauXlnVUvgeiZHg6fn+sy38KTfghGDwt1hZutAfNem/jqllm2fapa2ZA69a 1goULtiU9bDAX/AFihLLLaVFZ/N+Yx9Iumf6YWpPJNSy2tbV8fY+DNdigyVzXae2 vOBPwx3mW5FDWFOEcuI07yMZDALnM3J6zDRZl4k1VhHP73Bw8FbvU/XZQUzh3KjO PrwsR25TyT7n+aIQHJ0Tlo2bnou7hvE/XepdZkGt1RPGd2/QS2Pn0icL0Vp0cX4W Pk2jKsqMoRy9BCowNpVVHUw+JKm3lXfV86GFXrE3Np13mPQLHf24a1Q3WK2l20Ah LK3d265faF/c+R26yQv+hbV94pvZpg1OVa3waPQlWQXVbtq8vE0d0bLTSM3TzA+w ObSSHj7CWCWSedph/SlhZi9Q0qn3K1n+tvjNgee6UuuC+GhtkZc= =tccb -----END PGP SIGNATURE----- --Sig_/VBo=MB79FBb0DnNammDLyBG-- From unknown Sat Jun 21 03:03:19 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Wed, 23 Jan 2019 12:24:05 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator