summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* 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
| * 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
| | | |
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 22:10:10 +0000