GNU bug report logs -
#34361
[PATCH 1/4] gnu: Add ocaml-earley.
Previous Next
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.
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):
[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):
[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):
[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):
[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):
[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):
[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.