lambdapi.opam

synopsis: "Proof assistant based on the λΠ-calculus modulo rewriting"
description:
"""
Proof assistant based on the λΠ-calculus modulo rewriting,
mostly compatible with Dedukti.

This package contains both the `lambdapi` proof assistant and the `lp-lsp`
Language Server Protocol helper for IDEs to check lambdapi files.
"""
opam-version: "2.0"
maintainer: "dedukti-dev@inria.fr"
bug-reports: "https://github.com/Deducteam/lambdapi/issues"
homepage: "https://github.com/Deducteam/lambdapi"
dev-repo: "git+https://github.com/Deducteam/lambdapi.git"
authors: [
  "Rodolphe Lepigre <lepigre@mpi-sws.org>"
  "Frédéric Blanqui <frederic.blanqui@inria.fr>"
  "Emilio Jesús Gallego Arias <e@x80.org>" ]
license: "CeCILL 2.1"
doc: "https://deducteam.github.io/lambdapi/"

depends: [
  "ocaml"        { >= "4.05.0" }
  "dune"         { >= "1.3.0"  }
  "menhir"
  "bindlib"      { >= "5.0.1" }
  "earley"       { = "2.0.0" }
  "timed"        { = "1.0"   }
  "why3"         { >= "1.3.1" }
  "yojson"       { >= "1.6.0" }
  "cmdliner"     { >= "1.0.3" }
  "stdlib-shims"
]

post-messages: [
  "To use the Emacs mode, add the following line to ~/.emacs.d/init.el,
or ~/.emacs:\n
\t(load \"lambdapi-site-file\")\n"
]

build: [
  [ "dune" "subst" ]
  [ "dune" "build" "-p" name "-j" jobs ]
]