A simple proof assistant written in Rust.
The specification of the project may be found here, and the user manual here. The API documentation can be found by clicking on the corresponding badge below the project name.
To install proost with nix installed, simply type:
nix profile install git+ssh://git@gitlab.crans.org/loutr/proost.git?ref=mainOne may also install it from our GitHub mirror:
nix profile install github:proost-assistant/proostA toplevel instance can then be launched with proost. Alternatively, replace
profile install with run to give the program a go without installing it.
Without nix installed, git clone the project and, with Rust and
cargo properly setup to an
appropriate version (either through your package manager or
rustup), do cargo run --release.
Type nix develop. This provides an environment with all the necessary tools,
including cargo (with clippy, rustfmt) and rust-analyzer. Then, use your
regular cargo commands.
Please consider the syntax nix develop --profile <a-file-of-your-choosing>,
which will prevent the garbage collection of the development dependencies as
long as the given file lives.
The project is organised as such:
- the crate
kernelprovides an interface for building and manipulating terms, as well as type inference and type checking functions; - the crate
elaborationdefinesBuildertypes, which are high-level representations of terms that can be transformed into concrete terms; - the crate
parserprovides parsing functions which returnBuilderandCommandobjects, to be used by any client; - the crate
proostprovides a toplevel interface for end-users that can be used to manipulate terms and query the kernel. It provides partial auto-completion, some color highlighting and other readline-like features; - the crate
tilleulis a WIP implementation of the Language Server Protocol for Madeleine, the language of Proost.
graph TD;
kernel-->elaboration;
elaboration-->parser;
kernel-->tilleul;
parser-->tilleul;
parser-->proost;
kernel-->proost;