From patchwork Fri Feb 1 19:20:54 2019 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Gabriel Hondet X-Patchwork-Id: 969 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 0F1B716B45; Thu, 7 Feb 2019 06:44:10 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM, T_DKIM_INVALID,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id AD6D416ADC for ; Thu, 7 Feb 2019 06:44:09 +0000 (GMT) Received: from localhost ([127.0.0.1]:35207 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1grdPs-0002V3-0B for patchwork@mira.cbaines.net; Thu, 07 Feb 2019 01:44:08 -0500 Received: from eggs.gnu.org ([209.51.188.92]:53951) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1grdPn-0002Uy-Fs for guix-patches@gnu.org; Thu, 07 Feb 2019 01:44:04 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1grdPm-0007kk-MD for guix-patches@gnu.org; Thu, 07 Feb 2019 01:44:03 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:37185) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1grdPm-0007kZ-JD for guix-patches@gnu.org; Thu, 07 Feb 2019 01:44:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1grdPm-0003YI-D7 for guix-patches@gnu.org; Thu, 07 Feb 2019 01:44:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#34361] [PATCH 1/4] gnu: Add ocaml-earley. Resent-From: Gabriel Hondet Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Thu, 07 Feb 2019 06:44:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: report 34361 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 34361@debbugs.gnu.org X-Debbugs-Original-To: guix-patches@gnu.org Received: via spool by submit@debbugs.gnu.org id=B.154952178413573 (code B ref -1); Thu, 07 Feb 2019 06:44:02 +0000 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 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 Date: Fri, 1 Feb 2019 20:20:54 +0100 Message-ID: <87lg2sf6az.fsf@gmail.com> MIME-Version: 1.0 X-detected-operating-system: by eggs.gnu.org: Genre and OS details not recognized. X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6.x X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches * 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 dedukti files.") "Part of the Jane Street's PPX rewriters collection.") (license license:expat))) +(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. There +is also support for writing OCaml syntax extensions in a camlp4 style.") + (license license:cecill-b))) + (define-public ocaml-biniou (package (name "ocaml-biniou") From patchwork Fri Feb 1 19:31:34 2019 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Patchwork-Submitter: Gabriel Hondet X-Patchwork-Id: 970 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 9C27016B45; Thu, 7 Feb 2019 06:50:14 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM, T_DKIM_INVALID,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id 47EC416ADC for ; Thu, 7 Feb 2019 06:50:14 +0000 (GMT) Received: from localhost ([127.0.0.1]:35284 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1grdVl-0003em-Ug for patchwork@mira.cbaines.net; Thu, 07 Feb 2019 01:50:13 -0500 Received: from eggs.gnu.org ([209.51.188.92]:54658) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1grdVg-0003bj-HJ for guix-patches@gnu.org; Thu, 07 Feb 2019 01:50:09 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1grdVe-0002zu-9A for guix-patches@gnu.org; Thu, 07 Feb 2019 01:50:08 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:37190) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1grdVa-0002y7-Tr for guix-patches@gnu.org; Thu, 07 Feb 2019 01:50:04 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1grdVa-0003hm-Kz for guix-patches@gnu.org; Thu, 07 Feb 2019 01:50:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#34361] [PATCH 2/4] gnu: Add ocaml-bindlib. References: <87lg2sf6az.fsf@gmail.com> In-Reply-To: <87lg2sf6az.fsf@gmail.com> Resent-From: Gabriel Hondet Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Thu, 07 Feb 2019 06:50:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 34361 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 34361@debbugs.gnu.org Received: via spool by 34361-submit@debbugs.gnu.org id=B34361.154952215014166 (code B ref 34361); Thu, 07 Feb 2019 06:50:02 +0000 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 Date: Fri, 1 Feb 2019 20:31:34 +0100 Message-ID: <87k1icf603.fsf@gmail.com> MIME-Version: 1.0 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches * 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 dedukti files.") "Part of the Jane Street's PPX rewriters collection.") (license license:expat))) +(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 ASTs +for programming languages, but also for manipulating terms of the λ-calculus +or quantified formulas.") + (license license:gpl3+))) + (define-public ocaml-earley (package (name "ocaml-earley") From patchwork Fri Feb 1 19:50:25 2019 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Gabriel Hondet X-Patchwork-Id: 971 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 6327B16B45; Thu, 7 Feb 2019 07:05:25 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM, T_DKIM_INVALID,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id BB36E16B13 for ; Thu, 7 Feb 2019 07:05:23 +0000 (GMT) Received: from localhost ([127.0.0.1]:35392 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1grdkR-0005wr-2J for patchwork@mira.cbaines.net; Thu, 07 Feb 2019 02:05:23 -0500 Received: from eggs.gnu.org ([209.51.188.92]:57000) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1grdkE-0005vR-Po for guix-patches@gnu.org; Thu, 07 Feb 2019 02:05:11 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1grdk8-0003aL-Pu for guix-patches@gnu.org; Thu, 07 Feb 2019 02:05:10 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:37198) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1grdk8-0003a7-Hy for guix-patches@gnu.org; Thu, 07 Feb 2019 02:05:04 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1grdk6-00044r-Mt for guix-patches@gnu.org; Thu, 07 Feb 2019 02:05:04 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#34361] [PATCH 3/4] gnu: Add ocaml-timed. References: <87lg2sf6az.fsf@gmail.com> In-Reply-To: <87lg2sf6az.fsf@gmail.com> Resent-From: Gabriel Hondet Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Thu, 07 Feb 2019 07:05:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 34361 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 34361@debbugs.gnu.org Received: via spool by 34361-submit@debbugs.gnu.org id=B34361.154952307915633 (code B ref 34361); Thu, 07 Feb 2019 07:05:02 +0000 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 Date: Fri, 1 Feb 2019 20:50:25 +0100 Message-ID: <87imxwf5a9.fsf@gmail.com> MIME-Version: 1.0 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches * 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 the definition of parsers inside the language. There is also support for writing OCaml syntax extensions in a camlp4 style.") (license license:cecill-b))) +(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 provides +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. Note +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") -- 2.20.1 From patchwork Sat Feb 2 10:51:25 2019 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Patchwork-Submitter: Gabriel Hondet X-Patchwork-Id: 972 Return-Path: X-Original-To: patchwork@mira.cbaines.net Delivered-To: patchwork@mira.cbaines.net Received: by mira.cbaines.net (Postfix, from userid 113) id 54C4516B45; Thu, 7 Feb 2019 07:06:09 +0000 (GMT) X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on mira.cbaines.net X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM, T_DKIM_INVALID,URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.0 Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) by mira.cbaines.net (Postfix) with ESMTP id DCAC116ADC for ; Thu, 7 Feb 2019 07:06:08 +0000 (GMT) Received: from localhost ([127.0.0.1]:35402 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1grdlA-0006CN-Ho for patchwork@mira.cbaines.net; Thu, 07 Feb 2019 02:06:08 -0500 Received: from eggs.gnu.org ([209.51.188.92]:57195) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1grdl5-0006C2-By for guix-patches@gnu.org; Thu, 07 Feb 2019 02:06:04 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1grdl4-0004Dq-E6 for guix-patches@gnu.org; Thu, 07 Feb 2019 02:06:03 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:37202) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1grdl4-0004Dh-52 for guix-patches@gnu.org; Thu, 07 Feb 2019 02:06:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1grdl3-00046g-Sp for guix-patches@gnu.org; Thu, 07 Feb 2019 02:06:01 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#34361] [PATCH 4/4] gnu: Add lambdapi. References: <87lg2sf6az.fsf@gmail.com> In-Reply-To: <87lg2sf6az.fsf@gmail.com> Resent-From: Gabriel Hondet Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Thu, 07 Feb 2019 07:06:01 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 34361 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: 34361@debbugs.gnu.org Received: via spool by 34361-submit@debbugs.gnu.org id=B34361.154952314415762 (code B ref 34361); Thu, 07 Feb 2019 07:06:01 +0000 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 Date: Sat, 2 Feb 2019 11:51:25 +0100 Message-ID: <87h8dgf58h.fsf@gmail.com> MIME-Version: 1.0 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 209.51.188.43 X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+patchwork=mira.cbaines.net@gnu.org Sender: "Guix-patches" X-getmail-retrieved-from-mailbox: Patches * 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 (Pervasives module). However, it is less efficient than the first one.") (license license:expat))) +(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 λΠ-calculus 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")