[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[bug#34361] [PATCH 4/4] gnu: Add lambdapi.
From: |
Julien Lepiller |
Subject: |
[bug#34361] [PATCH 4/4] gnu: Add lambdapi. |
Date: |
Wed, 13 Feb 2019 22:53:21 +0100 |
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