Lucas Franceschino comments

Results 275 comments of


                                            Lucas Franceschino

Phase setup hard to use

Yes, when OCaml cannot unify two module signatures, the error it prints is very very verbose and hard to read... We want to have more docs on those, see https://github.com/cryspen/hax/issues/1141....

Engine: name clash for items within trait methods

This was **not** fixed by #1199

Engine: name clash for items within trait methods

This issue doesn't reproduce on `main`. The original example hits another unrelated problem though: the fact one cannot impl `Clone` manually. The original example is as follows: ```rust struct A;...

Engine: name clash for items within trait methods

Sounds good, let's close then!

`-i` flag doesn't work correctly with ProVerif backend

@jschneider-bensch do you think you could retry this and find a reproducer here? (even a large one)

Unsupported Rust: range patterns

@maximebuyse, that's probably something you will want to look at, that should be fairly simple to add on top of #878!

`let else` patterns with panic do not lax-check in F*

Still relevant

Rust engine: errors resugaring.

Let's keep this PR alive: we will use it and merge it as soon as the Rust engine itself produces errros.

ProVerif queries from a hax-lib annotation

Should be fixed as a larger pass on the annotation language in general.

Mutable Variable and Function analysis are using String instead of Concrete Ident

I think this is still relevant