GNU bug report logs - #34361
[PATCH 1/4] gnu: Add ocaml-earley.

Previous Next

Package: guix-patches;

Reported by: Gabriel Hondet <gabrielhondet <at> gmail.com>

Date: Thu, 7 Feb 2019 06:44:02 UTC

Severity: normal

Tags: patch

Done: Gabriel Hondet <gabrielhondet <at> gmail.com>

Bug is archived. No further changes may be made.

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 34361 in the body.
You can then email your comments to 34361 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

View this report as an mbox folder, status mbox, maintainer mbox


Report forwarded to guix-patches <at> gnu.org:
bug#34361; Package guix-patches. (Thu, 07 Feb 2019 06:44:02 GMT) Full text and rfc822 format available.

Acknowledgement sent to Gabriel Hondet <gabrielhondet <at> gmail.com>:
New bug report received and forwarded. Copy sent to guix-patches <at> gnu.org. (Thu, 07 Feb 2019 06:44:02 GMT) Full text and rfc822 format available.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

From: Gabriel Hondet <gabrielhondet <at> gmail.com>
To: guix-patches <at> gnu.org
Subject: [PATCH 1/4] gnu: Add ocaml-earley.
Date: Fri, 1 Feb 2019 20:20:54 +0100
[Message part 1 (text/plain, inline)]
* 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")
-- 
2.20.1
[signature.asc (application/pgp-signature, inline)]

Information forwarded to guix-patches <at> gnu.org:
bug#34361; Package guix-patches. (Thu, 07 Feb 2019 06:50:02 GMT) Full text and rfc822 format available.

Message #8 received at 34361 <at> debbugs.gnu.org (full text, mbox):

From: Gabriel Hondet <gabrielhondet <at> gmail.com>
To: 34361 <at> debbugs.gnu.org
Subject: [PATCH 2/4] gnu: Add ocaml-bindlib.
Date: Fri, 1 Feb 2019 20:31:34 +0100
[Message part 1 (text/plain, inline)]
* 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")
-- 
2.20.1
[signature.asc (application/pgp-signature, inline)]

Information forwarded to guix-patches <at> gnu.org:
bug#34361; Package guix-patches. (Thu, 07 Feb 2019 07:05:02 GMT) Full text and rfc822 format available.

Message #11 received at 34361 <at> debbugs.gnu.org (full text, mbox):

From: Gabriel Hondet <gabrielhondet <at> gmail.com>
To: 34361 <at> debbugs.gnu.org
Subject: [PATCH 3/4] gnu: Add ocaml-timed.
Date: Fri, 1 Feb 2019 20:50:25 +0100
[Message part 1 (text/plain, inline)]
* 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
[signature.asc (application/pgp-signature, inline)]

Information forwarded to guix-patches <at> gnu.org:
bug#34361; Package guix-patches. (Thu, 07 Feb 2019 07:06:01 GMT) Full text and rfc822 format available.

Message #14 received at 34361 <at> debbugs.gnu.org (full text, mbox):

From: Gabriel Hondet <gabrielhondet <at> gmail.com>
To: 34361 <at> debbugs.gnu.org
Subject: [PATCH 4/4] gnu: Add lambdapi.
Date: Sat, 2 Feb 2019 11:51:25 +0100
[Message part 1 (text/plain, inline)]
* 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")
-- 
2.20.1
[signature.asc (application/pgp-signature, inline)]

Information forwarded to guix-patches <at> gnu.org:
bug#34361; Package guix-patches. (Wed, 13 Feb 2019 21:54:01 GMT) Full text and rfc822 format available.

Message #17 received at 34361 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: 34361 <at> debbugs.gnu.org
Subject: Re: [bug#34361] [PATCH 4/4] gnu: Add lambdapi.
Date: Wed, 13 Feb 2019 22:53:21 +0100
[Message part 1 (text/plain, inline)]
Le Sat, 2 Feb 2019 11:51:25 +0100,
Gabriel Hondet <gabrielhondet <at> gmail.com> a écrit :

> * 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")

This package builds fine, but in the end, here is what I get installed:

Installing /gnu/store/1dh8ni590ai2nbbqrxxvgcfnlgwslsi3-lambdapi-1.0/lib/ocaml/site-lib/lambdapi/META
Installing /gnu/store/1dh8ni590ai2nbbqrxxvgcfnlgwslsi3-lambdapi-1.0/lib/ocaml/site-lib/lambdapi/opam
Installing /gnu/store/1dh8ni590ai2nbbqrxxvgcfnlgwslsi3-lambdapi-1.0/doc/lambdapi/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
[Message part 2 (application/pgp-signature, inline)]

Reply sent to Gabriel Hondet <gabrielhondet <at> gmail.com>:
You have taken responsibility. (Sat, 04 May 2019 19:15:03 GMT) Full text and rfc822 format available.

Notification sent to Gabriel Hondet <gabrielhondet <at> gmail.com>:
bug acknowledged by developer. (Sat, 04 May 2019 19:15:03 GMT) Full text and rfc822 format available.

Message #22 received at 34361-done <at> debbugs.gnu.org (full text, mbox):

From: Gabriel Hondet <gabrielhondet <at> gmail.com>
To: 34361-done <at> debbugs.gnu.org
Subject: closing lambdapi
Date: Sat, 04 May 2019 21:14:31 +0200
[Message part 1 (text/plain, inline)]
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
[signature.asc (application/pgp-signature, inline)]

bug archived. Request was from Debbugs Internal Request <help-debbugs <at> gnu.org> to internal_control <at> debbugs.gnu.org. (Sun, 02 Jun 2019 11:24:04 GMT) Full text and rfc822 format available.

This bug report was last modified 4 years and 301 days ago.

Previous Next


GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.