aeneas

aeneas copied to clipboard

Turn the ICFP tutorial into a Lean game

3

We can either self-host the game, implying some sysadmin, or we can reach out to the Lean community to add our own game. Docs on how to create a game:...

RaitoBezarius

Update the comment for `TypesUtils.ty_is_copyable`

2

https://github.com/AeneasVerif/charon/blob/a0c861ca28c34c72e43b55467f09bbfbafc7fb20/charon-ml/src/TypesUtils.ml#L209 The comment should explain why we keep the function: - it is used in the code of Aeneas exactly where we need to check that a type is copyable...

sonmarcho

We did the change in Charon, but there are also occurrences of the word "assumed" in Aeneas-specific files

sonmarcho

test(bst): add BST as an example

4

This adds BST as an example from my internship's staging repository. It adds a bunch of unit tests for them.

RaitoBezarius

Sometimes, when unfolding via `simp` or `unfold`, the resulting term is the fixed point and the unfolding theorem is not applied to obtain the nice code form. Workaround is to...

RaitoBezarius

Give the possibility of extracting the source code as comments

1

This follows from https://github.com/AeneasVerif/charon/pull/327

sonmarcho

The `progress` tactic has quite a few limitations, including: - it doesn't work on trait methods: we need to design a way of packing specifications for trait methods together, and...

sonmarcho

If we write: ```lean let (x, y) := ... f x y ``` the definition often gets desugared to something of the shape: ``` let __discr := ... f __discr.1...

sonmarcho

The call to `simp_all` in `scalar_tac` seems to loop at times, or at least take a lot more time than expected. For this reason, we set a low number of...

sonmarcho

See the README in the Loogle repo: https://github.com/nomeata/loogle/tree/master

sonmarcho