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
(
unfollow
)
Commit message (
Expand
)
Author
Files
Lines
2023-07-05
Simplify the names used in Primitives.lean
Son Ho
1
-16
/
+33
2023-07-05
Simplify the generated names for the types in Lean
Son Ho
1
-5
/
+12
2023-07-05
Start using namespaces in the Lean backend
Son Ho
5
-45
/
+84
2023-07-04
Fix minor issues
Son Ho
2
-55
/
+125
2023-07-04
Fix some issues with the extraction to Lean
Son Ho
1
-48
/
+86
2023-07-04
Reorganize the Lean tests
Son Ho
5
-43
/
+62
2023-06-04
Make progress on the HOL4 backend
Son Ho
2
-39
/
+80
2023-06-04
Make progress on extracting the HOL4 files
Son Ho
3
-16
/
+103
2023-06-04
Make the unfolding theorems collection from evalLib persistent
Son Ho
1
-9
/
+13
2023-06-04
Make good progress on generating code for HOL4
Son Ho
8
-487
/
+1217
2023-06-04
Use dune 3.7 and update the flake.lock
Son Ho
3
-5
/
+5
2023-06-04
Add a sanity check in Driver.ml
Son Ho
1
-0
/
+13
2023-06-04
Make more updates for the Lean backend
Son Ho
2
-26
/
+43
2023-06-04
Make minor modifications
Son Ho
2
-3
/
+23
2023-06-04
Update Extract.ml
Son Ho
1
-15
/
+35
2023-06-04
Make extract_adt_cons call extract_adt_g_value
Son Ho
1
-54
/
+15
2023-06-04
Make a minor fix
Son Ho
1
-7
/
+1
2023-06-04
Improve the generation of variant names for Lean
Son Ho
3
-15
/
+33
2023-06-04
Improve simplify_aggregates to introduce structure updates
Son Ho
2
-3
/
+48
2023-06-04
Start updating simplify_aggregates
Son Ho
1
-2
/
+43
2023-06-04
Add a special expression for structure creation/update
Son Ho
9
-182
/
+451
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
2
-25
/
+51
2023-06-04
Reorganize the Lean tests and extract the Polonius tests to Lean
Son Ho
1
-1
/
+1
2023-06-04
Remove the symbolic interpreter tests
Son Ho
2
-35
/
+0
2023-06-04
Automate the generation of the lakefile.lean files
Son Ho
2
-120
/
+167
2023-06-04
Add a check in Driver.ml
Son Ho
1
-0
/
+12
2023-06-04
Handle the "opaque_defs." prefix in a cleaner manner
Son Ho
3
-95
/
+253
2023-06-04
Make minor modifications
Son Ho
1
-41
/
+89
2023-06-04
Consistently use the names TerminationMeasure and DecreasesProof
Son Ho
5
-61
/
+108
2023-06-04
Update the generation of termination and decreases_by templates for Lean
Son Ho
2
-28
/
+39
2023-06-04
Add more checks in Driver.ml
Son Ho
2
-3
/
+8
2023-06-04
Print warnings for the Lean backend and loops
Son Ho
1
-8
/
+13
2023-06-04
WIP
Jonathan Protzenko
1
-3
/
+6
2023-06-04
More comments
Jonathan Protzenko
1
-0
/
+8
2023-06-04
Idiomatic naming conventions
Jonathan Protzenko
1
-2
/
+7
2023-06-04
Improve formatting further by removing useless spaces
Son Ho
1
-15
/
+22
2023-06-04
Make sure let-bindings in Lean end with line breaks and improve formatting
Son Ho
2
-43
/
+55
2023-06-04
Improve formatting of the termination_by clauses
Son Ho
1
-2
/
+8
2023-06-04
Make minor fixes, improve formatting for Lean and generate code for all the t...
Son Ho
3
-177
/
+203
2023-06-04
All of the generated code is syntactically correct
Jonathan Protzenko
2
-8
/
+19
2023-06-04
WIP
Jonathan Protzenko
3
-5
/
+30
2023-06-04
Fix runaway indentation
Jonathan Protzenko
1
-4
/
+4
2023-06-04
Fill out more of the primitives file, attempt at type classes for scalar_cast
Jonathan Protzenko
1
-10
/
+15
2023-06-04
Don't need extra variables for the decreases clauses
Jonathan Protzenko
1
-3
/
+9
2023-06-04
WIP printing proper clauses
Jonathan Protzenko
1
-3
/
+58
2023-06-04
Fix some printing bits, proper syntax for terminates and decreases clauses
Jonathan Protzenko
3
-16
/
+186
2023-06-04
WIP lots of stuff
Jonathan Protzenko
3
-27
/
+47
2023-06-04
Fix a syntax error
Jonathan Protzenko
1
-2
/
+6
2023-06-04
Custom syntax support for structures in Lean
Jonathan Protzenko
2
-20
/
+45
[next]