Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
| * | | | | ci: hydra -> github runner | Paul-Nicolas Madelaine | 2023-10-23 | 2 | -1/+19 | |
|/ / / / | ||||||
| * | | | Update the rule build-bin-dir in the Makefile | Son Ho | 2023-11-09 | 1 | -3/+6 | |
| | | | | ||||||
| * | | | Make administrative updates in the tests | Son Ho | 2023-11-09 | 2 | -405/+49 | |
| | | | | ||||||
| * | | | Update the failing proofs | Son Ho | 2023-11-09 | 16 | -1710/+1049 | |
| | | | | ||||||
| * | | | Regenerate the Coq test files | Son Ho | 2023-11-09 | 14 | -80/+1403 | |
| | | | | ||||||
| * | | | Make the traits work for Coq | Son Ho | 2023-11-09 | 7 | -194/+354 | |
| | | | | ||||||
| * | | | Deactivate the HOL4 tests | Son Ho | 2023-11-09 | 1 | -2/+10 | |
| | | | | ||||||
| * | | | Remove a file | Son Ho | 2023-11-09 | 1 | -387/+0 | |
| | | | | ||||||
| * | | | Update the Makefile for the F* array test | Son Ho | 2023-11-09 | 1 | -1/+1 | |
| | | | | ||||||
| * | | | Regenerate the tests | Son Ho | 2023-11-09 | 2 | -94/+37 | |
| | | | | ||||||
| * | | | Extract the trait parent clauses after the types and the constants | Son Ho | 2023-11-09 | 1 | -24/+25 | |
| | | | | ||||||
| * | | | Progress on making the traits work for F* | Son Ho | 2023-11-09 | 6 | -36/+1616 | |
| | | | | ||||||
| * | | | Modify some options and update the Makefile | Son Ho | 2023-11-09 | 11 | -1082/+2280 | |
| | | | | ||||||
| * | | | Update the Makefile to rename the "trans-" rules to "test-" | Son Ho | 2023-11-09 | 1 | -46/+46 | |
| | | | | ||||||
| * | | | Regenerate some Lean tests | Son Ho | 2023-11-09 | 2 | -0/+39 | |
| | | | | ||||||
| * | | | Fix a small issue in AssociatedTypes | Son Ho | 2023-11-09 | 7 | -15/+21 | |
| | | | | ||||||
| * | | | Update the Makefile and regenerate some tests | Son Ho | 2023-11-08 | 4 | -0/+40 | |
| | | | | ||||||
| * | | | Update the extraction | Son Ho | 2023-11-07 | 3 | -2/+15 | |
| | | | | ||||||
| * | | | Update the normalization of associated types | Son Ho | 2023-11-07 | 4 | -50/+126 | |
| | | | | ||||||
| * | | | Fix a naming issue | Son Ho | 2023-11-06 | 1 | -1/+3 | |
| | | | | ||||||
| * | | | Regenerate part of the trait tests for Lean | Son Ho | 2023-11-06 | 2 | -16/+65 | |
| | | | | ||||||
| * | | | Fix some issues when extracting references to Self | Son Ho | 2023-11-06 | 1 | -30/+57 | |
| | | | | ||||||
| * | | | Update following some changes in Charon | Son Ho | 2023-11-06 | 5 | -58/+68 | |
| | | | | ||||||
| * | | | Make minor updates following changes in Charon | Son Ho | 2023-10-30 | 2 | -6/+2 | |
| | | | | ||||||
| * | | | Add some files for the Coq trait tests | Son Ho | 2023-10-27 | 2 | -0/+28 | |
| | | | | ||||||
| * | | | Fix minor issues in the name collision detection | Son Ho | 2023-10-27 | 2 | -10/+23 | |
| | | | | ||||||
| * | | | Regenerate the Coq test files | Son Ho | 2023-10-27 | 24 | -2118/+3589 | |
| | | | | ||||||
| * | | | Update Primitives.v | Son Ho | 2023-10-27 | 1 | -60/+342 | |
| | | | | ||||||
| * | | | Regenerate more F* files | Son Ho | 2023-10-27 | 18 | -1549/+1427 | |
| | | | | ||||||
| * | | | Fix a minor issue and regenerate some F* test files | Son Ho | 2023-10-27 | 10 | -602/+646 | |
| | | | | ||||||
| * | | | Regenerate some of the F* test files | Son Ho | 2023-10-27 | 19 | -440/+549 | |
| | | | | ||||||
| * | | | Make minor modifications and update the array test for F* | Son Ho | 2023-10-26 | 6 | -188/+200 | |
| | | | | ||||||
| * | | | Update Primitives.fst | Son Ho | 2023-10-26 | 8 | -318/+2757 | |
| | | | | ||||||
| * | | | Fix some issues and regenerate the HashmapMain example for Lean | Son Ho | 2023-10-26 | 5 | -106/+147 | |
| | | | | ||||||
| * | | | Regenerate the betree example for Lean | Son Ho | 2023-10-26 | 1 | -40/+39 | |
| | | | | ||||||
| * | | | Regenerate several test files for Lean | Son Ho | 2023-10-26 | 4 | -122/+132 | |
| | | | | ||||||
| * | | | Improve the handling of saved function effects in ExtractBuiltin.ml | Son Ho | 2023-10-26 | 2 | -24/+44 | |
| | | | | ||||||
| * | | | Regenerate the array files for Lean | Son Ho | 2023-10-26 | 2 | -111/+103 | |
| | | | | ||||||
| * | | | Make progress on fixing the extraction | Son Ho | 2023-10-26 | 2 | -72/+88 | |
| | | | | ||||||
| * | | | Improve ExtractBuiltin.ml | Son Ho | 2023-10-26 | 2 | -46/+57 | |
| | | | | ||||||
| * | | | Make progress on fixing the extraction for Lean | Son Ho | 2023-10-26 | 5 | -220/+180 | |
| | | | | ||||||
| * | | | Fix more issues at extraction and factor out defs in ExtractBuiltin | Son Ho | 2023-10-26 | 2 | -266/+166 | |
| | | | | ||||||
| * | | | Regenerate the hashmap files | Son Ho | 2023-10-25 | 2 | -86/+133 | |
| | | | | ||||||
| * | | | Make the hashmap files typecheck again in Lean | Son Ho | 2023-10-25 | 12 | -2775/+2778 | |
| | | | | ||||||
| * | | | Regenerate the Lean array test | Son Ho | 2023-10-25 | 1 | -169/+150 | |
| | | | | ||||||
| * | | | Fix some issues at extraction and add builtins | Son Ho | 2023-10-25 | 11 | -61/+546 | |
| | | | | ||||||
| * | | | Fix some issues to make the array test succeed again | Son Ho | 2023-10-25 | 2 | -16/+44 | |
| | | | | ||||||
| * | | | Remove the warning for loops | Son Ho | 2023-10-25 | 1 | -8/+0 | |
| | | | | ||||||
| * | | | Update following the addition of raw pointers | Son Ho | 2023-10-25 | 12 | -17/+77 | |
| | | | | ||||||
| * | | | Handle properly the builtin, non fallible functions | Son Ho | 2023-10-24 | 5 | -26/+62 | |
| | | | |