* [bug#34361] [PATCH 1/4] gnu: Add ocaml-earley.
@ 2019-02-01 19:20 Gabriel Hondet
2019-02-01 19:31 ` [bug#34361] [PATCH 2/4] gnu: Add ocaml-bindlib Gabriel Hondet
` (3 more replies)
0 siblings, 4 replies; 6+ messages in thread
From: Gabriel Hondet @ 2019-02-01 19:20 UTC (permalink / raw)
To: 34361
[-- 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 --]
^ permalink raw reply related [flat|nested] 6+ messages in thread
* [bug#34361] [PATCH 2/4] gnu: Add ocaml-bindlib.
2019-02-01 19:20 [bug#34361] [PATCH 1/4] gnu: Add ocaml-earley Gabriel Hondet
@ 2019-02-01 19:31 ` Gabriel Hondet
2019-02-01 19:50 ` [bug#34361] [PATCH 3/4] gnu: Add ocaml-timed Gabriel Hondet
` (2 subsequent siblings)
3 siblings, 0 replies; 6+ messages in thread
From: Gabriel Hondet @ 2019-02-01 19:31 UTC (permalink / raw)
To: 34361
[-- 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 --]
^ permalink raw reply related [flat|nested] 6+ messages in thread
* [bug#34361] [PATCH 3/4] gnu: Add ocaml-timed.
2019-02-01 19:20 [bug#34361] [PATCH 1/4] gnu: Add ocaml-earley Gabriel Hondet
2019-02-01 19:31 ` [bug#34361] [PATCH 2/4] gnu: Add ocaml-bindlib Gabriel Hondet
@ 2019-02-01 19:50 ` Gabriel Hondet
2019-02-02 10:51 ` [bug#34361] [PATCH 4/4] gnu: Add lambdapi Gabriel Hondet
2019-05-04 19:14 ` bug#34361: closing lambdapi Gabriel Hondet
3 siblings, 0 replies; 6+ messages in thread
From: Gabriel Hondet @ 2019-02-01 19:50 UTC (permalink / raw)
To: 34361
[-- 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 --]
^ permalink raw reply related [flat|nested] 6+ messages in thread
* [bug#34361] [PATCH 4/4] gnu: Add lambdapi.
2019-02-01 19:20 [bug#34361] [PATCH 1/4] gnu: Add ocaml-earley Gabriel Hondet
2019-02-01 19:31 ` [bug#34361] [PATCH 2/4] gnu: Add ocaml-bindlib Gabriel Hondet
2019-02-01 19:50 ` [bug#34361] [PATCH 3/4] gnu: Add ocaml-timed Gabriel Hondet
@ 2019-02-02 10:51 ` Gabriel Hondet
2019-02-13 21:53 ` Julien Lepiller
2019-05-04 19:14 ` bug#34361: closing lambdapi Gabriel Hondet
3 siblings, 1 reply; 6+ messages in thread
From: Gabriel Hondet @ 2019-02-02 10:51 UTC (permalink / raw)
To: 34361
[-- 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 --]
^ permalink raw reply related [flat|nested] 6+ messages in thread
* [bug#34361] [PATCH 4/4] gnu: Add lambdapi.
2019-02-02 10:51 ` [bug#34361] [PATCH 4/4] gnu: Add lambdapi Gabriel Hondet
@ 2019-02-13 21:53 ` Julien Lepiller
0 siblings, 0 replies; 6+ messages in thread
From: Julien Lepiller @ 2019-02-13 21:53 UTC (permalink / raw)
To: 34361
[-- 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 --]
^ permalink raw reply [flat|nested] 6+ messages in thread
* bug#34361: closing lambdapi
2019-02-01 19:20 [bug#34361] [PATCH 1/4] gnu: Add ocaml-earley Gabriel Hondet
` (2 preceding siblings ...)
2019-02-02 10:51 ` [bug#34361] [PATCH 4/4] gnu: Add lambdapi Gabriel Hondet
@ 2019-05-04 19:14 ` Gabriel Hondet
3 siblings, 0 replies; 6+ messages in thread
From: Gabriel Hondet @ 2019-05-04 19:14 UTC (permalink / raw)
To: 34361-done
[-- 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 --]
^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2019-05-04 19:15 UTC | newest]
Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-02-01 19:20 [bug#34361] [PATCH 1/4] gnu: Add ocaml-earley Gabriel Hondet
2019-02-01 19:31 ` [bug#34361] [PATCH 2/4] gnu: Add ocaml-bindlib Gabriel Hondet
2019-02-01 19:50 ` [bug#34361] [PATCH 3/4] gnu: Add ocaml-timed Gabriel Hondet
2019-02-02 10:51 ` [bug#34361] [PATCH 4/4] gnu: Add lambdapi Gabriel Hondet
2019-02-13 21:53 ` Julien Lepiller
2019-05-04 19:14 ` bug#34361: closing lambdapi Gabriel Hondet
Code repositories for project(s) associated with this public inbox
https://git.savannah.gnu.org/cgit/guix.git
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).