Skip to content
master
Switch branches/tags
Code

Latest commit

- Add tests on product matching
- Fixed scoping of product in LHS
- Wildcard created during tree compilation are the most general ones, any free  variable may appear.
- Updated documentation of decision trees
1e823f3

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
 
 
 
 
 
 
src
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Lambdapi, a proof assistant based on the λΠ-calculus modulo rewriting Gitter Matrix

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

Lambdapi is under active development. A new version of the lambdapi Opam package will be released soon, when the development will have reached a more stable point. For now, we advise you to pin the development repository to get the latest development version:

opam pin add lambdapi https://github.com/Deducteam/lambdapi.git
opam install lambdapi # install emacs and vim support as well

For installing the VSCode extension, you need to get the sources (see below).

The installation gives you:

  • a main executable named lambdapi in your PATH
  • an OCaml library called lambdapi.core (system internals)
  • an OCaml library called lambdapi.pure (pure interface)
  • an OCaml library called lambdapi.lsp (LSP server)
  • a lambdapi mode for Vim (optional)
  • a lambdapi mode for emacs (optional)

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. For running tests, one also needs alcotest and alt-ergo. For building the source code documentation, one needs odoc. For building the User Manual, see docs/README.md.

Note on Why3: 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 switch 4.11.1
opam install dune bindlib timed 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
make vscode                 # Install vscode extension

Note: you can run lambdapi without installing it with dune exec -- lambdapi.

Note: the starting file of the source code html documentation is _build/default/_doc/_html/lambdapi/index.html.

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.