index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
Files
Lines
*
Merge pull request #245 from AeneasVerif/son/update-lean
Son HO
2024-06-17
6
-14
/
+14
|
\
|
*
Merge branch 'main' into son/update-lean
Son Ho
2024-06-17
1
-12
/
+4
|
|
\
|
|
/
|
/
|
*
|
Merge pull request #249 from Nadrieril/github-ci
Guillaume Boisseau
2024-06-17
1
-12
/
+4
|
\
\
|
*
|
Revert "Switch to GitHub CI runners"
Nadrieril
2024-06-17
1
-12
/
+4
|
/
/
|
*
Merge branch 'main' into son/update-lean
Son Ho
2024-06-17
1
-4
/
+12
|
|
\
|
|
/
|
/
|
*
|
Merge pull request #248 from Nadrieril/bump-charon2
Guillaume Boisseau
2024-06-17
17
-22
/
+22
|
\
\
|
*
|
Update charon
Nadrieril
2024-06-17
17
-22
/
+22
|
/
/
*
|
Merge pull request #247 from Nadrieril/github-ci
Guillaume Boisseau
2024-06-17
1
-4
/
+12
|
\
\
|
*
|
Switch to GitHub CI runners
Nadrieril
2024-06-17
1
-4
/
+12
|
/
/
|
*
Regenerate the tests
Son Ho
2024-06-17
15
-18
/
+18
|
*
Update the Charon pin
Son Ho
2024-06-17
2
-4
/
+4
|
*
Update the Lean dependencies
Son Ho
2024-06-17
2
-8
/
+8
|
*
Update the tests
Son Ho
2024-06-14
2
-4
/
+4
|
*
Start updating Lean to 4.9.0-rc2
Son Ho
2024-06-14
2
-4
/
+4
|
/
*
Merge pull request #243 from AeneasVerif/son/update-lean
Son HO
2024-06-13
18
-168
/
+196
|
\
|
*
Update the tests
Son Ho
2024-06-13
4
-34
/
+29
|
*
Update Lean to v4.9.0-rc1
Son Ho
2024-06-13
15
-139
/
+172
|
/
*
Merge pull request #242 from AeneasVerif/son/scalars2
Son HO
2024-06-13
9
-114
/
+150
|
\
|
*
Fix more issues with the scalar notations
Son Ho
2024-06-13
1
-15
/
+29
|
*
Fix more issues
Son Ho
2024-06-13
3
-16
/
+22
|
*
Fix a proof
Son Ho
2024-06-13
1
-1
/
+1
|
*
Merge branch 'main' into son/scalars2
Son HO
2024-06-13
1
-1
/
+1
|
|
\
|
|
/
|
/
|
*
|
Merge pull request #238 from RaitoBezarius/prop-has-imp-sort
Son HO
2024-06-13
1
-1
/
+1
|
\
\
|
*
\
Merge branch 'main' into prop-has-imp-sort
Son HO
2024-06-12
5
-45
/
+118
|
|
\
\
|
|
/
/
|
/
|
|
|
*
|
feat: `PropHasImp` can have `Sort u` as premisses
Ryan Lahfa
2024-06-11
1
-1
/
+1
|
|
*
Merge branch 'main' into son/scalars2
Son HO
2024-06-12
0
-0
/
+0
|
|
|
\
|
|
_
|
/
|
/
|
|
*
|
|
Merge pull request #241 from AeneasVerif/son/tactics
Son HO
2024-06-12
5
-45
/
+118
|
\
\
\
|
|
/
/
|
/
|
|
|
|
*
Add an example
Son Ho
2024-06-12
1
-0
/
+3
|
|
*
Update the code extraction and regenerate the tests
Son Ho
2024-06-12
3
-9
/
+15
|
|
*
Update the scalar notations in Lean
Son Ho
2024-06-12
3
-102
/
+109
|
|
/
|
*
Revert "Update the scalar notation for the Lean backend"
Son Ho
2024-06-12
2
-26
/
+26
|
*
Revert "Regenerate the tests"
Son Ho
2024-06-12
12
-333
/
+338
|
*
Revert "Update CoreConvertNum.lean"
Son Ho
2024-06-12
1
-22
/
+22
|
*
Revert "Fix some mistakes"
Son Ho
2024-06-12
4
-17
/
+15
|
*
Fix some mistakes
Son Ho
2024-06-12
4
-15
/
+17
|
*
Update CoreConvertNum.lean
Son Ho
2024-06-12
1
-22
/
+22
|
*
Regenerate the tests
Son Ho
2024-06-12
12
-338
/
+333
|
*
Update the scalar notation for the Lean backend
Son Ho
2024-06-12
2
-26
/
+26
|
*
Deactivate the coercion from Nat to Scalar
Son Ho
2024-06-12
2
-0
/
+17
|
*
Slightly simplify the progress tactic
Son Ho
2024-06-12
1
-8
/
+4
|
*
Add wrappers around the rewriter
Son Ho
2024-06-12
1
-0
/
+61
|
*
Add the Simp.Config to the simp wrappers
Son Ho
2024-06-12
4
-37
/
+36
|
/
*
Merge pull request #237 from AeneasVerif/son/tuples
Son HO
2024-06-11
6
-28
/
+96
|
\
|
*
Deactivate the use of tuple projectors in the Lean backend
Son Ho
2024-06-11
3
-7
/
+12
|
*
Update the tests for tuples
Son Ho
2024-06-11
4
-22
/
+85
|
/
*
Merge pull request #232 from Nadrieril/type-alias
Guillaume Boisseau
2024-06-06
7
-12
/
+56
|
\
|
*
Filter out type aliases
Nadrieril
2024-06-06
7
-12
/
+56
|
/
*
Merge pull request #233 from AeneasVerif/son/borrow-check
Son HO
2024-06-06
45
-759
/
+1500
|
\
|
*
Regenerate the Coq and Lean betrees
Son Ho
2024-06-05
2
-178
/
+423
|
*
Fix a minor issue
Son Ho
2024-06-05
1
-0
/
+1
[next]