lambdapi

Proof assistant for the λΠ-calculus modulo rewriting
README

>>>>> User Manual <<<<<

Issues can be reported on the following
issue tracker.

Questions can be asked on the following
forum.

Examples of developments made with Lambdapi:

Operating systems

Lambdapi requires a Unix-like system. It should work on Linux as well as on
MacOS. It might be possible to make it work on Windows too with Cygwin or
"bash on Windows".

Installation via Opam

opam install lambdapi

The installation gives you:

  • a main executable lambdapi in your PATH

  • OCaml libraries

  • a lambdapi mode for vim

  • a lambdapi mode for emacs

The VSCode extension is available on the Marketplace.

To browse the source code documentation, you can do:

opam install odig
odig doc lambdapi

To install Lambdapi libraries, see the opam-lambdapi-repository.

Compilation from the sources

You can get the sources using git as follows:

git clone https://github.com/Deducteam/lambdapi.git

Dependencies are described in lambdapi.opam. The command why3 config detect
must be run to make Why3 know the available provers.

Using Opam, a suitable OCaml environment can be setup as follows:

opam install dune bindlib timed sedlex menhir pratter yojson cmdliner why3 alcotest alt-ergo odoc
why3 config detect

To compile Lambdapi, just run the command make in the source directory.
This produces the _build/install/default/bin/lambdapi binary.
Use the --help option for more information. Other make targets are:

make                        # Build lambdapi
make doc                    # Build the user documentation (avalaible on readthedocs)
make odoc                   # Build the developer documentation
make install                # Install lambdapi
make install_emacs          # Install emacs mode
make install_vscode         # Install vscode extension
make install_vim            # Install vim support

You can run lambdapi without installing it with dune exec -- lambdapi.

For running tests, one also needs
alcotest and
alt-ergo.

For building the source code documentation, one needs
odoc. The starting file of the source
code html documentation is
_build/default/_doc/_html/lambdapi/index.html.

For building the User Manual, see doc/README.md.

The following commands can be used to clean up the repository:

make clean     # Removes files generated by OCaml.
make distclean # Same as clean, but also removes library checking files.
make fullclean # Same as distclean, but also removes downloaded libraries.
Install
Published
18 Mar 2022
Authors
Sources
lambdapi-2.2.0.tbz
sha256=920de48ec6c2c3223b6b93879bb65d07ea24aa27f7f7176b3de16e5e467b9939
sha512=135f132730825adeb084669222e68bc999de97b12378fae6abcd9f91ae13093eab29fa49c854adb28d064d52c9890c0f5c8ff9d47a9916f66fe5e0fba3479759
Dependencies
odoc
with-doc
stdlib-shims
>= "0.1.0"
cmdliner
>= "1.1.0"
yojson
>= "1.6.0"
why3
>= "1.4" & < "1.5~"
pratter
>= "1.2" & < "2.0.0"
timed
>= "1.0"
bindlib
>= "5.0.1"
alt-ergo
with-test
alcotest
with-test
sedlex
>= "2.2"
menhir
>= "20200624"
ocaml
>= "4.08.0"
dune
>= "2.7"
Reverse Dependencies