Lucas Franceschino comments

Results 275 comments of


                                            Lucas Franceschino

`cargo-hax`: add a `--single-file` to `cargo hax`

Still useful

[Lean] Panic-freedom tutorial example is broken

Thanks for the report! Just a note: the tutorial examples [are actually in CI already](https://github.com/cryspen/hax/pull/1690), but the job is failing (see e.g. https://github.com/cryspen/hax/actions/runs/18826038396). That CI job checks the website of...

Engine: warn if a name of the current crate is used but not defined

Would still be nice to have, let's reopen for the Rust engine

Frontend: THIR: missing `impl_expr` on `GlobalName`

Yes, that's what I had in mind as "similar fields" ^^

Write This Month in Hax

Release is currently waiting for #1742 to be merged

Engine: better debugging infrastructure

Let's close this one, it's very OCaml specific actually.

Trait implementation has extra _super variable

Thanks for the report! Seems like I can't reproduce a standalone example easily: ```rust trait KeccakItem {} pub(crate) trait Squeeze1 { fn squeeze(&self, out: &mut [u8], start: usize, len: usize);...

Trait implementation has extra _super variable

Looking at `libcrux-sha3/10fbd6f06ad9ba52138e0` on hax `main`, `./hax.py extract` gives me a `Libcrux_sha3.Traits.fsti` that contains: ```fstar /// Trait to squeeze bytes out of the state. /// Note that this is implemented...

Trait implementation has extra _super variable

@Parrot7483, do you think this issue is still relevant? If so, could you write a Rust reproducer for it?

Organise Helper/Macro libraries

Still relevant!