summaryrefslogtreecommitdiff
path: root/Makefile (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Fix minor issuesSon Ho2023-09-041-1/+1
|
* Add an option to not override Hashmap.leanSon Ho2023-08-041-1/+1
|
* Update the Makefile and regenerate the test filesSon Ho2023-08-041-15/+13
|
* Update the Makefile to add the array testSon Ho2023-08-031-1/+16
|
* Reorganize the Lean testsSon Ho2023-07-041-19/+13
|
* Start setting up the Nix derivation for HOL4Son Ho2023-06-041-1/+5
|
* Make minor modifications to the MakefileSon Ho2023-06-041-2/+2
|
* Add the generated HOL4 filesSon Ho2023-06-041-4/+25
|
* Use dune 3.7 and update the flake.lockSon Ho2023-06-041-2/+2
|
* Start adding Lean to the Nix flakeSon Ho2023-06-041-1/+5
|
* Make more updates for the Lean backendSon Ho2023-06-041-2/+13
|
* Reorganize the Lean tests and extract the Polonius tests to LeanSon Ho2023-06-041-7/+7
|
* Make minor fixes, improve formatting for Lean and generate code for all the ↵Son Ho2023-06-041-6/+27
| | | | test suite
* Initial Lean backend, WIPJonathan Protzenko2023-06-041-1/+7
|
* Make minor modifications and generate code for loopsSon Ho2023-02-031-1/+7
|
* Add a nix derivation for the Coq proofsSon Ho2022-11-161-1/+5
|
* Add the aeneas-verify-fstar derivationSon Ho2022-11-161-1/+8
|
* Extract the Polonius examples in CoqSon Ho2022-11-141-1/+11
|
* Add a `-use-fuel` optionSon Ho2022-11-141-0/+2
|
* Reactivate the option -test-trans-unis for CoqSon Ho2022-11-141-3/+1
|
* Implement a pass to decompose nested patterns in let-bindingsSon Ho2022-11-141-4/+4
|
* Make good progress on the Coq backendSon Ho2022-11-141-31/+65
|
* Reorganize the project to prepare for new backendsSon Ho2022-11-141-1/+1
|
* Make minor modifications to the tests and regenerate the .fst filesSon Ho2022-11-111-4/+4
|
* Move the fstar files to the new backends directorySon Ho2022-11-111-3/+7
|
* Add a `bin` folderSon Ho2022-11-111-4/+9
|
* Make the Nix build workSon Ho2022-11-111-29/+63
|
* Make a minor modificationSon Ho2022-11-101-1/+0
|
* Implement a Config.ml file which groups all the global options in referencesSon Ho2022-11-101-4/+4
|
* Implement the generation of stateful backward functions (controlled by an ↵Son Ho2022-11-101-6/+28
| | | | option)
* Update the MakefileSon Ho2022-10-281-2/+2
|
* Reformat the codeSon Ho2022-10-271-1/+1
|
* Move constant_value to PrimitiveValues.mlSon Ho2022-10-271-0/+4
|
* Reorganize a bit the projectSon Ho2022-10-271-9/+9
|
* Update the code documentation to fix links and syntax issuesSon Ho2022-10-261-1/+1
|
* Start generating documentationSon Ho2022-10-261-4/+13
|
* Update the MakefileSon Ho2022-10-181-3/+7
|
* Use "polonius" in the names instead of "nll"Son Ho2022-10-131-8/+9
|
* Make minor modifications to the MakefileSon Ho2022-10-131-5/+5
|
* Incorrect assumptions, incorrect recursive makeJonathan Protzenko2022-09-271-2/+7
|
* Add a `format` target in the MakefileSon Ho2022-09-221-0/+5
|
* Update MakefileSon HO2022-09-221-1/+1
|
* Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2Sidney Congard2022-06-301-5/+10
|\ | | | | | | Complete the constants extraction by making all functions fail
| * Make minor modificationsSon Ho2022-06-201-2/+2
| |
| * Add makefiles to test the F* filesSon Ho2022-06-201-4/+9
| |
* | concrete & symbolic evaluation work with new LLBC formatSidney Congard2022-06-211-1/+1
| |
* | crude generation working - missing unit tests & special constants handlingSidney Congard2022-06-131-2/+5
|/
* Update the Makefile for the betreeSon Ho2022-05-061-1/+5
|
* Fix minor issues for the translation of hashmap_on_diskSon Ho2022-03-041-18/+22
|
* Fix a minor issue with external function declarationsSon Ho2022-03-041-1/+4
|
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 23:34:06 +0000