index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Collapse
)
Author
Age
Files
Lines
*
Cleanup a bit
Son Ho
2023-06-04
3
-191
/
+17
|
*
Make progress on primitivesScript
Son Ho
2023-06-04
6
-211
/
+333
|
*
Make more progress on primitivesScript.sml
Son Ho
2023-06-04
2
-209
/
+191
|
*
Use lower case in the names for the HOL4 backend
Son Ho
2023-06-04
5
-832
/
+771
|
*
Make progress on primitivesScript.sml and experiment a bit
Son Ho
2023-06-04
4
-87
/
+890
|
*
Make progress on the primitives library for HOL4
Son Ho
2023-06-04
3
-12
/
+196
|
*
Organize a bit the HOL files
Son Ho
2023-06-04
8
-190
/
+1160
|
*
Make minor modifications
Son Ho
2023-06-04
2
-5
/
+5
|
*
Add a Holmakefile
Son Ho
2023-06-04
5
-17
/
+2527
|
*
Make good progress on Primitives.sml
Son Ho
2023-06-04
1
-24
/
+997
|
*
Start working on Primitives.sml
Son Ho
2023-06-04
2
-5
/
+387
|
*
Add a more interesting example
Son Ho
2023-06-04
1
-1
/
+69
|
*
Implement a progress tactic
Son Ho
2023-06-04
1
-33
/
+339
|
*
Make more progress on the automation
Son Ho
2023-06-04
1
-51
/
+199
|
*
Make minor modifications to the HOL experiment
Son Ho
2023-06-04
1
-5
/
+25
|
*
Make progress on implementing tactics
Son Ho
2023-06-04
1
-27
/
+347
|
*
Implement [assume_bounds_for_all_int_vars] to improve the proof experience
Son Ho
2023-06-04
1
-80
/
+145
|
*
Start making tests in HOL4
Son Ho
2023-06-04
1
-0
/
+825
|
*
Add a comment
Son Ho
2023-06-04
1
-1
/
+1
|
*
Update the flake.lock
Son Ho
2023-06-04
1
-15
/
+15
|
*
Use dune 3.7 and update the flake.lock
Son Ho
2023-06-04
6
-51
/
+73
|
*
Add a sanity check in Driver.ml
Son Ho
2023-06-04
1
-0
/
+13
|
*
Add Result_Inhabited to Primitives.lean
Son Ho
2023-06-04
9
-0
/
+27
|
*
Start adding Lean to the Nix flake
Son Ho
2023-06-04
3
-19
/
+388
|
*
Regenerate the translated files for Lean
Son Ho
2023-06-04
37
-4931
/
+4452
|
*
Make more updates for the Lean backend
Son Ho
2023-06-04
4
-61
/
+113
|
*
Make minor modifications
Son Ho
2023-06-04
2
-3
/
+23
|
*
Update Extract.ml
Son Ho
2023-06-04
1
-15
/
+35
|
*
Update Primitives.lean
Son Ho
2023-06-04
1
-90
/
+58
|
*
Update Primitives.lean
Son Ho
2023-06-04
1
-194
/
+390
|
*
Add backends/lean/lakefile.lean
Son Ho
2023-06-04
3
-0
/
+39
|
*
Make extract_adt_cons call extract_adt_g_value
Son Ho
2023-06-04
1
-54
/
+15
|
*
Make a minor modification to flake.nix
Son Ho
2023-06-04
1
-3
/
+3
|
*
Make a minor fix
Son Ho
2023-06-04
5
-46
/
+33
|
*
Improve the generation of variant names for Lean
Son Ho
2023-06-04
14
-466
/
+452
|
*
Improve simplify_aggregates to introduce structure updates
Son Ho
2023-06-04
9
-317
/
+127
|
*
Start updating simplify_aggregates
Son Ho
2023-06-04
15
-294
/
+632
|
*
Add a special expression for structure creation/update
Son Ho
2023-06-04
9
-182
/
+451
|
*
Make minor modifications to the Lean files
Son Ho
2023-06-04
3
-15
/
+14
|
*
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
44
-164
/
+415
|
*
Reorganize the Lean tests and extract the Polonius tests to Lean
Son Ho
2023-06-04
31
-8
/
+2365
|
*
Update the Nix flake
Son Ho
2023-06-04
1
-30
/
+51
|
*
Remove the symbolic interpreter tests
Son Ho
2023-06-04
2
-35
/
+0
|
*
Remove the tests/lean/hashmap_on_disk/Main.lean file
Son Ho
2023-06-04
1
-10
/
+0
|
*
Generate all the lakefile.lean files
Son Ho
2023-06-04
6
-0
/
+108
|
*
Automate the generation of the lakefile.lean files
Son Ho
2023-06-04
3
-127
/
+170
|
*
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
|
[next]