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

[Julien Lepiller]

Le Sat, 2 Feb 2019 11:51:25 +0100,
Gabriel Hondet <address@hidden> 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
> address@hidden
> address@hidden
> +a logical framework,
> address@hidden
> +a tool for interoperability of proof systems,
> address@hidden
> +an interactive proof system,
> address@hidden
> +an experimental proof system.
> address@hidden 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

pgpyrgholZNmd.pgp
Description: Signature digitale OpenPGP