| Commit message (Collapse) | Author | Age | Files | Lines |
|\
| |
| | |
chore(ci): move Lean CI under Nix
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
As it often happens, the Lean CI under Ubuntu is broken:
https://github.com/AeneasVerif/aeneas/actions/runs/8814059410/job/24193132680?pr=135
and blocking PRs.
Lean doesn't work nicely under the Nix sandbox, but in a CI context, we
can impurely run scripts and use Nix to get our dependencies, e.g. curl
or elan in this case.
It is still more reliable than letting Ubuntu or GitHub Actions figure
out their signing for their APT repositories apparently.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
|\ \
| |/
|/| |
compiler: add `core::option::Option::{take, is_none}` and `core::mem::swap` support
|
| | |
|
| | |
|
| | |
|
| |\
| |/
|/| |
|
|\ \
| | |
| | | |
feat(backends/lean): scalars form a linear order
|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
More than c1c33de8, actually, scalars form a linear order with a
decidable ≤ operation which is induced by the integer (Z) model.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
|\ \ \
| | | |
| | | | |
ci: check code formatting and forbid warnings
|
| | | |
| | | |
| | | | |
Co-authored-by: Son HO <hosonmarc@gmail.com>
|
| | | | |
|
| | | | |
|
|\ \ \ \
| |/ / /
|/| | | |
ci: avoid running duplicate jobs
|
|/ / / |
|
|\ \ \
| | | |
| | | | |
Fix an issue in the loops fixed point
|
| | | | |
|
|/ / / |
|
|\ \ \
| | | |
| | | | |
Ensure we regenerate files properly in CI
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
Files that weren't regenerated were marked as not
automatically-generated.
|
|\ \ \ \
| | |/ /
| |/| | |
fix(backends/lean): add a significant amount of keywords
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Taken from
https://github.com/leanprover/lean4/blob/master/doc/latex/lstlean.tex#L33
and
https://github.com/leanprover/lean4/blob/master/doc/latex/lstlean.tex#L36-L43.
This will not extract the tactics.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Taken from
https://github.com/leanprover/lean4/blob/master/doc/latex/lstlean.tex#L12
and sorted.
Tactics are ignored.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
OCD. :D
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| | | |
| | | |
| | | |
| | | | |
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
`as` is a reserved keyword and cannot be used as a variable name.
Fixes #139.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
|\ \ \ \
| |_|/ /
|/| | | |
|
| | | | |
|
|/ / / |
|
|\ \ \ |
|
| |/ /
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Not all Nix users can make use of Flakes.
This adds the compatibility for non-Flakes users.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
|\ \ \
| | | |
| | | | |
Run sanity checks in CI only
|
| | | | |
|
|\ \ \ \
| |_|/ /
|/| | | |
Bump charon
|
|/ / / |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
On the long run, all backends will not have equivalent or equal support
for extraction.
This introduces a function to filter out some Lean-only definitions in
our various arrays of core functions.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Our backend already have support for `isNone`, we just map it and filter
out passing the actual type as it can be inferred via implicit types.
Other backends than Lean are not done in this commit.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
In the pure functional model, `swap` is mostly about borrow checking and
should simplify to the pure swap in our backends.
Other backends than Lean are not done in this commit.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
| |/
|/|
| |
| |
| |
| |
| |
| | |
`take` in a pure functional model is the identity function and
everything related to borrow checking is handled by the forward/backward
mechanism.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
|\ \
| |/
|/| |
lean: scalars form a preorder
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Via the canonical injection, we can easily define an induced preorder on
scalars and inherit all nice properties.
It's useful to reason on specific scalar preorders w.r.t. Ordering, see
the binary search tree verification example.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
|
|\ \
| |/
|/| |
Fix CI
|
|/ |
|
|\
| |
| | |
Add more definitions to the Lean library
|
| | |
|
| | |
|
|/ |
|
|\
| |
| | |
Add builtins for some checked ops for the Lean backend
|
| | |
|