* [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).