* 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")
-- 
2.20.1