summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* 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 #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
| * Fix CINadrieril2024-04-152-2/+5
|/
* Merge pull request #124 from AeneasVerif/son/lean1Son HO2024-04-1211-60/+674
|\ | | | | Add more definitions to the Lean library
| * Add more definitions to the Lean librarySon Ho2024-04-125-0/+200
| |
| * Reorganize the files in the Lean backend a bitSon Ho2024-04-125-241/+266
| |
| * Start adding integer functions to the Lean librarySon Ho2024-04-127-58/+447
|/
* Merge pull request #110 from zhassan-aws/checked-opsSon HO2024-04-122-21/+279
|\ | | | | Add builtins for some checked ops for the Lean backend
| * Update the bindings for the extractionSon Ho2024-04-121-14/+11
| |
| * Merge branch 'main' into checked-opsSon Ho2024-04-120-0/+0
| |\ | |/ |/|
* | Merge pull request #123 from AeneasVerif/son/cleanSon HO2024-04-1180-1997/+1989
|\ \ | | | | | | Cleanup the code in preparation of the nested loops
| | * Fix a proofSon Ho2024-04-121-1/+0
| | |
| | * Update the core.num.checked_* definitionsSon Ho2024-04-121-31/+233
| | |
| | * Merge branch 'son/clean' into checked-opsSon Ho2024-04-11117-2327/+2546
| | |\ | | |/ | |/|
| * | Update a Lean fileSon Ho2024-04-111-1/+1
| | |
| * | Update some Lean proofsSon Ho2024-04-113-24/+24
| | |
| * | Update a commentSon Ho2024-04-111-2/+2
| | |
| * | Fix a Coq fileSon Ho2024-04-111-1/+1
| | |
| * | Fix some F* proofsSon Ho2024-04-111-4/+4
| | |
| * | Merge remote-tracking branch 'origin/main' into son/cleanSon Ho2024-04-1140-130/+310
| |\ \ | |/ / |/| |
* | | Merge pull request #121 from AeneasVerif/son/formatSon HO2024-04-111-9/+6
|\ \ \ | | | | | | | | Reformat the code
| * | | Reformat the codeSon Ho2024-04-111-9/+6
|/ / /
* | | Merge pull request #119 from AeneasVerif/generic-copyGuillaume Boisseau2024-04-114-11/+11
|\ \ \
| * | | Use charon mainNadrieril2024-04-112-5/+4
| | | |
| * | | Update a commentSon HO2024-04-111-1/+1
| | | |
| * | | Trust rustc regarding `Copy` boundsNadrieril2024-04-105-11/+12
|/ / /
* | | Merge pull request #115 from AeneasVerif/nixSon HO2024-04-101-0/+7
|\ \ \ | | | | | | | | Update flake.nix
| * | | Update flake.nixNadrieril2024-04-081-0/+7
|/ / / | | | | | | | | | | | | It was missing some dependencies, and while we're at it we can disable sanity checks in tests.
* | | Merge pull request #113 from AeneasVerif/escherichia/error_catching_translateSon HO2024-04-0715-66/+186
|\ \ \ | | | | | | | | Error catching should tell when code couldn't be generated
| * | | Improve the error messages furtherSon Ho2024-04-073-1/+44
| | | |
| * | | Cleanup a bit and improve the error messagesSon Ho2024-04-0712-82/+91
| | | |
| * | | Resolved comments and added the name of the not translated elementEscherichia2024-04-052-7/+18
| | | |
| * | | resolved commentsEscherichia2024-04-053-99/+113
| | | |
| * | | error catching should now be able to tell when code couldn't be generatedEscherichia2024-04-053-101/+144
| | | |
* | | | Merge pull request #114 from AeneasVerif/son/lean-versionSon HO2024-04-0512-36/+36
|\ \ \ \ | |/ / / |/| | | Bump the version of Lean to 4.7.0
| * | | Update the lean toolchain and fix the proofsSon Ho2024-04-0512-36/+36
| | | |
* | | | Merge pull request #106 from AeneasVerif/escherichia/error_catchingSon HO2024-04-0413-9/+54
|\ \ \ \ | | | | | | | | | | Added Error and EError to expressions and propagated related changes
| * | | | Fix a minor issueSon Ho2024-04-041-1/+1
| | | | |
| * | | | Merge remote-tracking branch 'origin/main' into escherichia/error_catchingSon Ho2024-04-0445-396/+446
| |\ \ \ \
| * | | | | Update the way errors are reportedSon Ho2024-04-042-10/+7
| | | | | |
| * | | | | Update the nix flakeSon Ho2024-04-041-3/+3
| | | | | |
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 12:32:07 +0000