index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
compiler
/
Translate.ml
(
unfollow
)
Commit message (
Expand
)
Author
Files
Lines
2023-10-25
Fix some issues at extraction and add builtins
Son Ho
1
-4
/
+6
2023-10-24
Filter some type arguments for the builtin types/functions
Son Ho
1
-0
/
+2
2023-10-24
Remove the possibility of generating opaque module signatures
Son Ho
1
-32
/
+2
2023-10-24
Add support for builtin trait implementations
Son Ho
1
-1
/
+16
2023-10-24
Fix various issues with the builtins
Son Ho
1
-68
/
+90
2023-10-23
Make progress on handling the builtins
Son Ho
1
-2
/
+7
2023-10-23
Remove some assumed types and add more support for builtin definitions
Son Ho
1
-42
/
+65
2023-10-20
Start updating to handle function pointers
Son Ho
1
-5
/
+5
2023-09-17
Make minor modifications
Son Ho
1
-4
/
+1
2023-09-17
Merge trans_ctx and decls_ctx
Son Ho
1
-62
/
+17
2023-09-17
Fix more issues with the extraction
Son Ho
1
-7
/
+33
2023-09-16
Add a strict_names_map in the extraction_ctx
Son Ho
1
-0
/
+14
2023-09-07
Map some globals like u32::MAX to standard definitions
Son Ho
1
-18
/
+18
2023-09-03
Do more cleanup
Son Ho
1
-3
/
+1
2023-09-03
Add the keep_fwd field in TranslateCore.pure_fun_translation
Son Ho
1
-18
/
+16
2023-09-03
Update TranslateCore.pure_fun_translation
Son Ho
1
-21
/
+19
2023-09-03
Update the type TranslateCore.fun_and_loops
Son Ho
1
-23
/
+23
2023-09-03
Make progress on extracting trait decls and merge gen_ctx and extraction_ctx
Son Ho
1
-93
/
+70
2023-09-03
Make more progress
Son Ho
1
-18
/
+52
2023-09-03
Make progress on the extraction
Son Ho
1
-0
/
+1
2023-09-03
Make progress on the extraction
Son Ho
1
-16
/
+93
2023-08-31
Start adding support for traits
Son Ho
1
-3
/
+1
2023-08-08
Update the code following a refactor on Charon's side
Son Ho
1
-4
/
+7
2023-08-04
Add an option to not override Hashmap.lean
Son Ho
1
-2
/
+1
2023-08-04
Fix issues with the extraction and extend the primitive libraries for Coq and F*
Son Ho
1
-0
/
+2
2023-08-03
Make a minor formatting modification for Lean
Son Ho
1
-1
/
+1
2023-07-06
Use short names for the structure fields in Lean
Son Ho
1
-0
/
+1
2023-07-06
Improve the generated comments
Son Ho
1
-0
/
+4
2023-07-05
Start using namespaces in the Lean backend
Son Ho
1
-28
/
+52
2023-07-04
Fix minor issues
Son Ho
1
-51
/
+115
2023-07-04
Reorganize the Lean tests
Son Ho
1
-35
/
+35
2023-06-04
Make progress on the HOL4 backend
Son Ho
1
-29
/
+46
2023-06-04
Make progress on extracting the HOL4 files
Son Ho
1
-1
/
+1
2023-06-04
Make good progress on generating code for HOL4
Son Ho
1
-190
/
+276
2023-06-04
Make more updates for the Lean backend
Son Ho
1
-12
/
+16
2023-06-04
Make minor modifications
Son Ho
1
-2
/
+14
2023-06-04
Improve the generation of variant names for Lean
Son Ho
1
-1
/
+5
2023-06-04
Add a special expression for structure creation/update
Son Ho
1
-1
/
+9
2023-06-04
Don't create useless directories in Lean
Son Ho
1
-2
/
+4
2023-06-04
Update the extraction of Lean files
Son Ho
1
-11
/
+23
2023-06-04
Automate the generation of the lakefile.lean files
Son Ho
1
-119
/
+166
2023-06-04
Handle the "opaque_defs." prefix in a cleaner manner
Son Ho
1
-2
/
+23
2023-06-04
Consistently use the names TerminationMeasure and DecreasesProof
Son Ho
1
-4
/
+6
2023-06-04
Update the generation of termination and decreases_by templates for Lean
Son Ho
1
-5
/
+9
2023-06-04
More comments
Jonathan Protzenko
1
-0
/
+8
2023-06-04
Make minor fixes, improve formatting for Lean and generate code for all the t...
Son Ho
1
-43
/
+60
2023-06-04
WIP
Jonathan Protzenko
1
-2
/
+19
2023-06-04
Fix some printing bits, proper syntax for terminates and decreases clauses
Jonathan Protzenko
1
-1
/
+4
2023-06-04
WIP lots of stuff
Jonathan Protzenko
1
-3
/
+11
2023-06-04
New directory structure and corresponding extraction, + misc fixes, for Lean
Jonathan Protzenko
1
-25
/
+37
[next]