trouble proving derive PartialEq with v0.1

[Emilie-Thome]

Unless I did something wrong, I can not prove #[derive(creusot_contracts::prelude::PartialEq)] with why3 and Creusot v0.1.
Here is an extract of something I want proved:

use creusot_contracts::{ensures, logic, open, prelude, requires, DeepModel};
#[derive(prelude :: Clone, Copy, prelude :: PartialEq, prelude :: Default, DeepModel)]
pub enum Braking {
    #[default]
    NoBrake,
    SoftBrake,
    UrgentBrake,
}

To my knowledge, only the PartialEq is not proved by why3.

[xldenis]

Hmm, that's weird, I'm not able to reproduce the issue, can you provide exactly the commands that you used to create the files ?

[Emilie-Thome]

Yep, it's cargo creusot why3 ide.
I reproduced it with another computer (but it's still the same person who runs it, me...).

[xldenis]

That's the whole file?

[Emilie-Thome]

That's the whole file?

Yes, that's my lib.rs file. There is nothing else in src/.

[Emilie-Thome]

test_creusot.txt
Here is the mlcfg file, in case it might help.
(I just converted it into a txt because github does not want to attach mlcfg files.)

[xldenis]

Aha, this is an occurence of #1014. We need to backport this patch and push a v0.1.1

[xldenis]

Until 0.1.1 comes out you can use the stable branch instead. Note: you need to manually implement Default since we don't actually handle that one automatically.

[Emilie-Thome]

Ok thanks a lot!