summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* 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
|\
| * 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
| | |\ | | |/ | |/|
| | * 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>
| | * compiler: map `core::mem::swap` to the pure swapRyan Lahfa2024-04-243-6/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | | 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>
| | * compiler: map `core::option::Option::take` to identity functionRyan Lahfa2024-04-172-0/+6
| | | | | | | | | | | | | | | | | | | | | | | | `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>
* | | 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 #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
|/ /
* | Merge pull request #126 from RaitoBezarius/scalar-preordersSon HO2024-04-151-0/+10
|\ \ | |/ |/| lean: scalars form a preorder
| * lean: scalars form a preorderRyan Lahfa2024-04-121-0/+10
| | | | | | | | | | | | | | | | | | | | 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>
* | Merge pull request #127 from AeneasVerif/fix-ciSon HO2024-04-152-2/+5
|\ \ | |/ |/| Fix CI
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 11:26:40 +0000