summaryrefslogtreecommitdiff
path: root/Makefile (unfollow)
Commit message (Expand)AuthorFilesLines
2023-12-22Add an option to split the fwd/back functions and fix a minor issueSon Ho1-2/+17
2023-12-22Update the library for F*Son Ho1-2/+4
2023-11-29Add support for more bitwise operations and update the extractionSon Ho1-9/+10
2023-11-27Do not activate the sanity (invariant) checks by defaultSon Ho1-5/+2
2023-11-16Rename Driver.ml to Main.mlSon Ho1-7/+7
2023-11-09Update the rule build-bin-dir in the MakefileSon Ho1-3/+6
2023-11-09Make the traits work for CoqSon Ho1-1/+1
2023-11-09Deactivate the HOL4 testsSon Ho1-2/+10
2023-11-09Update the Makefile for the F* array testSon Ho1-1/+1
2023-11-09Modify some options and update the MakefileSon Ho1-13/+13
2023-11-09Update the Makefile to rename the "trans-" rules to "test-"Son Ho1-46/+46
2023-11-08Update the Makefile and regenerate some testsSon Ho1-0/+4
2023-11-06Update following some changes in CharonSon Ho1-1/+9
2023-10-25Make the hashmap files typecheck again in LeanSon Ho1-2/+4
2023-10-24Deactivate the concrete interpreter testsSon Ho1-2/+2
2023-09-04Fix minor issuesSon Ho1-1/+1
2023-08-04Add an option to not override Hashmap.leanSon Ho1-1/+1
2023-08-04Update the Makefile and regenerate the test filesSon Ho1-15/+13
2023-08-03Update the Makefile to add the array testSon Ho1-1/+16
2023-07-04Reorganize the Lean testsSon Ho1-19/+13
2023-06-04Start setting up the Nix derivation for HOL4Son Ho1-1/+5
2023-06-04Make minor modifications to the MakefileSon Ho1-2/+2
2023-06-04Add the generated HOL4 filesSon Ho1-4/+25
2023-06-04Use dune 3.7 and update the flake.lockSon Ho1-2/+2
2023-06-04Start adding Lean to the Nix flakeSon Ho1-1/+5
2023-06-04Make more updates for the Lean backendSon Ho1-2/+13
2023-06-04Reorganize the Lean tests and extract the Polonius tests to LeanSon Ho1-7/+7
2023-06-04Make minor fixes, improve formatting for Lean and generate code for all the t...Son Ho1-6/+27
2023-06-04Initial Lean backend, WIPJonathan Protzenko1-1/+7
2023-02-03Make minor modifications and generate code for loopsSon Ho1-1/+7
2022-11-16Add a nix derivation for the Coq proofsSon Ho1-1/+5
2022-11-16Add the aeneas-verify-fstar derivationSon Ho1-1/+8
2022-11-14Extract the Polonius examples in CoqSon Ho1-1/+11
2022-11-14Add a `-use-fuel` optionSon Ho1-0/+2
2022-11-14Reactivate the option -test-trans-unis for CoqSon Ho1-3/+1
2022-11-14Implement a pass to decompose nested patterns in let-bindingsSon Ho1-4/+4
2022-11-14Make good progress on the Coq backendSon Ho1-31/+65
2022-11-14Reorganize the project to prepare for new backendsSon Ho1-1/+1
2022-11-11Make minor modifications to the tests and regenerate the .fst filesSon Ho1-4/+4
2022-11-11Move the fstar files to the new backends directorySon Ho1-3/+7
2022-11-11Add a `bin` folderSon Ho1-4/+9
2022-11-11Make the Nix build workSon Ho1-29/+63
2022-11-10Make a minor modificationSon Ho1-1/+0
2022-11-10Implement a Config.ml file which groups all the global options in referencesSon Ho1-4/+4
2022-11-10Implement the generation of stateful backward functions (controlled by an opt...Son Ho1-6/+28
2022-10-28Update the MakefileSon Ho1-2/+2
2022-10-27Reformat the codeSon Ho1-1/+1
2022-10-27Move constant_value to PrimitiveValues.mlSon Ho1-0/+4
2022-10-27Reorganize a bit the projectSon Ho1-9/+9
2022-10-26Update the code documentation to fix links and syntax issuesSon Ho1-1/+1
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 05:25:11 +0000