Skip to content
Snippets Groups Projects
Select Git revision
  • 99-add-let-binder
  • main default protected
  • 108-opaque-traces
  • 115-improve-ci-by-using-nix
  • 106-logsem-seminar-talk
  • 109-feat-tilleul-add-vscode-support
  • 111-non-dependent-products-optimisation
  • 81-bug-parser-no-error-when-defining-a-declaration-with-the-same-name-as-a-definition
  • 110-unhandled-lsp-requests-declared-as-capabilities-in-tilleul
  • 107-parser-simplification
  • 95-replace-succ-with-an-add-constructor-on-level
  • 102-add-match-syntax
  • 105-specialize-traces
  • 66-implement-bidirectional-type-checking
  • 104-implement-normalisation-by-evaluation
  • 98-parsing-building-allow-left-arguments
  • 91-add-examples-as-a-test-suite-for-the-pipeline
  • 52-add-better-tab-behavior-for-proost-toplevel
  • 103-normal-form-memoization
  • 97-preparations-for-v0-3-0
  • v0.3.0
  • v0.2.0
  • 0.1.0
23 results
Compare History
v-lafeychine's avatar
Resolve "proost fonctionality and UI" ✨️
v-lafeychine authored 
Closes #22 et #7 🐔️👍️
Approved-by: default avataraalbert <augustin.albert@bleu-azure.fr>
Approved-by: default avatarbelazy <aarthuur01@gmail.com>
Approved-by: default avatarloutr <loutr@crans.org>

🦀️🍰🦀️🍰🦀️🍰

* Chore : add test

* Fix : shift vars when binding lambda-abstractions

* fix(kernel): some tests were wrong

* HOT fix(kernel): command definition fixed

* HOT fix(parser): fix parenthesis

* HOT fix(parser): order of fun

* feat(parser): resolve threads

* chore(parser): Merge renamed_rules on Error

* chore(command): Merge Define/DefineCheckType + Add tests

* chore(parser): apply suggestions

* feat(parser): add location conversion from pest to proost's kernel

* Apply 1 suggestion(s) to 1 file(s)

* fix(all): resolve thread and change Pos for Loc (range position) +
conversion from position to range position in parser

* fix(all): resolve threads

* feat(kernel): Add tests in commands.rs

* feat(parser, error): add new errors for parser, pos struct, first use of pos and pretty print of parsing errors

* feat(parser, kernel): new kernel error: cannot parse

* feat(proost): new ui v1

* feat(proost): new interface!

* feat(parser, kernel): change grammar and pretty printing
36190e2a
Name Last commit Last update
docs
kernel
parser
proost
.gitattributes
.gitignore
.gitlab-ci.yml
.gitlab-cov.xsl
Cargo.lock
Cargo.toml
LICENSE.md
README.md
flake.lock
flake.nix
README.md

Proost

A simple proof assistant written in Rust.

Development environment

With nix installed, simply type nix develop. This provides an environment with all the necessary tools, including clippy and rustfmt. There, it is possible to run the usual cargo build and so on.

Please consider the syntax nix develop --profile <a-file-of-your-choosing>, which will prevent the garbage collection of the development dependencies.

Build and install

With nix installed, type nix build to perform a build and have it in the nix store. One can also type nix profile install in the repo to install proost to your profile and use it everywhere!