summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* Use eachDefaultSystem in flake.nix, update charon in flake.lockZack Grannan2024-04-261-1/+1
|
* Merge pull request #125 from zhassan-aws/core-option-unwrapSon HO2024-04-2636-89/+173
|\ | | | | Add `core::option::unwrap` builtin
| * Update the decreases clauses for the betreeSon Ho2024-04-262-8/+3
| |
| * Update the F* clauses for the betreeSon Ho2024-04-261-2/+1
| |
| * Update compiler/ExtractBuiltin.mlSon HO2024-04-261-1/+1
| | | | | | Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
| * Update a decreases clauseSon Ho2024-04-261-1/+7
| |
| * Regenerate and fix the testsSon Ho2024-04-2523-51/+140
| |
| * Update the backend and ExtractBuiltin.mlSon Ho2024-04-254-2/+18
| |
| * Merge branch 'main' into core-option-unwrapSon Ho2024-04-2537-238/+1491
| |\
| * | Fix a couple of testsZyad Hassan2024-04-244-13/+4
| | |
| * | Update testsZyad Hassan2024-04-247-44/+0
| | |
| * | Add core::option::unwrap builtinZyad Hassan2024-04-244-5/+15
| | |
* | | Merge pull request #158 from RaitoBezarius/lean-ci-under-nixSon HO2024-04-262-14/+6
|\ \ \ | |_|/ |/| | chore(ci): move Lean CI under Nix
| * | chore(ci): move Lean CI under NixRyan Lahfa2024-04-242-14/+6
| |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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>
* | Merge pull request #135 from RaitoBezarius/option-takeSon HO2024-04-2536-258/+1489
|\ \ | |/ |/| compiler: add `core::option::Option::{take, is_none}` and `core::mem::swap` support
| * Regenerate the Primitives filesSon Ho2024-04-2513-0/+975
| |
| * Update the flake.lockSon Ho2024-04-251-15/+15
| |
| * Update the tests for ExternalSon Ho2024-04-2520-237/+470
| |
| * Merge branch 'main' into option-takeSon Ho2024-04-2529-605/+523
| |\ | |/ |/|
* | Merge pull request #156 from RaitoBezarius/ordersSon HO2024-04-231-0/+15
|\ \ | | | | | | feat(backends/lean): scalars form a linear order
| * | feat(backends/lean): scalars form a linear orderRyan Lahfa2024-04-231-0/+15
| | | | | | | | | | | | | | | | | | | | | 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>
* | | Merge pull request #154 from AeneasVerif/ci-fmtSon HO2024-04-233-2/+23
|\ \ \ | | | | | | | | ci: check code formatting and forbid warnings
| * | | TypoGuillaume Boisseau2024-04-231-1/+1
| | | | | | | | | | | | Co-authored-by: Son HO <hosonmarc@gmail.com>
| * | | ci: Forbid compilation warningsNadrieril2024-04-221-0/+1
| | | |
| * | | ci: check code formattingNadrieril2024-04-223-2/+22
| | | |
* | | | Merge pull request #155 from AeneasVerif/dedup-ciSon HO2024-04-231-0/+22
|\ \ \ \ | |/ / / |/| | | ci: avoid running duplicate jobs
| * | | ci: avoid running duplicate jobsNadrieril2024-04-221-0/+22
|/ / /
* | | Merge pull request #151 from AeneasVerif/son/fix-loops2Son HO2024-04-226-35/+80
|\ \ \ | | | | | | | | Fix an issue in the loops fixed point
| * | | Fix an issue when joining a symbolic value with bottomSon Ho2024-04-222-11/+33
| | | |
| * | | Reformat some filesSon Ho2024-04-225-24/+47
|/ / /
* | | Merge pull request #132 from AeneasVerif/regen-testsSon HO2024-04-1910-15/+10
|\ \ \ | | | | | | | | Ensure we regenerate files properly in CI
| * | | Address review commentsNadrieril2024-04-1818-2/+20
| | | |
| * | | Ensure we regenerate files properly in CINadrieril2024-04-1827-32/+9
| | | | | | | | | | | | | | | | | | | | Files that weren't regenerated were marked as not automatically-generated.
* | | | Merge pull request #146 from RaitoBezarius/mainSon HO2024-04-191-3/+69
|\ \ \ \ | | |/ / | |/| | fix(backends/lean): add a significant amount of keywords
| * | | fix(backends/lean): extract more keywords from `lstlean.tex`Ryan Lahfa2024-04-181-0/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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>
| * | | fix(backends/lean): extract more keywords from `lstlean.latex`Ryan Lahfa2024-04-181-0/+62
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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>
| * | | chore(backends/lean): sort the keyword listRyan Lahfa2024-04-171-4/+4
| | | | | | | | | | | | | | | | | | | | | | | | OCD. :D Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
| * | | fix(backends/lean): `from` is a keywordRyan Lahfa2024-04-171-0/+1
| | | | | | | | | | | | | | | | Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
| * | | fix(backends/lean): `as` is a keywordRyan Lahfa2024-04-171-0/+1
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | `as` is a reserved keyword and cannot be used as a variable name. Fixes #139. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
* | | | Merge pull request #116 from AeneasVerif/item_metaGuillaume Boisseau2024-04-1811-85/+101
|\ \ \ \ | |_|/ / |/| | |
| * | | Update charon pinNadrieril2024-04-182-5/+20
| | | |
| * | | item_metaNadrieril2024-04-189-80/+81
|/ / /
* | | Merge pull request #145 from RaitoBezarius/no-flakesGuillaume Boisseau2024-04-184-1/+50
|\ \ \
| * | | feat(nix): support non-Flakes usersRyan Lahfa2024-04-174-1/+50
| |/ / | | | | | | | | | | | | | | | | | | | | | 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>
* | | Merge pull request #130 from AeneasVerif/fast-tests-outside-of-ciSon HO2024-04-182-8/+4
|\ \ \ | | | | | | | | Run sanity checks in CI only
| * | | Run sanity checks in CI onlyNadrieril2024-04-162-8/+4
| | | |
* | | | Merge pull request #147 from AeneasVerif/binops-simplificationSon HO2024-04-184-478/+171
|\ \ \ \ | |_|/ / |/| | | Bump charon
| * | | Bump charonNadrieril2024-04-174-478/+171
|/ / /
| | * compiler: introduce Lean-only translationsRyan Lahfa2024-04-241-10/+25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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>
| | * compiler: map `core::option::Option::is_none` to `Option.isNone`Ryan Lahfa2024-04-241-0/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | 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>
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 02:52:22 +0000