summaryrefslogtreecommitdiff
path: root/compiler/Driver.ml (follow)
Commit message (Expand)AuthorAgeFilesLines
* 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 19:54:20 +0000