summaryrefslogtreecommitdiff
path: root/compiler/Driver.ml (follow)
Commit message (Expand)AuthorAgeFilesLines
* Make minor modifications and update the array test for F*Son Ho2023-10-261-1/+3
* Remove the warning for loopsSon Ho2023-10-251-8/+0
* Fix a small issueSon Ho2023-10-161-2/+0
* Add supSon Ho2023-10-131-0/+2
* Map some globals like u32::MAX to standard definitionsSon Ho2023-09-071-14/+0
* Fix minor issuesSon Ho2023-09-041-1/+3
* Update the code following a refactor on Charon's sideSon Ho2023-08-081-2/+6
* Add an option to not override Hashmap.leanSon Ho2023-08-041-0/+6
* Use short names for the structure fields in LeanSon Ho2023-07-061-1/+3
* Reorganize the Lean testsSon Ho2023-07-041-0/+6
* Make good progress on generating code for HOL4Son Ho2023-06-041-0/+5
* Add a sanity check in Driver.mlSon Ho2023-06-041-0/+13
* Remove the symbolic interpreter testsSon Ho2023-06-041-5/+0
* Automate the generation of the lakefile.lean filesSon Ho2023-06-041-1/+1
* Add a check in Driver.mlSon Ho2023-06-041-0/+12
* Consistently use the names TerminationMeasure and DecreasesProofSon Ho2023-06-041-11/+13
* Add more checks in Driver.mlSon Ho2023-06-041-2/+6
* Print warnings for the Lean backend and loopsSon Ho2023-06-041-8/+13
* WIP lots of stuffJonathan Protzenko2023-06-041-15/+19
* Initial Lean backend, WIPJonathan Protzenko2023-06-041-0/+2
* Do not unfold the monadic lets for the generated F* codeSon Ho2023-02-031-2/+3
* Split InterpreterLoops into several filesSon Ho2023-02-031-0/+3
* Make minor modifications and generate code for loopsSon Ho2023-02-031-24/+28
* Remove the meta-value field from AMutBorrowSon Ho2023-02-031-16/+18
* Generate record field projectors for CoqSon Ho2022-11-161-7/+0
* Add a `-use-fuel` optionSon Ho2022-11-141-0/+8
* Implement a pass to decompose nested patterns in let-bindingsSon Ho2022-11-141-21/+13
* Make good progress on the Coq backendSon Ho2022-11-141-5/+31
* Make the Nix build workSon Ho2022-11-111-3/+4
* Implement a Config.ml file which groups all the global options in referencesSon Ho2022-11-101-63/+21
* Implement the generation of stateful backward functions (controlled by an opt...Son Ho2022-11-101-2/+10
* Add some .mli filesSon Ho2022-11-071-0/+1
* Make minor modificationsSon Ho2022-10-281-1/+1
* Make minor updates to account for Charon's changesSon Ho2022-10-281-1/+1
* Rename driver.ml to Driver.mlSon Ho2022-10-271-0/+208
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 14:13:21 +0000