summaryrefslogtreecommitdiff
path: root/compiler/Main.ml (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-05Implement a BorrowCheck.borrow_check_crateSon Ho1-3/+6
2024-06-05Add an option to run Aeneas as a borrow checkerSon Ho1-30/+67
2024-05-24Rename meta into spanAymeric Fromherz1-1/+1
2024-04-07Cleanup a bit and improve the error messagesSon Ho1-1/+3
2024-04-04Update the way errors are reportedSon Ho1-4/+7
2024-04-04Now prints all errors in the error_listEscherichia1-3/+5
2024-04-03Update the initial configurationSon Ho1-3/+0
2024-03-29Cleanup a bitSon Ho1-17/+5
2024-03-29Make a minor modificationSon Ho1-1/+4
2024-03-29Improve the error messagesSon Ho1-8/+23
2024-03-28formattingEscherichia1-1/+3
2024-03-28Should answer all comments, there are still some TODO: error message leftEscherichia1-1/+1
2024-03-28WIP: translate.ml and extract.ml do not compile. Some assert left to do and w...Escherichia1-2/+2
2024-03-28WIP: does not compile yet because we need to propagate the meta variable.Escherichia1-1/+1
2024-03-28WIP Beginning working on better errors: began replacing raise (Failure) and a...Escherichia1-2/+2
2024-03-10Update the name generation and add CLI to print external pat namesSon Ho1-0/+3
2024-03-08Make progress on propagating the changesSon Ho1-6/+0
2024-03-08Remove the option to split fwd/back functions and update SymbolicToPureSon Ho1-3/+0
2024-03-08Update the code generated for tuple projectorsSon Ho1-0/+4
2023-12-23Fix an issue when deconstructing tuples in CoqSon Ho1-3/+0
2023-12-22Add an option to split the fwd/back functions and fix a minor issueSon Ho1-0/+3
2023-12-05Print error messages when the command line arguments are invalidSon Ho1-10/+40
2023-11-27Do not activate the sanity (invariant) checks by defaultSon Ho1-4/+4
2023-11-21Reorganize the "Extract" filesSon Ho1-1/+4
2023-11-20Fix minor issuesSon Ho1-0/+1
2023-11-16Rename Driver.ml to Main.mlSon Ho1-0/+0
2023-11-16Finish propagating the changes to the names and cleaningSon Ho1-12/+9
2023-11-13Make minor modificationsSon Ho1-0/+1
2023-11-09Modify some options and update the MakefileSon Ho1-7/+7
2023-11-09Fix a small issue in AssociatedTypesSon Ho1-1/+7
2023-10-26Make minor modifications and update the array test for F*Son Ho1-1/+3
2023-10-25Remove the warning for loopsSon Ho1-8/+0
2023-10-16Fix a small issueSon Ho1-2/+0
2023-10-13Add supSon Ho1-0/+2
2023-09-07Map some globals like u32::MAX to standard definitionsSon Ho1-14/+0
2023-09-04Fix minor issuesSon Ho1-1/+3
2023-08-08Update the code following a refactor on Charon's sideSon Ho1-2/+6
2023-08-04Add an option to not override Hashmap.leanSon Ho1-0/+6
2023-07-06Use short names for the structure fields in LeanSon Ho1-1/+3
2023-07-04Reorganize the Lean testsSon Ho1-0/+6
2023-06-04Make good progress on generating code for HOL4Son Ho1-0/+5
2023-06-04Add a sanity check in Driver.mlSon Ho1-0/+13
2023-06-04Remove the symbolic interpreter testsSon Ho1-5/+0
2023-06-04Automate the generation of the lakefile.lean filesSon Ho1-1/+1
2023-06-04Add a check in Driver.mlSon Ho1-0/+12
2023-06-04Consistently use the names TerminationMeasure and DecreasesProofSon Ho1-11/+13
2023-06-04Add more checks in Driver.mlSon Ho1-2/+6
2023-06-04Print warnings for the Lean backend and loopsSon Ho1-8/+13
2023-06-04WIP lots of stuffJonathan Protzenko1-15/+19
2023-06-04Initial Lean backend, WIPJonathan Protzenko1-0/+2
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 02:09:54 +0000