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

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

[Gabriel Hondet]

[-- Attachment #1: Type: text/plain, Size: 1673 bytes --]


* 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

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 832 bytes --]

[bug#34361] [PATCH 2/4] gnu: Add ocaml-bindlib.

[Gabriel Hondet]

[-- Attachment #1: Type: text/plain, Size: 1960 bytes --]


* 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

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 832 bytes --]

[bug#34361] [PATCH 3/4] gnu: Add ocaml-timed.

[Gabriel Hondet]

[-- Attachment #1: Type: text/plain, Size: 2434 bytes --]


* 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

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 832 bytes --]

[bug#34361] [PATCH 4/4] gnu: Add lambdapi.

[Gabriel Hondet]

[-- Attachment #1: Type: text/plain, Size: 2753 bytes --]


* 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

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 832 bytes --]

[bug#34361] [PATCH 4/4] gnu: Add lambdapi.

[Julien Lepiller]

[-- Attachment #1: Type: text/plain, Size: 3561 bytes --]

Le Sat, 2 Feb 2019 11:51:25 +0100,
Gabriel Hondet <gabrielhondet@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

[-- Attachment #2: Signature digitale OpenPGP --]
[-- Type: application/pgp-signature, Size: 833 bytes --]

bug#34361: closing lambdapi

[Gabriel Hondet]

[-- Attachment #1: Type: text/plain, Size: 146 bytes --]

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

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 832 bytes --]