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
...
|
*
added a meta option field to norm_ctx and changed the meta used by some asser...
Escherichia
2024-03-28
8
-38
/
+35
|
*
Inverted meta and config argument orders (from meta -> config to config -> meta)
Escherichia
2024-03-28
20
-303
/
+303
|
*
Replaced some unclear TODOs error message placeholder by clearer TODOs, they ...
Escherichia
2024-03-28
4
-36
/
+36
|
*
Still need to fill the TODO: error message and check some meta but it builds
Escherichia
2024-03-28
10
-178
/
+186
|
*
WIP: translate.ml and extract.ml do not compile. Some assert left to do and w...
Escherichia
2024-03-28
45
-1885
/
+1947
|
*
WIP: does not compile yet because we need to propagate the meta variable.
Escherichia
2024-03-28
11
-223
/
+226
|
*
WIP Beginning working on better errors: began replacing raise (Failure) and a...
Escherichia
2024-03-28
15
-1032
/
+1076
*
|
Merge pull request #94 from RaitoBezarius/nix
Son HO
2024-03-29
2
-0
/
+10
|
\
\
|
|
/
|
/
|
|
*
project(installation): provide a default shell for `aeneas`
Ryan Lahfa
2024-03-21
1
-0
/
+9
|
*
shell(ux): enter into the default devshell via nix-direnv
Ryan Lahfa
2024-03-21
1
-0
/
+1
*
|
Merge pull request #96 from RaitoBezarius/bump-lean
Son HO
2024-03-25
2
-2
/
+2
|
\
\
|
|
/
|
/
|
|
*
backend(/tests)/lean: 4.6.0-rc1 → 4.6.1
Ryan Lahfa
2024-03-25
2
-2
/
+2
|
/
*
Merge pull request #93 from AeneasVerif/son/examples
Son HO
2024-03-20
45
-711
/
+846
|
\
|
*
Merge remote-tracking branch 'origin/main' into son/examples
Son Ho
2024-03-20
1
-3
/
+7
|
|
\
|
|
/
|
/
|
*
|
Merge pull request #90 from AeneasVerif/son/makefile
Son HO
2024-03-20
2
-9
/
+13
|
\
\
|
*
|
Change the tests target to test
Son Ho
2024-03-11
2
-6
/
+6
|
*
|
Update the Makefile to automatically reformat the code
Son Ho
2024-03-11
1
-3
/
+7
|
|
*
Update the Makefile
Son Ho
2024-03-20
2
-8
/
+8
|
|
*
Update the flake.lock
Son Ho
2024-03-20
1
-15
/
+15
|
|
*
Regenerate the code
Son Ho
2024-03-20
29
-454
/
+431
|
|
*
Improve the generation of pretty name and the micro passes
Son Ho
2024-03-20
8
-30
/
+144
|
|
*
Regenerate the tests
Son Ho
2024-03-19
22
-188
/
+80
|
|
*
Improve the pure micro passes
Son Ho
2024-03-19
2
-8
/
+64
|
|
*
Update the demo
Son Ho
2024-03-19
4
-30
/
+126
|
|
/
|
/
|
*
|
Merge pull request #92 from AeneasVerif/son/globals
Son HO
2024-03-18
18
-462
/
+506
|
\
\
|
*
|
Update the flake.nix and the flake.lock
Son Ho
2024-03-18
2
-367
/
+4
|
*
|
Fix a minor issue
Son Ho
2024-03-18
1
-1
/
+3
|
*
|
Regenerate the test files
Son Ho
2024-03-18
6
-66
/
+297
|
*
|
Update extract_trait_impl
Son Ho
2024-03-18
1
-7
/
+23
|
*
|
Fix the extraction of trait constants
Son Ho
2024-03-18
2
-35
/
+22
|
*
|
Regenerate the constants tests and update Primitives/Base.lean
Son Ho
2024-03-18
4
-55
/
+101
|
*
|
Make good progress on adding generics to global constants
Son Ho
2024-03-18
8
-47
/
+172
|
/
/
*
|
Merge pull request #91 from AeneasVerif/son/hax
Son HO
2024-03-17
16
-101
/
+75
|
\
\
|
|
/
|
/
|
|
*
Update the flake.lock
Son Ho
2024-03-17
1
-21
/
+21
|
*
Fix a minor issue
Son Ho
2024-03-17
1
-1
/
+1
|
*
Make minor updates
Son Ho
2024-03-17
3
-7
/
+14
|
*
Fix a small issue ollowing updates in Charon
Son Ho
2024-03-17
1
-3
/
+8
|
*
Update following changes in Charon
Son Ho
2024-03-17
11
-72
/
+34
|
/
*
Merge pull request #88 from AeneasVerif/son/clashes
Son HO
2024-03-11
37
-703
/
+825
|
\
|
*
Update the flake.lock
Son Ho
2024-03-11
1
-12
/
+12
|
*
Regenerate the test files
Son Ho
2024-03-11
14
-244
/
+227
|
*
Simplify the generated names
Son Ho
2024-03-11
1
-14
/
+25
|
*
Update the generated files
Son Ho
2024-03-11
15
-380
/
+389
|
*
Update tests/Makefile
Son Ho
2024-03-11
1
-1
/
+1
|
*
Update the generation of names
Son Ho
2024-03-11
7
-39
/
+57
|
*
Update a builtin name
Son Ho
2024-03-11
1
-1
/
+1
|
*
Update the builtin name patterns
Son Ho
2024-03-10
1
-23
/
+66
|
*
Update the name generation and add CLI to print external pat names
Son Ho
2024-03-10
7
-48
/
+106
|
/
*
Merge pull request #85 from AeneasVerif/son/fix_loops3
Son HO
2024-03-09
28
-350
/
+1185
|
\
|
*
Update the flake.lock
Son Ho
2024-03-09
1
-24
/
+24
[prev]
[next]