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 (
Collapse
)
Author
Age
Files
Lines
*
Make progress on Extract and ExtractBase
Son Ho
2023-08-31
3
-52
/
+132
|
*
Update TranslateCore and factor out some definitions in PrintPure
Son Ho
2023-08-31
2
-42
/
+42
|
*
Finish updating SymbolicToPure.ml
Son Ho
2023-08-31
4
-115
/
+212
|
*
Start adding support for traits
Son Ho
2023-08-31
31
-776
/
+1258
|
*
Add tests which use const generics as values
Son Ho
2023-08-18
2
-2
/
+5
|
*
Update following the introduction of ConstantExpr
Son Ho
2023-08-18
16
-143
/
+220
|
*
Make a minor modification
Son Ho
2023-08-17
1
-11
/
+0
|
*
Update the code following a refactor on Charon's side
Son Ho
2023-08-08
4
-12
/
+27
|
*
Change some fun id names to use "Mut"/"Shared" as a suffix
Son Ho
2023-08-07
5
-66
/
+66
|
*
Add an option to not override Hashmap.lean
Son Ho
2023-08-04
3
-2
/
+15
|
*
Fix issues with the extraction and extend the primitive libraries for Coq and F*
Son Ho
2023-08-04
2
-12
/
+12
|
*
Add SliceLen as a primitive function and make minor adjustments
Son Ho
2023-08-04
5
-35
/
+62
|
*
Start adding support for Arrays/Slices in the Lean library
Son Ho
2023-08-04
1
-10
/
+12
|
*
Fix an issue with the extraction of aggregated arrays
Son Ho
2023-08-03
10
-180
/
+320
|
*
Make a minor formatting modification for Lean
Son Ho
2023-08-03
1
-1
/
+1
|
*
Fix issues
Son Ho
2023-08-03
10
-57
/
+139
|
*
Make minor modifications
Son Ho
2023-08-02
3
-16
/
+29
|
*
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
|
[next]