From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([209.51.188.92]:56104) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1gu2Tm-0005Ir-Oa for guix-patches@gnu.org; Wed, 13 Feb 2019 16:54:07 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1gu2Tk-0005ZL-Sg for guix-patches@gnu.org; Wed, 13 Feb 2019 16:54:06 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:48154) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1gu2Ti-0005XU-Dp for guix-patches@gnu.org; Wed, 13 Feb 2019 16:54:03 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1gu2Ti-0005U4-1D for guix-patches@gnu.org; Wed, 13 Feb 2019 16:54:02 -0500 Subject: [bug#34361] [PATCH 4/4] gnu: Add lambdapi. Resent-Message-ID: Date: Wed, 13 Feb 2019 22:53:21 +0100 From: Julien Lepiller Message-ID: <20190213225321.0d3becac@lepiller.eu> In-Reply-To: <87h8dgf58h.fsf@gmail.com> References: <87lg2sf6az.fsf@gmail.com> <87h8dgf58h.fsf@gmail.com> MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; boundary="Sig_/cK_fFEVOzLXRnyB0eeBFKzb"; 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: 34361@debbugs.gnu.org --Sig_/cK_fFEVOzLXRnyB0eeBFKzb Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Le Sat, 2 Feb 2019 11:51:25 +0100, Gabriel Hondet a =C3=A9crit : > * gnu/packages/ocaml.scm (lambdapi): New variable. > --- > gnu/packages/ocaml.scm | 57 > ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 > insertions(+) >=20 > diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm > index 34229107f..227a87287 100644 > --- a/gnu/packages/ocaml.scm > +++ b/gnu/packages/ocaml.scm > @@ -4843,6 +4843,63 @@ of the standard library (Pervasives module). > However, it is less efficient than the first one.") > (license license:expat))) > =20 > +(define-public lambdapi > + (package > + (name "lambdapi") > + (version "1.0") > + (home-page "https://github.com/Deducteam/lambdapi") > + (source (origin > + (method git-fetch) > + (uri (git-reference > + (url (string-append home-page ".git")) > + (commit (string-append name "-" version)))) > + (modules '((guix build utils))) > + (snippet '(begin > + ;; 'Earley_core' not opened in the files > + (substitute* '("src/pos.ml" > + "src/parser.ml" > + "src/lambdapi.ml") > + (("(Input|Earley|Charset)" all) > + (string-append "Earley_core." all))))) > + (sha256 > + (base32 > + > "0kf31xcwsgvadf3kfw8ipwkgcwh99xwb8adx8ap8sd7b4pwa5rc0")) > + (file-name (git-file-name name version)))) > + (build-system dune-build-system) > + (inputs > + `(("ocaml-yojson" ,ocaml-yojson) > + ("ocaml-easy-format" ,ocaml-easy-format) > + ("ocaml-biniou" ,ocaml-biniou) > + ("ocaml-menhir" ,ocaml-menhir) > + ("ocaml-cmdliner" ,ocaml-cmdliner) > + ("ocaml-ppx-inline-test" ,ocaml-ppx-inline-test) > + ("ocaml-timed" ,ocaml-timed) > + ("ocaml-bindlib" ,ocaml-bindlib) > + ("ocaml-earley" ,ocaml-earley) > + ("ocamlbuild" ,ocamlbuild))) ;ocamlbuild for tests > + (arguments > + '(#:phases > + (modify-phases %standard-phases > + (replace 'check > + (lambda _ > + (invoke "make" "real_tests") > + #t))))) > + (synopsis "Extension of Dedukti with metavariables and tactics") > + (description "Lambdapi is an implementation of the =CE=BB=CE=A0-calc= ulus > modulo +rewriting, which is the system of > @url{https://github.com/Deducteam/Dedukti, +Dedukti}. Lamdapi is > +@itemize > +@item > +a logical framework, > +@item > +a tool for interoperability of proof systems, > +@item > +an interactive proof system, > +@item > +an experimental proof system. > +@end itemize") > + (license license:lgpl2.1))) > + > (define-public ocaml-biniou > (package > (name "ocaml-biniou") This package builds fine, but in the end, here is what I get installed: Installing /gnu/store/1dh8ni590ai2nbbqrxxvgcfnlgwslsi3-lambdapi-1.0/lib/oca= ml/site-lib/lambdapi/META Installing /gnu/store/1dh8ni590ai2nbbqrxxvgcfnlgwslsi3-lambdapi-1.0/lib/oca= ml/site-lib/lambdapi/opam Installing /gnu/store/1dh8ni590ai2nbbqrxxvgcfnlgwslsi3-lambdapi-1.0/doc/lam= bdapi/README.md and that's all. Could you fix this package so it actually installs something usefull? I've pushed all three dependencies already as 70c7d02590a93d3950747a9538e3882cb34bcd49 - 8213db7c951ea84597f8ac859d3ae588481ec5a2 --Sig_/cK_fFEVOzLXRnyB0eeBFKzb Content-Type: application/pgp-signature Content-Description: Signature digitale OpenPGP -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEEtfrmKFtBNyiyoPrtQxEfRSAIagwFAlxkkdIACgkQQxEfRSAI agyAkw/7ByKBujcsCSe1p0a1MMzc6ygffnAVaOZZmHThdD2i3xd0DOS52V+7q/uE Yp49eYIJ4jRqDjmd140CczlizP9t8NfZBsq9F1WkusXMuGZKS+huosz0lr7+NGlF A/7Z7sObCAKPWH4U3lo0uq6RvyuQqBXh7ybeWKiJyj+bIAXc1p+mLxDtYXL8r5Fc XYakGiWDWR9mMHUVo4qKe+F7ykm50oLeOzaxoGe5W9PaXPbcTZnF7VDQ4V2SWkid PtTU+OhzXw9SNvTULv8X94RAvoAR9pRrMCxoX3POeseki3Tmc9v3hHNhzxLMC7LF WGxbChn9mvB+8SwltWkwtCE3IAhAGfN/XatM244fkhBqGjuUY3ktRmAwwZVJLgRk itW8NwsFSJcRpyc4HcFsO+Lmv2wZEmTPUv+KEqK8Ea3gjxGAgtQ+aSM6E64Nnwyx 3V/U7+t5hwhrIxEllu6tbBt6ycK8VsEh8k7wdfxYrJnRLpjlCkbRsgS+k9y7Iepe 2Ree9uPiZIL/frEvQmqIZJW8SFRw7CGsTu4KMRcyn4ALi0FJ564aVusG5Hx1B3Lb KaXTaFkrjJ67tWsKpSMX50JMxGtnrfiQRoKb3Kvj+P71r0HQw8SVoxw2r9+bmrlp mGCgGjKhh8Osu5mLTwinTlvxqO737UMEPM1cAr3pYmguRqKJqIE= =EP/A -----END PGP SIGNATURE----- --Sig_/cK_fFEVOzLXRnyB0eeBFKzb--