[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[bug#34361] [PATCH 4/4] gnu: Add lambdapi.
From: |
Gabriel Hondet |
Subject: |
[bug#34361] [PATCH 4/4] gnu: Add lambdapi. |
Date: |
Sat, 2 Feb 2019 11:51:25 +0100 |
User-agent: |
mu4e 1.0; emacs 26.1 |
* 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")
--
2.20.1
signature.asc
Description: PGP signature