summaryrefslogtreecommitdiff
path: root/compiler/Translate.ml (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Remove redundant `llbc_name` fieldNadrieril2024-06-281-4/+5
| | | | It's redundant with `item_meta.name`
* Update charonNadrieril2024-06-241-13/+26
|
* Update charonNadrieril2024-06-211-0/+3
|
* Deactivate some linter options for the generated Lean filesSon Ho2024-06-171-0/+9
|
* Implement a BorrowCheck.borrow_check_crateSon Ho2024-06-051-2/+3
|
* Add an option to run Aeneas as a borrow checkerSon Ho2024-06-051-18/+19
|
* Remove the options from the functions synthesizing the symbolic ASTSon Ho2024-05-301-3/+2
|
* Rename meta into spanAymeric Fromherz2024-05-241-14/+14
|
* Fix a crash which happens when type definitions are ignoredSon Ho2024-05-241-2/+5
|
* Print the name patterns of the definitions which fail to extractSon Ho2024-05-241-11/+19
|
* Add error when handling mutually recursive traitsAymeric Fromherz2024-05-011-1/+4
|
* item_metaNadrieril2024-04-181-3/+3
|
* Merge remote-tracking branch 'origin/main' into son/cleanSon Ho2024-04-111-20/+73
|\
| * Cleanup a bit and improve the error messagesSon Ho2024-04-071-34/+35
| |
| * Resolved comments and added the name of the not translated elementEscherichia2024-04-051-6/+14
| |
| * resolved commentsEscherichia2024-04-051-7/+16
| |
| * error catching should now be able to tell when code couldn't be generatedEscherichia2024-04-051-11/+46
| |
* | Add field mk_return, mk_panic in SymbolicToPure.bs_ctxSon Ho2024-04-041-0/+2
|/
* Cleanup and fix a mistakeSon Ho2024-03-291-0/+1
|
* added file and line arg to craise and cassertEscherichia2024-03-291-2/+2
|
* changes after git rebase mainEscherichia2024-03-281-3/+2
|
* Should answer all comments, there are still some TODO: error message leftEscherichia2024-03-281-7/+7
|
* Still need to fill the TODO: error message and check some meta but it buildsEscherichia2024-03-281-24/+24
|
* WIP: translate.ml and extract.ml do not compile. Some assert left to do and ↵Escherichia2024-03-281-25/+25
| | | | we need to see how translate_crate can give meta to the functions it calls
* WIP: does not compile yet because we need to propagate the meta variable.Escherichia2024-03-281-3/+3
|
* WIP Beginning working on better errors: began replacing raise (Failure) and ↵Escherichia2024-03-281-40/+42
| | | | assert by craise and cassert. Does not compile yet, still need to propagate the meta variable where it's relevant
* Make good progress on adding generics to global constantsSon Ho2024-03-181-0/+1
|
* Fix a minor issueSon Ho2024-03-171-1/+1
|
* Update the generation of namesSon Ho2024-03-111-1/+1
|
* Make progress on propagating the changesSon Ho2024-03-081-118/+27
|
* Update the library for F*Son Ho2023-12-221-1/+7
|
* Fix several issuesSon Ho2023-12-211-13/+16
|
* Make good progress on merging the fwd/back functionsSon Ho2023-12-211-1/+2
|
* Remove SymbolicToPure.bs_ctx.loop_backward_outputsSon Ho2023-12-191-1/+0
|
* Simplify SymbolicToPure.bs_ctx.{backward_outputs, loop_backward_outputs}Son Ho2023-12-191-16/+1
|
* Rename some definitionsSon Ho2023-12-181-7/+7
|
* Make progress on updating the codeSon Ho2023-12-151-114/+93
|
* Make progress on generated merged fwd/back functionsSon Ho2023-12-141-1/+3
|
* Update Pure.fun_sig_infoSon Ho2023-12-131-2/+6
|
* Update following changes in CharonSon Ho2023-12-051-1/+1
|
* Update the way the Primitives file is copiedSon Ho2023-11-271-13/+20
|
* Generate a dedicated file for the external typesSon Ho2023-11-271-12/+102
|
* Update the generation of files for external definitions and regenerate the testsSon Ho2023-11-271-9/+14
|
* Reorganize the "Extract" filesSon Ho2023-11-211-15/+4
|
* Use the name matcher implemented in CharonSon Ho2023-11-201-11/+14
|
* Finish propagating the changes to the names and cleaningSon Ho2023-11-161-81/+78
|
* Add RegionsHierarchy.mlSon Ho2023-11-131-2/+5
|
* Remove the 'r type variable from the ty type definitionSon Ho2023-11-121-6/+6
|
* Make the traits work for CoqSon Ho2023-11-091-6/+16
|
* Make progress on fixing the extraction for LeanSon Ho2023-10-261-18/+3
|
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 21:03:13 +0000