summaryrefslogtreecommitdiff
path: root/compiler/Driver.ml (follow)
Commit message (Collapse)AuthorAgeFilesLines
* 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 ↵Son Ho2022-11-101-2/+10
| | | | option)
* 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-29 14:20:46 +0000