summaryrefslogtreecommitdiff
path: root/Makefile (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Fix CINadrieril2024-04-151-1/+4
|
* Remove the check for CHARON_HOMESon Ho2024-04-031-4/+0
|
* Improve the MakefileSon Ho2024-04-031-1/+5
|
* Update the format rule in the MakefileSon Ho2024-03-281-1/+1
|
* Merge remote-tracking branch 'origin/main' into son/examplesSon Ho2024-03-201-3/+7
|\
| * Change the tests target to testSon Ho2024-03-111-2/+2
| |
| * Update the Makefile to automatically reformat the codeSon Ho2024-03-111-3/+7
| |
* | Update the MakefileSon Ho2024-03-201-4/+4
|/
* Update the Makefile and remove the split files for F*Son Ho2024-03-081-21/+4
|
* Add some demo filesSon Ho2024-02-091-1/+8
|
* Rename and regenerate some filesSon Ho2024-02-021-8/+8
|
* Update the MakefileSon Ho2023-12-231-1/+6
|
* Add an option to split the fwd/back functions and fix a minor issueSon Ho2023-12-221-2/+17
|
* Update the library for F*Son Ho2023-12-221-2/+4
|
* Add support for more bitwise operations and update the extractionSon Ho2023-11-291-9/+10
|
* Do not activate the sanity (invariant) checks by defaultSon Ho2023-11-271-5/+2
|
* Rename Driver.ml to Main.mlSon Ho2023-11-161-7/+7
|
* Update the rule build-bin-dir in the MakefileSon Ho2023-11-091-3/+6
|
* Make the traits work for CoqSon Ho2023-11-091-1/+1
|
* Deactivate the HOL4 testsSon Ho2023-11-091-2/+10
|
* Update the Makefile for the F* array testSon Ho2023-11-091-1/+1
|
* Modify some options and update the MakefileSon Ho2023-11-091-13/+13
|
* Update the Makefile to rename the "trans-" rules to "test-"Son Ho2023-11-091-46/+46
|
* Update the Makefile and regenerate some testsSon Ho2023-11-081-0/+4
|
* Update following some changes in CharonSon Ho2023-11-061-1/+9
|
* Make the hashmap files typecheck again in LeanSon Ho2023-10-251-2/+4
|
* Deactivate the concrete interpreter testsSon Ho2023-10-241-2/+2
|
* 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
|
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 09:59:22 +0000