From debbugs-submit-bounces@debbugs.gnu.org Thu Feb 07 01:43:04 2019 Received: (at submit) by debbugs.gnu.org; 7 Feb 2019 06:43:04 +0000 Received: from localhost ([127.0.0.1]:36466 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1grdOq-0003Wq-FJ for submit@debbugs.gnu.org; Thu, 07 Feb 2019 01:43:04 -0500 Received: from eggs.gnu.org ([209.51.188.92]:39468) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1grdOo-0003WJ-B2 for submit@debbugs.gnu.org; Thu, 07 Feb 2019 01:43:02 -0500 Received: from lists.gnu.org ([209.51.188.17]:47100) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1grdOj-0007Ib-0Z for submit@debbugs.gnu.org; Thu, 07 Feb 2019 01:42:57 -0500 Received: from eggs.gnu.org ([209.51.188.92]:53837) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1grdOi-0002NT-2U for guix-patches@gnu.org; Thu, 07 Feb 2019 01:42:56 -0500 X-Spam-Checker-Version: SpamAssassin 3.3.2 (2011-06-06) on eggs.gnu.org X-Spam-Level: **** X-Spam-Status: No, score=4.2 required=5.0 tests=BAYES_50,DATE_IN_PAST_96_XX, 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 1grdOh-0007HH-7Z for guix-patches@gnu.org; Thu, 07 Feb 2019 01:42:56 -0500 Received: from mail-wm1-x343.google.com ([2a00:1450:4864:20::343]:40880) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1grdOg-000785-Ug for guix-patches@gnu.org; Thu, 07 Feb 2019 01:42:55 -0500 Received: by mail-wm1-x343.google.com with SMTP id q21so5376066wmc.5 for ; Wed, 06 Feb 2019 22:42:36 -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=jA1qnZnaKkskHrll72SunLPDHSgirFdW/aS7J1LBO1o=; b=LwfyaliZilPtvOYbCzXnEahJQWxTw5eEeKTr1cpDuaAzF85u39+vpwSDlDeYoI4TeM ERbK5s71DFwDha54IdofH8LH2aPSXafaODCbSrH3yg+RAHyJrQRm3kOZl79O/X33hCoC KkcGFJEGn4nuiFBv5ZSIiY+L8icqiSrGPqg5q8M3YuJ6miClccltLvIoaxKrpXrU8rUP 1Bg0v/nAWDCmTxAsJ6Jfq0NIRpvTm2Jk+qfxwOOYQVAKBLHvI+vLxJhABLX7CO2bh3pY Xyv+EomPc8kcbNm+sr/QYQZlWx095gif8PV+zUpb9/UHGUst6K5HwMWMLODPQWp0pZA7 ZBEw== 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=jA1qnZnaKkskHrll72SunLPDHSgirFdW/aS7J1LBO1o=; b=ddgA/BGF6U0bJhjFUOzfWociSYVWdpQIZqEUWPCGXr5Q5DIzB7yA62TPc00VCAeSXc VtxuaJNnbmUQHwRkEwk+TdhbK4yUeDbQ3H+es8FebrI9WJ9trYd8jZZNjiwh+1D/9kgu Hm7VB3dKJXSVvKjDCv/q7Cp2Df9RKMWrJsmFsuVPMT0VzGC16XA8U/vstZ6ob/nweugR Np/yS6qqDJbpLJeraA0jAdIjqe4YFVlhEjFrWYwWTcfJI89sGD5XdhqohgqM+K+vyY3w Bc84BtYR7zwWoguj9qECceh/Ukl6H+TsZtpmM1lQpzp1PHxHH54FmMOl5nZkhO5/yDL/ wXgw== X-Gm-Message-State: AHQUAubaLQpsxeIQ0u/Ihv/ObiRANlkJAkiwUc03Y8kpD7MJ1zajpRXD mioKaHxV0mv7o7YZhF8JcCJEuCfZ X-Google-Smtp-Source: AHgI3IZXjC5tSyTctxu4VYUciUAdHtZok8dNroMJrJin4axaKxawc9WEdD4Q7PGo4wARHcuWmCBsQw== X-Received: by 2002:a1c:a4c4:: with SMTP id n187mr5971306wme.15.1549521754863; Wed, 06 Feb 2019 22:42:34 -0800 (PST) Received: from glht-aurore.gmail.com (2a01cb04062c860082fa5bfffe3823d7.ipv6.abo.wanadoo.fr. [2a01:cb04:62c:8600:82fa:5bff:fe38:23d7]) by smtp.gmail.com with ESMTPSA id m6sm15111551wrv.24.2019.02.06.22.42.33 for (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Wed, 06 Feb 2019 22:42:33 -0800 (PST) User-agent: mu4e 1.0; emacs 26.1 From: Gabriel Hondet To: guix-patches@gnu.org Subject: [PATCH 1/4] gnu: Add ocaml-earley. Date: Fri, 1 Feb 2019 20:20:54 +0100 Message-ID: <87lg2sf6az.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::343 X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-Spam-Score: 3.0 (+++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: * gnu/packages/ocaml.scm (ocaml-earley): New variable. --- gnu/packages/ocaml.scm | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 2d33db1c0..59630028e 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -4727,6 +4727,36 @@ syntax checking on deduk [...] Content analysis details: (3.0 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 1.0 SPF_SOFTFAIL SPF: sender does not match SPF record (softfail) 2.1 DATE_IN_PAST_96_XX Date: is 96 hours or more before Received: date 0.0 FREEMAIL_FROM Sender email is commonly abused enduser mail provider (gabrielhondet[at]gmail.com) 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: 2.0 (++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: * gnu/packages/ocaml.scm (ocaml-earley): New variable. --- gnu/packages/ocaml.scm | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 2d33db1c0..59630028e 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -4727,6 +4727,36 @@ syntax checking on deduk [...] Content analysis details: (2.0 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 1.0 SPF_SOFTFAIL SPF: sender does not match SPF record (softfail) 2.1 DATE_IN_PAST_96_XX Date: is 96 hours or more before Received: date 0.0 FREEMAIL_FROM Sender email is commonly abused enduser mail provider (gabrielhondet[at]gmail.com) -1.0 MAILING_LIST_MULTI Multiple indicators imply a widely-seen list manager --=-=-= Content-Type: text/plain Content-Transfer-Encoding: quoted-printable * gnu/packages/ocaml.scm (ocaml-earley): New variable. =2D-- gnu/packages/ocaml.scm | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 2d33db1c0..59630028e 100644 =2D-- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -4727,6 +4727,36 @@ syntax checking on dedukti files.") "Part of the Jane Street's PPX rewriters collection.") (license license:expat))) =20 +(define-public ocaml-earley + (package + (name "ocaml-earley") + (version "2.0.0") + (home-page "https://github.com/rlepigre/ocaml-earley") + (source + (origin + (method git-fetch) + (uri (git-reference + (url (string-append home-page ".git")) + (commit version))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "18k7bi7krc4bvqnhijz1q0pfr0nfahghfjifci8rh1q4i5zd0xz5")))) + (build-system dune-build-system) + (arguments + `(#:phases + (modify-phases %standard-phases + (replace 'check + (lambda _ + (invoke "make" "tests") + #t))))) + (synopsis "Parsing library based on Earley Algorithm") + (description "Earley is a parser combinator library base on Earley's +algorithm. It is intended to be used in conjunction with an OCaml syntax +extension which allows the definition of parsers inside the language. The= re +is also support for writing OCaml syntax extensions in a camlp4 style.") + (license license:cecill-b))) + (define-public ocaml-biniou (package (name "ocaml-biniou") =2D-=20 2.20.1 --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEE5ercJXBcjd3P1FcAMbyBBfZZ1CUFAlxb01QACgkQMbyBBfZZ 1CWdCQ//dXd+Kt4pwK+eVS0z3Nf3AFNyVthcoDD4KfUnC5HEtItT9RbwEqDK80AI FMt+0uN+ByhFp4mileTnBPANQqQFpou1XJGE+M75VmvjFRw8iZUTQiuwoa0wJM+6 lmXfem+OPEzhV5B9LRKhXDPEMI00fs1gKyiep7SFhyx8yug/vzil65QFG1HEHkAG ihqyLlTpYaHx5pR37CIE2NS/um1bJJpHr0ZCGA830BcbZKCPqr/nqUJNJP3ENWor cE6uKgWLG/aR1lx/HWn+wfxQY8LytnActLBeC56JDbWJNAQrhT+Xn0wmX3qlYTiX 94zqx7vyUF64knTMtLP2K9gBidSZCn4U0HxZiVaEoX7Xwo+m9WGm7c71S3AzbmB7 QCLXSqg3eSw7Wc4DOKJdPteRXs7BdIUo2XHnCyI9EuxTewiTItKg5vuxE3It4iYW hlnuti0BNkMpCDp6ktH4xX49T9qCBSlCAKpqKUIFI1iOH+zf5H9+P7aczZEN5XR8 2l4WSUVJpEikFgTf5pgV2xpPCD3Hzo5nXsH/6XaCFB4+SQeCB0hhszZ5PIHgTrEv aIT8PLK2ygLS5Xkvv/tbUhLCYx3Z4UriN4Xeo0NhEDlk8FPErILPaJi2AGLn8sdF ZunbAPj7Bd+iX0HCIdqxbusDHV0tr+4IqeEuRtBKwFthzKO0coY= =o1No -----END PGP SIGNATURE----- --=-=-=-- From debbugs-submit-bounces@debbugs.gnu.org Thu Feb 07 01:49:10 2019 Received: (at 34361) by debbugs.gnu.org; 7 Feb 2019 06:49:10 +0000 Received: from localhost ([127.0.0.1]:36471 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1grdUk-0003gQ-9W for submit@debbugs.gnu.org; Thu, 07 Feb 2019 01:49:10 -0500 Received: from mail-wr1-f66.google.com ([209.85.221.66]:32963) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1grdUh-0003fy-JS for 34361@debbugs.gnu.org; Thu, 07 Feb 2019 01:49:08 -0500 Received: by mail-wr1-f66.google.com with SMTP id a16so10279655wrv.0 for <34361@debbugs.gnu.org>; Wed, 06 Feb 2019 22:49:07 -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=kcUbAl0SaZaylvpJhvf9KWdKYtCvS5NcjLJvLQTnI+E=; b=Wvr6/Ue3IY0En+vG0zO4esSyk9v1vK7tg+6QX2Ad3m2ZfSY2hWqHOHu7FKU3vOFLSE Ukj1s738Ecvv/AUlQzdXqztppuuqLm+tDiO5AvvdlUrkIjmzhaW5KuXCStxbSmeOPftp rnIXbpK4ASWyeN1kUlM/EFNlpEGLoezDO4Bt2KNHas9xuYivB5tpWO4jpkLnz7gzE1cM GiXYMfNl3Q/LNjMDcPZiPskM+L/1IAwWsrEoTPakk8zlRLNzDXFJ7C+gcTT+FqePfz5j XGpdtxFHASZlr3mfTeK+Qi7ribdGt0c1FUSfyWRat0dxg6cDHunIalFIaMNanEA0ZsZG ducA== 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=kcUbAl0SaZaylvpJhvf9KWdKYtCvS5NcjLJvLQTnI+E=; b=KNzB9PaUo3wivSAL7fFDf25sUw4H/mXBsi0Xru1Ep3O1a/Cb466ycGWjJxtZZsH7w3 9l0AbBQyiw2sWgSjkE+GmFrgQ0bjMx8eJZ0Hg42j+95GgXSr2siNj2czP0GwMv7AXjRi UwG9YccYt6242hIVlucmdo5mXNreXSQy6M17uFHnZknG12WOAevFAMv3jxnmyjUd7oeI c0TZhu/wYapN1XNgFEE59Ff3CtAbFIdf7aawwb7/wzqSqTsSwO6DurUTnlOLix7iqd+m XOpuuRnVyYLTFMsiD1re6KuKIFRiY/g+TKCEMzX/OaiohOIHbk2V4iAmO49e/IbQOZEE iYHw== X-Gm-Message-State: AHQUAubWOSB7ifDtHIrFpBbKQ0HNg6QWhhhBw3ABDMWYGY1v5jZFCttT eq9M9k+xP4eMkFaJjJamLvdTmfvy X-Google-Smtp-Source: AHgI3IbWjCX7QwYz5J34a3AfW3mMDJufy0BxmKx3T3SsjSEnzNF4J7oY/+GmFZ19JA8KTJepc69TjA== X-Received: by 2002:adf:e949:: with SMTP id m9mr9839106wrn.17.1549522141231; Wed, 06 Feb 2019 22:49:01 -0800 (PST) Received: from glht-aurore.gmail.com (2a01cb04062c860082fa5bfffe3823d7.ipv6.abo.wanadoo.fr. [2a01:cb04:62c:8600:82fa:5bff:fe38:23d7]) by smtp.gmail.com with ESMTPSA id o64sm21770896wmo.47.2019.02.06.22.49.00 for <34361@debbugs.gnu.org> (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Wed, 06 Feb 2019 22:49:00 -0800 (PST) User-agent: mu4e 1.0; emacs 26.1 From: Gabriel Hondet To: 34361@debbugs.gnu.org Subject: [PATCH 2/4] gnu: Add ocaml-bindlib. Date: Fri, 1 Feb 2019 20:31:34 +0100 Message-ID: <87k1icf603.fsf@gmail.com> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha256; protocol="application/pgp-signature" X-Spam-Score: 2.1 (++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: * gnu/packages/ocaml.scm (ocaml-bindlib): New variable. --- gnu/packages/ocaml.scm | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 59630028e..ede3beb03 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -4727,6 +4727,45 @@ syntax checking on deduk [...] Content analysis details: (2.1 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- -0.0 RCVD_IN_DNSWL_NONE RBL: Sender listed at http://www.dnswl.org/, no trust [209.85.221.66 listed in list.dnswl.org] -0.0 RCVD_IN_MSPIKE_H2 RBL: Average reputation (+2) [209.85.221.66 listed in wl.mailspike.net] -0.0 SPF_PASS SPF: sender matches SPF record 2.1 DATE_IN_PAST_96_XX Date: is 96 hours or more before Received: date 0.0 FREEMAIL_FROM Sender email is commonly abused enduser mail provider (gabrielhondet[at]gmail.com) X-Debbugs-Envelope-To: 34361 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.1 (+) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: * gnu/packages/ocaml.scm (ocaml-bindlib): New variable. --- gnu/packages/ocaml.scm | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 59630028e..ede3beb03 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -4727,6 +4727,45 @@ syntax checking on deduk [...] Content analysis details: (1.1 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- -0.0 RCVD_IN_MSPIKE_H2 RBL: Average reputation (+2) [209.85.221.66 listed in wl.mailspike.net] -0.0 RCVD_IN_DNSWL_NONE RBL: Sender listed at http://www.dnswl.org/, no trust [209.85.221.66 listed in list.dnswl.org] -0.0 SPF_PASS SPF: sender matches SPF record 2.1 DATE_IN_PAST_96_XX Date: is 96 hours or more before Received: date 0.0 FREEMAIL_FROM Sender email is commonly abused enduser mail provider (gabrielhondet[at]gmail.com) -1.0 MAILING_LIST_MULTI Multiple indicators imply a widely-seen list manager --=-=-= Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable * gnu/packages/ocaml.scm (ocaml-bindlib): New variable. =2D-- gnu/packages/ocaml.scm | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 59630028e..ede3beb03 100644 =2D-- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -4727,6 +4727,45 @@ syntax checking on dedukti files.") "Part of the Jane Street's PPX rewriters collection.") (license license:expat))) =20 +(define-public ocaml-bindlib + (package + (name "ocaml-bindlib") + (version "5.0.1") + (build-system ocaml-build-system) + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/rlepigre/ocaml-bindlib.git") + (commit (string-append "ocaml-bindlib_" version)))) + (file-name (git-file-name name version)) + (sha256 + (base32 + "1f8kr81w8vsi4gv61xn1qbc6zrzkjp8l9ix0942vjh4gjxc74v75")))) + (native-inputs + `(("ocamlbuild" ,ocamlbuild) + ("ocaml-findlib" ,ocaml-findlib))) + (arguments + `(#:tests? #f ;no tests + #:phases + (modify-phases %standard-phases + (delete 'configure) + (replace 'build + (lambda _ + (invoke "make") + #t)) + (replace 'install + (lambda _ + (invoke "make" "install") + #t))))) + (home-page "https://rlepigre.github.io/ocaml-bindlib/") + (synopsis "OCaml Bindlib library for bound variables") + (description "Bindlib is a library allowing the manipulation of data +structures with bound variables. It is particularly useful when writing A= STs +for programming languages, but also for manipulating terms of the =CE=BB-c= alculus +or quantified formulas.") + (license license:gpl3+))) + (define-public ocaml-earley (package (name "ocaml-earley") =2D-=20 2.20.1 --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEE5ercJXBcjd3P1FcAMbyBBfZZ1CUFAlxb1NwACgkQMbyBBfZZ 1CXesg//TXQEzeLoyJ5M2gmBKrKLGnDG1YtY2+nFVi0HjfDQLp4wj1uYOXUYFDIk O4m9zt+xD9YT3Wu9KpqhWW6/camQ8evht47zhH/+YYlQqaA2VFf8KvvHbhu+fW2A VW6vo3n2GXNxZHTNIFW1U6Fedkcmd2ZuTgNVuZ2zUONcddlsjG/Hx5G6P/Q5Rs0N F/0CUusURsr9j6D0/J36lOSC1Pb5wO/onPxwYWxZbXH6Q4llRjmn7h1rvyRtBmfj bgal/Fy0rMXuC5Y4LkMWwTHglzexU1c6UcoIOWUlsYet1P8nrl/+jCqMKcUaWmpS UTQZDF5Rj824BuNRBNcxMfTuut60l9NkWcSo2YgHyQ0UZuSyn7KZjsJxN7bzu1DX pP2YiIyuES0S4koYn6nZTPGmz2TnfC3dHNBCgPVQvYy3TKW+ELVtSgd8fBTFn89F Bd9emdvOeuUsRRo0NmzrPC/V1j9Ds12f/Q2UN66hEcfE/YPHpUXw32hC3eRdXKJq KW6xWvERaMdR5HHcaGqhwaK6RPOoGiQS7Wky7vHDSH/80FsxQIliF9jD4Gvace1+ JifzG5N70lsLgvxVk6+LEQDjk/xbAvtSquGDvX5AWFcgczTFpuWxBsixxKHvIECg 6FPtuPicaOl8C6+oV+tmXJxeq7VEBaXGENUGyJRCLGVIYaX+H3Q= =Ljky -----END PGP SIGNATURE----- --=-=-=-- From debbugs-submit-bounces@debbugs.gnu.org Thu Feb 07 02:04:39 2019 Received: (at 34361) by debbugs.gnu.org; 7 Feb 2019 07:04:39 +0000 Received: from localhost ([127.0.0.1]:36478 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1grdjj-000445-3q for submit@debbugs.gnu.org; Thu, 07 Feb 2019 02:04:39 -0500 Received: from mail-wm1-f67.google.com ([209.85.128.67]:36482) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1grdjh-00043s-Nd for 34361@debbugs.gnu.org; Thu, 07 Feb 2019 02:04:38 -0500 Received: by mail-wm1-f67.google.com with SMTP id p6so5422980wmc.1 for <34361@debbugs.gnu.org>; Wed, 06 Feb 2019 23:04:37 -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=wI7/zAZiTNi22FWCuFENfFe94Sro2HVtV4GwvHfeAJY=; b=Op/jQV8TtwtNT3To2OefkLXIiWYyihKHrK/sFBpQFRfKt3pS22KWl+lQoS9P0nwCgK RfKGiai0V7GT1jBBngkweZJCB3/9xBx0dCq89nXQxpqCeCR6QrogCjT2km3nhPupTN0g kGLuLHtmZ2t6bdu+hE7Mwwy6QHK5q1OkiiHzgUQVGrwbz6F5AWEGcsBODEOyWKizT+qP R6JeaXjW3qeCv0+3BUUWdwXu5rocIVjOaw3vc3m+EfeRxhG2Jwi9gabJ5t4SNagbkxUV IJO/x2YzmhGMDMkEXAX9QT1Ej7yBbm6OCe1uk4ArWJ7yslKVP4/8qn/obLYuJjkTcdwC 3WUg== 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=wI7/zAZiTNi22FWCuFENfFe94Sro2HVtV4GwvHfeAJY=; b=FQUMUX9ZY4SVTOJRJQ2U1mmY3ZfCV5vATvm9NxfYBxwDnxcYoKZT62G5WmxlXGlU/9 iRFkC3g8p8fST5TqN26lTGRWDfZtxEhP8XFfbcdQE7kZiO87icLly7uJ+hslLGD7st67 +q4aI1LsegWw+hivTx5fxgb7NOv9ijEwy/CUGIuQPV5j9CQbUytzVrir5iQ1gB9hFApT Kan8FI2fT7Q84mM0U5kCqKXOECDOOYePd4ldQNOrwaPOOhcdPzKmqmg5brCID2YqOLQh aJuwl4fdD66AAD9ZFOHM8BPsCy+tIOtGXYnCMOCiQQsx+qKdFTLt9wqko+Fx0mQvVWwO x/jA== X-Gm-Message-State: AHQUAuam0aaMYak/+jduEcxauhGdWjq6sVDVE7+pxLsqQ9ktQmlX6oAl 27PICav0bRclw5Rku7jkJEva0aN9 X-Google-Smtp-Source: AHgI3IboBOp9gn4iSyKGrdt552kMSz0TgNElhJqMdbyqJpcOQMZ1UceoilD6lY6htcnXi8bAta4BKA== X-Received: by 2002:a1c:27c6:: with SMTP id n189mr5907357wmn.108.1549523071683; Wed, 06 Feb 2019 23:04:31 -0800 (PST) Received: from glht-aurore.gmail.com (2a01cb04062c860082fa5bfffe3823d7.ipv6.abo.wanadoo.fr. [2a01:cb04:62c:8600:82fa:5bff:fe38:23d7]) by smtp.gmail.com with ESMTPSA id y145sm17987192wmd.30.2019.02.06.23.04.30 for <34361@debbugs.gnu.org> (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Wed, 06 Feb 2019 23:04:31 -0800 (PST) User-agent: mu4e 1.0; emacs 26.1 From: Gabriel Hondet To: 34361@debbugs.gnu.org Subject: [PATCH 3/4] gnu: Add ocaml-timed. Date: Fri, 1 Feb 2019 20:50:25 +0100 Message-ID: <87imxwf5a9.fsf@gmail.com> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha256; protocol="application/pgp-signature" X-Spam-Score: 2.1 (++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: * gnu/packages/ocaml.scm (ocaml-timed): New variable. --- gnu/packages/ocaml.scm | 47 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index ede3beb03..34229107f 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -4796,6 +4796,53 @@ extension which allows t [...] Content analysis details: (2.1 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- -0.0 SPF_PASS SPF: sender matches SPF record 2.1 DATE_IN_PAST_96_XX Date: is 96 hours or more before Received: date 0.0 FREEMAIL_FROM Sender email is commonly abused enduser mail provider (gabrielhondet[at]gmail.com) -0.0 RCVD_IN_DNSWL_NONE RBL: Sender listed at http://www.dnswl.org/, no trust [209.85.128.67 listed in list.dnswl.org] X-Debbugs-Envelope-To: 34361 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.1 (+) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: * gnu/packages/ocaml.scm (ocaml-timed): New variable. --- gnu/packages/ocaml.scm | 47 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index ede3beb03..34229107f 100644 --- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -4796,6 +4796,53 @@ extension which allows t [...] Content analysis details: (1.1 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- -0.0 RCVD_IN_DNSWL_NONE RBL: Sender listed at http://www.dnswl.org/, no trust [209.85.128.67 listed in list.dnswl.org] -0.0 SPF_PASS SPF: sender matches SPF record 2.1 DATE_IN_PAST_96_XX Date: is 96 hours or more before Received: date 0.0 FREEMAIL_FROM Sender email is commonly abused enduser mail provider (gabrielhondet[at]gmail.com) -1.0 MAILING_LIST_MULTI Multiple indicators imply a widely-seen list manager --=-=-= Content-Type: text/plain Content-Transfer-Encoding: quoted-printable * gnu/packages/ocaml.scm (ocaml-timed): New variable. =2D-- gnu/packages/ocaml.scm | 47 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index ede3beb03..34229107f 100644 =2D-- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -4796,6 +4796,53 @@ extension which allows the definition of parsers ins= ide the language. There is also support for writing OCaml syntax extensions in a camlp4 style.") (license license:cecill-b))) =20 +(define-public ocaml-timed + (package + (name "ocaml-timed") + (version "1.0") + (home-page "https://github.com/rlepigre/ocaml-timed") + (source (origin + (method git-fetch) + (uri (git-reference + (url (string-append home-page ".git")) + (commit (string-append name "_" version)))) + (sha256 + (base32 + "0hfxz710faxy5yk97bkfnw87r732jcxxhmjppwrbfdb6pd0wks96")) + (file-name (git-file-name name version)))) + (build-system ocaml-build-system) + (native-inputs + `(("ocaml-findlib" ,ocaml-findlib))) + (arguments + '(#:phases + (modify-phases %standard-phases + (delete 'configure) + (replace 'build + (lambda _ + (invoke "make") + #t)) + (replace 'install + (lambda _ + (invoke "make" "install") + #t)) + (replace 'check + (lambda _ + (invoke "make" "tests") + #t))))) + (synopsis "Timed references for imperative state") + (description "Timed references for imperative state. This module prov= ides +an alternative type for references (or mutable cells) supporting undo/redo +operations. In particular, an abstract notion of time is used to capture = the +state of the references at any given point, so that it can be restored. N= ote +that usual reference operations only have a constant time / memory overhead +(compared to those of the standard library). + +Moreover, we provide an alternative implementation based on the references +of the standard library (Pervasives module). However, it is less efficient +than the first one.") + (license license:expat))) + (define-public ocaml-biniou (package (name "ocaml-biniou") =2D-=20 2.20.1 --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEE5ercJXBcjd3P1FcAMbyBBfZZ1CUFAlxb2H4ACgkQMbyBBfZZ 1CXbSQ/7BghTKXXuXkjVAZHAJkPrwhqes4UauDAeIx9QfXzAYTsp3E3OVkdTe3al vm30/lOMQ7JlIbHCPnWSGZ8uYibE4D55QnGhrMBWMM/7WDgfBdxLQYRLWbOjPdbd qOLeWjlQR1rIIh5+WGvm0N4BmXHwc1UqURhtP/2pm3ffwwu+vJl5W/4F0kPXwZsm MsH2gFW8nZOsjq4Hj8aqUBppoz3VAFpbqnynd70nb5LlkmISBhrZD5OaIbWVgN+l O5kV5QkMTvSjaobuSU1VgpCM9M8ZN+tjO2BZNDTTJHDFIc7pwKsU1Ixmv887BoRg 6eyhK969lMYy2G8ohfnXRhWut6PzqHtCq+EAIn9vKZyfieaZdI0W/t5WkZpawueh qyy6yTVfGlPyhLA+cCQQU5iM6w02dCO8tnpLeUD9DRJSFFMC1+kc50eCBatA67yR fwg1L2o9C0IbswwG1E7LEJiHkqIo28BZqkR3oXrZCEF7LxaoRi7Y5Df7n5VnPncy pGk3WozRkNYazfPFUVP9kKPAKojYN79CX/obqFbewhlPUaDxmVnrcGNLhwibeQUy ypfjxbVHwWE8VlkNqmCMXr949dKvGJUMUPOJMAD6yYyAizR9aR41bjgNB4r9KmHj n4n8Xfku7I7gUmGdS+jKiIv8P+Bejd0d3TKJYElbJO7vGO5YW2M= =HiSi -----END PGP SIGNATURE----- --=-=-=-- From debbugs-submit-bounces@debbugs.gnu.org Thu Feb 07 02:05:44 2019 Received: (at 34361) by debbugs.gnu.org; 7 Feb 2019 07:05:44 +0000 Received: from localhost ([127.0.0.1]:36483 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1grdkm-00046A-Gf for submit@debbugs.gnu.org; Thu, 07 Feb 2019 02:05:44 -0500 Received: from mail-wr1-f67.google.com ([209.85.221.67]:43616) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1grdkk-00045t-06 for 34361@debbugs.gnu.org; Thu, 07 Feb 2019 02:05:42 -0500 Received: by mail-wr1-f67.google.com with SMTP id r2so10224289wrv.10 for <34361@debbugs.gnu.org>; Wed, 06 Feb 2019 23:05:41 -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=nC8+KxZE38OipeEDkEeLsFA7Hz5wZTQnZihmjOsb26k=; b=vbTqJoPtp6iW59N35vFlE2XoLEoN4MrxqklWrgVFJjD+A5QY8x80OanfVHsSqvapu8 aryItgdL2Jg3Z1P08PKBZmvG5yMqmC/9Y1PxpVKof+Xcl0OodOEHDYJcSKnpOLAvoDC+ uN3E/rwWg1KplaaF7rOKa+RqILcyjk13mAbRnlqEfLYYx4W+yIAC77JxN5kR9eBb26No 3cpMmjmvwIjU1PtKmoROp+3mllVdo0D2hCB9zGEV82ZF2sr2jplxobO3u2wYUTtiVr7e 8UG+Y/cvFrURmu3Cd+uz19/POSdAcYIqId8xe4EjEl25bk54jE8mWTXpLRk8dXhq93qR iVwg== 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=nC8+KxZE38OipeEDkEeLsFA7Hz5wZTQnZihmjOsb26k=; b=BN9qmcSSCTOY0ZgMnnZtO+S8r6nhcEKzneGape4Fs9JmQgIR/Z+N0sGBMy2CWI1CUV DjbMle/iTkoDC0mW28i48x/Wq5p7zL1Gxh7UC03joAwr7/w2v6xua9Vub/jp+O2K7bbV VuufSDQg8baGElB1ttybPjzTFUZXpY7cvgzrkh8irkWrCHfdQx1mfAQfA3nJqW5gLeyL Us8TWY2pqLCl37A6fP0OZ3kPLbJbs1ZjzhRtKC9ohwxYtr+yEM1li87vFTWiF8/VGbF4 RwZ5hLXPpJY6mSXlyUF1QQi30Vmfb5a1MUCmj1VwmKNObveslmtGij7wfCZCuPZYnA50 UoEQ== X-Gm-Message-State: AHQUAuYUXMWiq0Rh7OEJoscL43x7jIlJrHmYnXhJ8RBFgeWgioiplRCx WZFpvWDm40E3EusbzbMI2Qdj5Eq/ X-Google-Smtp-Source: AHgI3IbXGz0oIfnWilf1iazHQBLgcgZu13HkdDgwSRzme6ODnbfBc6WMa/Cx0o0KRYvKWybhkoKChg== X-Received: by 2002:a5d:4bc7:: with SMTP id l7mr10583100wrt.242.1549523136085; Wed, 06 Feb 2019 23:05:36 -0800 (PST) Received: from glht-aurore.gmail.com (2a01cb04062c860082fa5bfffe3823d7.ipv6.abo.wanadoo.fr. [2a01:cb04:62c:8600:82fa:5bff:fe38:23d7]) by smtp.gmail.com with ESMTPSA id a12sm40824987wro.18.2019.02.06.23.05.35 for <34361@debbugs.gnu.org> (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Wed, 06 Feb 2019 23:05:35 -0800 (PST) User-agent: mu4e 1.0; emacs 26.1 From: Gabriel Hondet To: 34361@debbugs.gnu.org Subject: [PATCH 4/4] gnu: Add lambdapi. Date: Sat, 2 Feb 2019 11:51:25 +0100 Message-ID: <87h8dgf58h.fsf@gmail.com> MIME-Version: 1.0 Content-Type: multipart/signed; boundary="=-=-="; micalg=pgp-sha256; protocol="application/pgp-signature" X-Spam-Score: 3.8 (+++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: * gnu/packages/ocaml.scm (lambdapi): New variable. --- gnu/packages/ocaml.scm | 57 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) 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 [...] Content analysis details: (3.8 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 1.7 URIBL_BLACK Contains an URL listed in the URIBL blacklist [URIs: parser.ml] -0.0 SPF_PASS SPF: sender matches SPF record 2.1 DATE_IN_PAST_96_XX Date: is 96 hours or more before Received: date 0.0 FREEMAIL_FROM Sender email is commonly abused enduser mail provider (gabrielhondet[at]gmail.com) -0.0 RCVD_IN_DNSWL_NONE RBL: Sender listed at http://www.dnswl.org/, no trust [209.85.221.67 listed in list.dnswl.org] -0.0 RCVD_IN_MSPIKE_H2 RBL: Average reputation (+2) [209.85.221.67 listed in wl.mailspike.net] X-Debbugs-Envelope-To: 34361 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: 2.8 (++) X-Spam-Report: Spam detection software, running on the system "debbugs.gnu.org", has NOT identified this incoming email as spam. The original message has been attached to this so you can view it or label similar future email. If you have any questions, see the administrator of that system for details. Content preview: * gnu/packages/ocaml.scm (lambdapi): New variable. --- gnu/packages/ocaml.scm | 57 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) 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 [...] Content analysis details: (2.8 points, 10.0 required) pts rule name description ---- ---------------------- -------------------------------------------------- 1.7 URIBL_BLACK Contains an URL listed in the URIBL blacklist [URIs: parser.ml] -0.0 RCVD_IN_MSPIKE_H2 RBL: Average reputation (+2) [209.85.221.67 listed in wl.mailspike.net] -0.0 RCVD_IN_DNSWL_NONE RBL: Sender listed at http://www.dnswl.org/, no trust [209.85.221.67 listed in list.dnswl.org] -0.0 SPF_PASS SPF: sender matches SPF record 2.1 DATE_IN_PAST_96_XX Date: is 96 hours or more before Received: date 0.0 FREEMAIL_FROM Sender email is commonly abused enduser mail provider (gabrielhondet[at]gmail.com) -1.0 MAILING_LIST_MULTI Multiple indicators imply a widely-seen list manager --=-=-= Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable * gnu/packages/ocaml.scm (lambdapi): New variable. =2D-- gnu/packages/ocaml.scm | 57 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/gnu/packages/ocaml.scm b/gnu/packages/ocaml.scm index 34229107f..227a87287 100644 =2D-- a/gnu/packages/ocaml.scm +++ b/gnu/packages/ocaml.scm @@ -4843,6 +4843,63 @@ of the standard library (Pervasives module). Howeve= r, 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-calcul= us modulo +rewriting, which is the system of @url{https://github.com/Deducteam/Dedukt= i, +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") =2D-=20 2.20.1 --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEE5ercJXBcjd3P1FcAMbyBBfZZ1CUFAlxb2L4ACgkQMbyBBfZZ 1CVETA/8DfxW5i8FOQMcANbEC7HW4JaexhnwUshUqCdS/xjNe2rTrxLtfqwm7ZZw 3ribFWIeFOR1V+eG3W9jR49CIxJT/rWn31YnLh20Uvp7woWV5za20+6ZEZ+oCi6O fyyXifyGc22rmTFjd7GpmIk3QjHpe/ozvHN5ylATac3cMHmGwF8xVqn6NfvBzgat A4yJlcrRLk9GG8gm1JiQgFm8JXSXWMiMtgjwY9pjIDMz5Dl3CRsnvKsSzuGcsbe5 ffpgFabfFaUByoUmaXVkiP6Afn1HRfqAC+uV9W0eiSW75FiR3D6lB7FnniDVplwO 0ciNhemNIaMahc/b2foAvbHssvE79Zx6v5ycjpr6BfUzPC9YKanD++nBkq5HxQCk 99ADB1t4eOk19N682U9QK8pATzu34ayqF6cRNjd9tIuKCOog4bxkgIHYQ4EZxYjk y+1ESPvVaTKwLmP1SlAObHT4cr8kll9E5e5TvDESJPbRpKUyQMReECUnBN7rPw/G Uvd3BBfdPlEhpW0eaepe4f83Sj0H/+lZxSfO89VAKZu5PUMd4yBnqqBHbXKE/spA rjYAJ1r7+el0JJEfqT4FwGOYB+aCDF2FOLBknY3lxVsUzzNC1AX2Dy/Vr7VU+miY PZmzXHFdztny/Nnnpkq0Ts+4kh/HNjZqs5nyG8LbB+19EyZj+zs= =6KiN -----END PGP SIGNATURE----- --=-=-=-- From debbugs-submit-bounces@debbugs.gnu.org Wed Feb 13 16:53:45 2019 Received: (at 34361) by debbugs.gnu.org; 13 Feb 2019 21:53:45 +0000 Received: from localhost ([127.0.0.1]:47435 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gu2TR-0005TU-0R for submit@debbugs.gnu.org; Wed, 13 Feb 2019 16:53:45 -0500 Received: from lepiller.eu ([89.234.186.109]:51276) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1gu2TO-0005TI-BD for 34361@debbugs.gnu.org; Wed, 13 Feb 2019 16:53:43 -0500 Received: from localhost (static-176-182-42-79.ncc.abo.bbox.fr [176.182.42.79]) by lepiller.eu (OpenSMTPD) with ESMTPSA id a49963f7 (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256:NO) for <34361@debbugs.gnu.org>; Wed, 13 Feb 2019 21:53:33 +0000 (UTC) Date: Wed, 13 Feb 2019 22:53:21 +0100 From: Julien Lepiller To: 34361@debbugs.gnu.org Subject: Re: [bug#34361] [PATCH 4/4] gnu: Add lambdapi. Message-ID: <20190213225321.0d3becac@lepiller.eu> In-Reply-To: <87h8dgf58h.fsf@gmail.com> References: <87lg2sf6az.fsf@gmail.com> <87h8dgf58h.fsf@gmail.com> X-Mailer: Claws Mail 3.17.3 (GTK+ 2.24.32; x86_64-unknown-linux-gnu) MIME-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; boundary="Sig_/cK_fFEVOzLXRnyB0eeBFKzb"; protocol="application/pgp-signature" X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 34361 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_/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-- From debbugs-submit-bounces@debbugs.gnu.org Sat May 04 15:14:45 2019 Received: (at 34361-done) by debbugs.gnu.org; 4 May 2019 19:14:45 +0000 Received: from localhost ([127.0.0.1]:52298 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1hN07Q-0008OZ-UP for submit@debbugs.gnu.org; Sat, 04 May 2019 15:14:45 -0400 Received: from mail-wr1-f54.google.com ([209.85.221.54]:46722) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1hN07P-0008OM-QI for 34361-done@debbugs.gnu.org; Sat, 04 May 2019 15:14:44 -0400 Received: by mail-wr1-f54.google.com with SMTP id r7so11931212wrr.13 for <34361-done@debbugs.gnu.org>; Sat, 04 May 2019 12:14:43 -0700 (PDT) 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=NEv5RMu0IlG5tJk2W9+bxNDneJdRTBfdESEuFABoeKA=; b=Zn3mfxqmYLsGEqdO0mspULsh/gQ4cxZcT35elxbzyjMI6wY9kbO0f3bTEzRXdgsjgX iXSCRlJMsVn91aChVnCm6lLuKNUVv16AAB+vmKUgUQv4FNKFuFGpmh/t8k7rSRBfNRDb fITrtjJDfmlpGbcswQ8uMWTymogDSZGWeHVYkYoyyWOz1pVxSd9yQdK4iZsJWUU3Oebb TiZRuGSKgTR1sRhLg8WlbE/nV0GpzipRBWNoGAPE7zNi3HNhpO4GZpZ1XX8+774l5+Zn sGTWmLb7ctGB3iTvx9JZJbWNqmNbgKDWnbykbQcBlwIQFGlDqiEre3QV0ds3EYwMlpg4 PLRg== 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=NEv5RMu0IlG5tJk2W9+bxNDneJdRTBfdESEuFABoeKA=; b=cYH1y0X9jNVjmV1T+wLwcPwYuqOvHjF2lr3CgrXcibsTChQmnmOLWYt7J9CMuCwEkv K7Y6NBJZ2vENXn5NeE69KOzBbEh03DcUPYQFs11s29r7uascbVuEuIl3HkFqsbxaazlR 6vtNAnFKakbc7rlLw+9YOmJU+QMsEALQQ1fAJ76SIeLsXjMP7VJeOUd4viWo80i4zxaa I9N+we3yFxbi/VXka5ubav+kzIhjQ+nMPHVuk6vmR9GZczw0ldGd7xOxxkC+k5RGnnSm jXUQHjtjLY05K/GufA3EVt9FucIl0zNNhSY+51qqqxQF0NH/EoQdtoRjB+SnqW6k07f9 Mfrg== X-Gm-Message-State: APjAAAU1xG/RafswkuWxOO1mYozZiUv7bD6DGbne8icTWVgcLLUfoTqv BMXRJLA2Nm3nTfXiNIZqycYipS3a X-Google-Smtp-Source: APXvYqwvb7PBIlF6ShKV+svtlK92d0zUDB76p6lQa545p76bPvwWDwtRdZcOn2IeV/5sSj9RHiX/CQ== X-Received: by 2002:adf:d850:: with SMTP id k16mr4448814wrl.57.1556997277948; Sat, 04 May 2019 12:14:37 -0700 (PDT) Received: from glht-aurore.gmail.com (2a01cb04062c860082fa5bfffe3823d7.ipv6.abo.wanadoo.fr. [2a01:cb04:62c:8600:82fa:5bff:fe38:23d7]) by smtp.gmail.com with ESMTPSA id s3sm11560229wre.97.2019.05.04.12.14.37 for <34361-done@debbugs.gnu.org> (version=TLS1_3 cipher=AEAD-AES256-GCM-SHA384 bits=256/256); Sat, 04 May 2019 12:14:37 -0700 (PDT) User-agent: mu4e 1.2.0; emacs 26.2 From: Gabriel Hondet To: 34361-done@debbugs.gnu.org Subject: closing lambdapi Date: Sat, 04 May 2019 21:14:31 +0200 Message-ID: <87r29exca0.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: 34361-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 (-) --=-=-= Content-Type: text/plain Sorry for the delay regarding this package, I missed an email. Anyway, this software is still in development so I prefer not to add it. Gabriel --=-=-= Content-Type: application/pgp-signature; name="signature.asc" -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEE5ercJXBcjd3P1FcAMbyBBfZZ1CUFAlzN5JcACgkQMbyBBfZZ 1CUqtBAAh78NUX/biukvMmflZDACqyShkQ4jr+qTzBMPk4TIH3B+L2e4LFjYGchg DO9ESTNgbLp8mDmILPH/0/hbWUfO1q1MDyHiUT5zDijGjybbASI/tDQXtJQyIvpY 9D+Ra3/O7fwen+bdOYQcfhQny/Dy3oV3wYjibYpokhttyzEhQxIQ6nVUB1uFm+Vw cQSVPki5eUn9oo8vh05mS/XqI2/fqoBwkwwD36KWHDGvP1dxJkhn8941KpPWjeCY Jndx6thOn5ybVWcdTPvVX5ZLxxo7ajuV1GRzeH7u1uTnuboQlkpyzjekDusNPekB x8oF4cDC3qfrjA/+XXYN1T9hMcEKUjF4OQZIiomCkiPbl1HR90Rw0729r9rfqVFK mAp43KJrLua4QGpP32ihkehi0GEgVQ1tOBshOyYcWusn4Bfn8hVL7u2RCrfOHMF0 4Q+rfauzOjS/oSr8d0ktgzJzzAR1Qlv0Lq1Gmm3eaORvKh8WyguRYtHMgWQA0jAM js1hTwzkgu57fYvrnwJRG7eUXta1NdvvyZ3BwjhvuRk1PJ1snPS2i5ueH05yJcnh G2yLdGPZPNGGsak/Ig2MnrHWulSFV/2xTLPA6naIIPtoDrMU2V6Nt9goF73ZOWfw 5Uus6vutVBLwAZhSBY/iXfHeY4NCR3/TkpejcTscU/Aa0IWuV4E= =uuJJ -----END PGP SIGNATURE----- --=-=-=-- From unknown Tue Jun 17 22:12:45 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Sun, 02 Jun 2019 11:24:04 +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