GNU bug report logs - #34361
[PATCH 1/4] gnu: Add ocaml-earley.

Previous Next

Full log

Message #17 received at 34361 <at> debbugs.gnu.org (full text, mbox):

From: Julien Lepiller <julien <at> lepiller.eu>
To: 34361 <at> debbugs.gnu.org
Subject: Re: [bug#34361] [PATCH 4/4] gnu: Add lambdapi.
Date: Wed, 13 Feb 2019 22:53:21 +0100

[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)]

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.