Son HO

The unit tests in HOL4 are slow: investigate and fix this.

HOL4 only supports uniform polymorphism, which is not granted by Rust: it would be good to check this, and at least print a warning if the functions we translate/the generated...

This generates an error: ``` const S: &str = "Hello"; ``` Error: ``` Unsupported constant: "ConstValue::Slice: Slice { data: ConstAllocation { .. }, start: 0, end: 98 }" ```

Add support for quantified lifetimes (`for <'a>`)

1

For now Charon does not support quantified lifetimes, as indicated by `for

Check in CI that the build doesn't generate warnings

1

It can happen that the compilation generates warnings (for instance, clippy warnings): I want to make sure it doesn't happen (i.e., all warnings are addressed before we merge).

The Makefiles are getting bloated, especially for the tests, and are hard to maintain especially for people who are not used to writing makefiles. It would be better to have...

Update the comment for `TypesUtils.ty_is_copyable`

1

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...

Turn charon into a subcommand

2

We want to be able to run `cargo charon`