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
/
Extract.ml
(
follow
)
Commit message (
Expand
)
Author
Age
Files
Lines
...
*
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
1
-14
/
+21
*
Improve simplify_aggregates to introduce structure updates
Son Ho
2023-06-04
1
-1
/
+7
*
Add a special expression for structure creation/update
Son Ho
2023-06-04
1
-51
/
+54
*
Update the extraction of Lean files
Son Ho
2023-06-04
1
-14
/
+28
*
Reorganize the Lean tests and extract the Polonius tests to Lean
Son Ho
2023-06-04
1
-1
/
+1
*
Handle the "opaque_defs." prefix in a cleaner manner
Son Ho
2023-06-04
1
-31
/
+70
*
Make minor modifications
Son Ho
2023-06-04
1
-41
/
+89
*
Consistently use the names TerminationMeasure and DecreasesProof
Son Ho
2023-06-04
1
-16
/
+33
*
Update the generation of termination and decreases_by templates for Lean
Son Ho
2023-06-04
1
-23
/
+30
*
WIP
Jonathan Protzenko
2023-06-04
1
-3
/
+6
*
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
1
-41
/
+48
*
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
1
-124
/
+135
*
All of the generated code is syntactically correct
Jonathan Protzenko
2023-06-04
1
-4
/
+5
*
WIP
Jonathan Protzenko
2023-06-04
1
-2
/
+8
*
Fix runaway indentation
Jonathan Protzenko
2023-06-04
1
-4
/
+4
*
Fill out more of the primitives file, attempt at type classes for scalar_cast
Jonathan Protzenko
2023-06-04
1
-10
/
+15
*
Don't need extra variables for the decreases clauses
Jonathan Protzenko
2023-06-04
1
-3
/
+9
*
WIP printing proper clauses
Jonathan Protzenko
2023-06-04
1
-3
/
+58
*
Fix some printing bits, proper syntax for terminates and decreases clauses
Jonathan Protzenko
2023-06-04
1
-15
/
+136
*
WIP lots of stuff
Jonathan Protzenko
2023-06-04
1
-9
/
+17
*
Fix a syntax error
Jonathan Protzenko
2023-06-04
1
-2
/
+6
*
Custom syntax support for structures in Lean
Jonathan Protzenko
2023-06-04
1
-9
/
+34
*
More cosmetic improvements
Jonathan Protzenko
2023-06-04
1
-12
/
+20
*
Fix a couple bugs here and there, improve Lean code-gen, still WIP
Jonathan Protzenko
2023-06-04
1
-9
/
+30
*
New directory structure and corresponding extraction, + misc fixes, for Lean
Jonathan Protzenko
2023-06-04
1
-12
/
+11
*
Write a tactic to discharge integer literal proof obligations
Jonathan Protzenko
2023-06-04
1
-1
/
+1
*
Initial Lean backend, WIP
Jonathan Protzenko
2023-06-04
1
-91
/
+197
*
Fix an issue with the names of the loop decreases clauses
Son Ho
2023-02-03
1
-3
/
+4
*
Fix various issues with the generation of code for the loops
Son Ho
2023-02-03
1
-11
/
+18
*
Add a `Loop` node in the pure AST
Son Ho
2023-02-03
1
-0
/
+3
*
Introduce new loop ids in Pure and keep track of the number of loops in a fun...
Son Ho
2023-02-03
1
-3
/
+4
*
Add loop ids to the pure functions identifiers
Son Ho
2023-02-03
1
-4
/
+10
*
Generate record field projectors for Coq
Son Ho
2022-11-16
1
-71
/
+228
*
Improve formatting
Son Ho
2022-11-16
1
-95
/
+116
*
Make minor modifications to the extraction
Son Ho
2022-11-16
1
-4
/
+13
*
Extract the Polonius examples in Coq
Son Ho
2022-11-14
1
-13
/
+16
*
Add a `-use-fuel` option
Son Ho
2022-11-14
1
-7
/
+22
*
Make [Result::Failure] type an [Error] parameter
Son Ho
2022-11-14
1
-1
/
+12
*
Improve the formatting of [if then else] expressions
Son Ho
2022-11-14
1
-15
/
+24
*
Improve the formatting of the generated code
Son Ho
2022-11-14
1
-33
/
+47
*
Make good progress on the Coq backend
Son Ho
2022-11-14
1
-0
/
+2001
[prev]