| Commit message (Expand) | Author | Age | Files | Lines |
... | |
| * | Update the backend and ExtractBuiltin.ml | Son Ho | 2024-04-25 | 4 | -2/+18 |
| * | Merge branch 'main' into core-option-unwrap | Son Ho | 2024-04-25 | 37 | -238/+1491 |
| |\ |
|
| * | | Fix a couple of tests | Zyad Hassan | 2024-04-24 | 4 | -13/+4 |
| * | | Update tests | Zyad Hassan | 2024-04-24 | 7 | -44/+0 |
| * | | Add core::option::unwrap builtin | Zyad Hassan | 2024-04-24 | 4 | -5/+15 |
* | | | Merge pull request #158 from RaitoBezarius/lean-ci-under-nix | Son HO | 2024-04-26 | 2 | -14/+6 |
|\ \ \
| |_|/
|/| | |
|
| * | | chore(ci): move Lean CI under Nix | Ryan Lahfa | 2024-04-24 | 2 | -14/+6 |
| |/ |
|
* | | Merge pull request #135 from RaitoBezarius/option-take | Son HO | 2024-04-25 | 36 | -258/+1489 |
|\ \
| |/
|/| |
|
| * | Regenerate the Primitives files | Son Ho | 2024-04-25 | 13 | -0/+975 |
| * | Update the flake.lock | Son Ho | 2024-04-25 | 1 | -15/+15 |
| * | Update the tests for External | Son Ho | 2024-04-25 | 20 | -237/+470 |
| * | Merge branch 'main' into option-take | Son Ho | 2024-04-25 | 29 | -605/+523 |
| |\
| |/
|/| |
|
* | | Merge pull request #156 from RaitoBezarius/orders | Son HO | 2024-04-23 | 1 | -0/+15 |
|\ \ |
|
| * | | feat(backends/lean): scalars form a linear order | Ryan Lahfa | 2024-04-23 | 1 | -0/+15 |
* | | | Merge pull request #154 from AeneasVerif/ci-fmt | Son HO | 2024-04-23 | 3 | -2/+23 |
|\ \ \ |
|
| * | | | Typo | Guillaume Boisseau | 2024-04-23 | 1 | -1/+1 |
| * | | | ci: Forbid compilation warnings | Nadrieril | 2024-04-22 | 1 | -0/+1 |
| * | | | ci: check code formatting | Nadrieril | 2024-04-22 | 3 | -2/+22 |
* | | | | Merge pull request #155 from AeneasVerif/dedup-ci | Son HO | 2024-04-23 | 1 | -0/+22 |
|\ \ \ \
| |/ / /
|/| | | |
|
| * | | | ci: avoid running duplicate jobs | Nadrieril | 2024-04-22 | 1 | -0/+22 |
|/ / / |
|
* | | | Merge pull request #151 from AeneasVerif/son/fix-loops2 | Son HO | 2024-04-22 | 6 | -35/+80 |
|\ \ \ |
|
| * | | | Fix an issue when joining a symbolic value with bottom | Son Ho | 2024-04-22 | 2 | -11/+33 |
| * | | | Reformat some files | Son Ho | 2024-04-22 | 5 | -24/+47 |
|/ / / |
|
* | | | Merge pull request #132 from AeneasVerif/regen-tests | Son HO | 2024-04-19 | 10 | -15/+10 |
|\ \ \ |
|
| * | | | Address review comments | Nadrieril | 2024-04-18 | 18 | -2/+20 |
| * | | | Ensure we regenerate files properly in CI | Nadrieril | 2024-04-18 | 27 | -32/+9 |
* | | | | Merge pull request #146 from RaitoBezarius/main | Son HO | 2024-04-19 | 1 | -3/+69 |
|\ \ \ \
| | |/ /
| |/| | |
|
| * | | | fix(backends/lean): extract more keywords from `lstlean.tex` | Ryan Lahfa | 2024-04-18 | 1 | -0/+2 |
| * | | | fix(backends/lean): extract more keywords from `lstlean.latex` | Ryan Lahfa | 2024-04-18 | 1 | -0/+62 |
| * | | | chore(backends/lean): sort the keyword list | Ryan Lahfa | 2024-04-17 | 1 | -4/+4 |
| * | | | fix(backends/lean): `from` is a keyword | Ryan Lahfa | 2024-04-17 | 1 | -0/+1 |
| * | | | fix(backends/lean): `as` is a keyword | Ryan Lahfa | 2024-04-17 | 1 | -0/+1 |
* | | | | Merge pull request #116 from AeneasVerif/item_meta | Guillaume Boisseau | 2024-04-18 | 11 | -85/+101 |
|\ \ \ \
| |_|/ /
|/| | | |
|
| * | | | Update charon pin | Nadrieril | 2024-04-18 | 2 | -5/+20 |
| * | | | item_meta | Nadrieril | 2024-04-18 | 9 | -80/+81 |
|/ / / |
|
* | | | Merge pull request #145 from RaitoBezarius/no-flakes | Guillaume Boisseau | 2024-04-18 | 4 | -1/+50 |
|\ \ \ |
|
| * | | | feat(nix): support non-Flakes users | Ryan Lahfa | 2024-04-17 | 4 | -1/+50 |
| |/ / |
|
* | | | Merge pull request #130 from AeneasVerif/fast-tests-outside-of-ci | Son HO | 2024-04-18 | 2 | -8/+4 |
|\ \ \ |
|
| * | | | Run sanity checks in CI only | Nadrieril | 2024-04-16 | 2 | -8/+4 |
* | | | | Merge pull request #147 from AeneasVerif/binops-simplification | Son HO | 2024-04-18 | 4 | -478/+171 |
|\ \ \ \
| |_|/ /
|/| | | |
|
| * | | | Bump charon | Nadrieril | 2024-04-17 | 4 | -478/+171 |
|/ / / |
|
| | * | compiler: introduce Lean-only translations | Ryan Lahfa | 2024-04-24 | 1 | -10/+25 |
| | * | compiler: map `core::option::Option::is_none` to `Option.isNone` | Ryan Lahfa | 2024-04-24 | 1 | -0/+4 |
| | * | compiler: map `core::mem::swap` to the pure swap | Ryan Lahfa | 2024-04-24 | 3 | -6/+4 |
| | * | compiler: map `core::option::Option::take` to identity function | Ryan Lahfa | 2024-04-17 | 2 | -0/+6 |
| |/
|/| |
|
* | | Merge pull request #126 from RaitoBezarius/scalar-preorders | Son HO | 2024-04-15 | 1 | -0/+10 |
|\ \
| |/
|/| |
|
| * | lean: scalars form a preorder | Ryan Lahfa | 2024-04-12 | 1 | -0/+10 |
* | | Merge pull request #127 from AeneasVerif/fix-ci | Son HO | 2024-04-15 | 2 | -2/+5 |
|\ \
| |/
|/| |
|
| * | Fix CI | Nadrieril | 2024-04-15 | 2 | -2/+5 |
|/ |
|
* | Merge pull request #124 from AeneasVerif/son/lean1 | Son HO | 2024-04-12 | 11 | -60/+674 |
|\ |
|