package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=ba73f288e435130293408bd44732f1dfc5ec8a8db91c7453c9baf9c740095829
sha512=f88bb92fdb8aee8add60588673040fac012b2eab17c2a1d529c4b7c795cf0e1a9168122dc19889f04a31bda2bb2cf820237cbbe7e319121618aba3d134381756
README.md.html
Lambdapi, a proof assistant based on the λΠ-calculus modulo rewriting
>>>>>
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 yourPATH
OCaml libraries
a
lambdapi
mode forvim
a
lambdapi
mode foremacs
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_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.