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
(
follow
)
Commit message (
Expand
)
Author
Age
Files
Lines
...
*
Add the function signatures in Assumed.ml
Son Ho
2023-08-02
1
-0
/
+143
*
Make more progress
Son Ho
2023-08-02
2
-75
/
+186
*
Make progress
Son Ho
2023-08-02
5
-53
/
+80
*
Make progress
Son Ho
2023-08-02
14
-76
/
+178
*
Make progress
Son Ho
2023-08-02
7
-164
/
+232
*
Make progress proapagating the changes
Son Ho
2023-08-02
25
-273
/
+407
*
Start adding support for const generics
Son Ho
2023-08-01
11
-226
/
+246
*
Make the `by inlit` implicit
Son Ho
2023-07-12
1
-1
/
+1
*
Use short names for the structure fields in Lean
Son Ho
2023-07-06
5
-19
/
+78
*
Improve the generated comments
Son Ho
2023-07-06
3
-24
/
+102
*
Simplify the names used in Primitives.lean
Son Ho
2023-07-05
1
-16
/
+33
*
Simplify the generated names for the types in Lean
Son Ho
2023-07-05
1
-5
/
+12
*
Start using namespaces in the Lean backend
Son Ho
2023-07-05
5
-45
/
+84
*
Fix minor issues
Son Ho
2023-07-04
2
-55
/
+125
*
Fix some issues with the extraction to Lean
Son Ho
2023-07-04
1
-48
/
+86
*
Reorganize the Lean tests
Son Ho
2023-07-04
5
-43
/
+62
*
Make progress on the HOL4 backend
Son Ho
2023-06-04
2
-39
/
+80
*
Make progress on extracting the HOL4 files
Son Ho
2023-06-04
3
-16
/
+103
*
Make the unfolding theorems collection from evalLib persistent
Son Ho
2023-06-04
1
-9
/
+13
*
Make good progress on generating code for HOL4
Son Ho
2023-06-04
8
-487
/
+1217
*
Use dune 3.7 and update the flake.lock
Son Ho
2023-06-04
3
-5
/
+5
*
Add a sanity check in Driver.ml
Son Ho
2023-06-04
1
-0
/
+13
*
Make more updates for the Lean backend
Son Ho
2023-06-04
2
-26
/
+43
*
Make minor modifications
Son Ho
2023-06-04
2
-3
/
+23
*
Update Extract.ml
Son Ho
2023-06-04
1
-15
/
+35
*
Make extract_adt_cons call extract_adt_g_value
Son Ho
2023-06-04
1
-54
/
+15
*
Make a minor fix
Son Ho
2023-06-04
1
-7
/
+1
*
Improve the generation of variant names for Lean
Son Ho
2023-06-04
3
-15
/
+33
*
Improve simplify_aggregates to introduce structure updates
Son Ho
2023-06-04
2
-3
/
+48
*
Start updating simplify_aggregates
Son Ho
2023-06-04
1
-2
/
+43
*
Add a special expression for structure creation/update
Son Ho
2023-06-04
9
-182
/
+451
*
Don't create useless directories in Lean
Son Ho
2023-06-04
1
-2
/
+4
*
Update the extraction of Lean files
Son Ho
2023-06-04
2
-25
/
+51
*
Reorganize the Lean tests and extract the Polonius tests to Lean
Son Ho
2023-06-04
1
-1
/
+1
*
Remove the symbolic interpreter tests
Son Ho
2023-06-04
2
-35
/
+0
*
Automate the generation of the lakefile.lean files
Son Ho
2023-06-04
2
-120
/
+167
*
Add a check in Driver.ml
Son Ho
2023-06-04
1
-0
/
+12
*
Handle the "opaque_defs." prefix in a cleaner manner
Son Ho
2023-06-04
3
-95
/
+253
*
Make minor modifications
Son Ho
2023-06-04
1
-41
/
+89
*
Consistently use the names TerminationMeasure and DecreasesProof
Son Ho
2023-06-04
5
-61
/
+108
*
Update the generation of termination and decreases_by templates for Lean
Son Ho
2023-06-04
2
-28
/
+39
*
Add more checks in Driver.ml
Son Ho
2023-06-04
2
-3
/
+8
*
Print warnings for the Lean backend and loops
Son Ho
2023-06-04
1
-8
/
+13
*
WIP
Jonathan Protzenko
2023-06-04
1
-3
/
+6
*
More comments
Jonathan Protzenko
2023-06-04
1
-0
/
+8
*
Idiomatic naming conventions
Jonathan Protzenko
2023-06-04
1
-2
/
+7
*
Improve formatting further by removing useless spaces
Son Ho
2023-06-04
1
-15
/
+22
*
Make sure let-bindings in Lean end with line breaks and improve formatting
Son Ho
2023-06-04
2
-43
/
+55
*
Improve formatting of the termination_by clauses
Son Ho
2023-06-04
1
-2
/
+8
*
Make minor fixes, improve formatting for Lean and generate code for all the t...
Son Ho
2023-06-04
3
-177
/
+203
[prev]
[next]