| Message ID | 87h8dgf58h.fsf@gmail.com |
|---|---|
| State | Accepted |
| Headers | show |
| Series | [bug#34361,1/4] gnu: Add ocaml-earley. | expand |
| Context | Check | Description |
|---|---|---|
| cbaines/applying patch | fail | Apply failed |
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
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")