Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
| * | Merge remote-tracking branch 'origin/main' into son/examples | Son Ho | 2024-03-20 | 1 | -3/+7 | |
| |\ | |/ |/| | ||||||
* | | Merge pull request #90 from AeneasVerif/son/makefile | Son HO | 2024-03-20 | 2 | -9/+13 | |
|\ \ | | | | | | | Update the Makefile to automatically reformat the code | |||||
| * | | Change the tests target to test | Son Ho | 2024-03-11 | 2 | -6/+6 | |
| | | | ||||||
| * | | Update the Makefile to automatically reformat the code | Son Ho | 2024-03-11 | 1 | -3/+7 | |
| | | | ||||||
| | * | Update the Makefile | Son Ho | 2024-03-20 | 2 | -8/+8 | |
| | | | ||||||
| | * | Update the flake.lock | Son Ho | 2024-03-20 | 1 | -15/+15 | |
| | | | ||||||
| | * | Regenerate the code | Son Ho | 2024-03-20 | 29 | -454/+431 | |
| | | | ||||||
| | * | Improve the generation of pretty name and the micro passes | Son Ho | 2024-03-20 | 8 | -30/+144 | |
| | | | ||||||
| | * | Regenerate the tests | Son Ho | 2024-03-19 | 22 | -188/+80 | |
| | | | ||||||
| | * | Improve the pure micro passes | Son Ho | 2024-03-19 | 2 | -8/+64 | |
| | | | ||||||
| | * | Update the demo | Son Ho | 2024-03-19 | 4 | -30/+126 | |
| |/ |/| | ||||||
* | | Merge pull request #92 from AeneasVerif/son/globals | Son HO | 2024-03-18 | 18 | -462/+506 | |
|\ \ | | | | | | | Add generics to constants/globals | |||||
| * | | Update the flake.nix and the flake.lock | Son Ho | 2024-03-18 | 2 | -367/+4 | |
| | | | ||||||
| * | | Fix a minor issue | Son Ho | 2024-03-18 | 1 | -1/+3 | |
| | | | ||||||
| * | | Regenerate the test files | Son Ho | 2024-03-18 | 6 | -66/+297 | |
| | | | ||||||
| * | | Update extract_trait_impl | Son Ho | 2024-03-18 | 1 | -7/+23 | |
| | | | ||||||
| * | | Fix the extraction of trait constants | Son Ho | 2024-03-18 | 2 | -35/+22 | |
| | | | ||||||
| * | | Regenerate the constants tests and update Primitives/Base.lean | Son Ho | 2024-03-18 | 4 | -55/+101 | |
| | | | ||||||
| * | | Make good progress on adding generics to global constants | Son Ho | 2024-03-18 | 8 | -47/+172 | |
|/ / | ||||||
* | | Merge pull request #91 from AeneasVerif/son/hax | Son HO | 2024-03-17 | 16 | -101/+75 | |
|\ \ | |/ |/| | Prepare the merge in hax | |||||
| * | Update the flake.lock | Son Ho | 2024-03-17 | 1 | -21/+21 | |
| | | ||||||
| * | Fix a minor issue | Son Ho | 2024-03-17 | 1 | -1/+1 | |
| | | ||||||
| * | Make minor updates | Son Ho | 2024-03-17 | 3 | -7/+14 | |
| | | ||||||
| * | Fix a small issue ollowing updates in Charon | Son Ho | 2024-03-17 | 1 | -3/+8 | |
| | | ||||||
| * | Update following changes in Charon | Son Ho | 2024-03-17 | 11 | -72/+34 | |
|/ | ||||||
* | Merge pull request #88 from AeneasVerif/son/clashes | Son HO | 2024-03-11 | 37 | -703/+825 | |
|\ | | | | | Improve the name generation for code extraction | |||||
| * | Update the flake.lock | Son Ho | 2024-03-11 | 1 | -12/+12 | |
| | | ||||||
| * | Regenerate the test files | Son Ho | 2024-03-11 | 14 | -244/+227 | |
| | | ||||||
| * | Simplify the generated names | Son Ho | 2024-03-11 | 1 | -14/+25 | |
| | | ||||||
| * | Update the generated files | Son Ho | 2024-03-11 | 15 | -380/+389 | |
| | | ||||||
| * | Update tests/Makefile | Son Ho | 2024-03-11 | 1 | -1/+1 | |
| | | ||||||
| * | Update the generation of names | Son Ho | 2024-03-11 | 7 | -39/+57 | |
| | | ||||||
| * | Update a builtin name | Son Ho | 2024-03-11 | 1 | -1/+1 | |
| | | ||||||
| * | Update the builtin name patterns | Son Ho | 2024-03-10 | 1 | -23/+66 | |
| | | ||||||
| * | Update the name generation and add CLI to print external pat names | Son Ho | 2024-03-10 | 7 | -48/+106 | |
|/ | ||||||
* | Merge pull request #85 from AeneasVerif/son/fix_loops3 | Son HO | 2024-03-09 | 28 | -350/+1185 | |
|\ | | | | | Fix some issues with the loops | |||||
| * | Update the flake.lock | Son Ho | 2024-03-09 | 1 | -24/+24 | |
| | | ||||||
| * | Regenerate the test files | Son Ho | 2024-03-09 | 10 | -0/+420 | |
| | | ||||||
| * | Fix an issue with the divergent encoding | Son Ho | 2024-03-09 | 1 | -3/+27 | |
| | | ||||||
| * | Fix some issues | Son Ho | 2024-03-08 | 2 | -9/+10 | |
| | | ||||||
| * | Add some comments | Son Ho | 2024-03-08 | 2 | -9/+12 | |
| | | ||||||
| * | Fix an issue in PureMicroPasses.filter_loop_inputs | Son Ho | 2024-03-08 | 1 | -13/+43 | |
| | | ||||||
| * | Simplify the contexts before symbolically evaluating loops | Son Ho | 2024-03-08 | 4 | -2/+137 | |
| | | ||||||
| * | Fix a last issue | Son Ho | 2024-03-08 | 2 | -51/+110 | |
| | | ||||||
| * | Fix an issue with the loops | Son Ho | 2024-03-08 | 1 | -1/+7 | |
| | | ||||||
| * | Make progress on fixing the loops | Son Ho | 2024-03-08 | 8 | -31/+70 | |
| | | ||||||
| * | Fix a small issue with the loops | Son Ho | 2024-03-08 | 2 | -7/+19 | |
| | | ||||||
| * | Fix some issues with the loops | Son Ho | 2024-03-08 | 3 | -140/+206 | |
| | | ||||||
| * | Do not fail in end_abstraction_aux if the abs disappeared | Son Ho | 2024-03-08 | 2 | -64/+80 | |
| | | ||||||
| * | Add logging information | Son Ho | 2024-03-08 | 3 | -0/+24 | |
| | |