cargo creusot ignores source code changes

[champignoom]

After running cargo creusot, target/debug/ is created, where there's the mlcfg file.

But then if one modifies the code and run cargo creusot again, nothing in target/debug/ is changed.

Of course, one can remove target/ before running cargo creusot each time, but that causes unnecessary recompilation of creusot-contract, pearlite-syn, unicode-indent, and other external crates. Is there a more effective workflow than this?

Thanks.

[xldenis]

Sorry, I thought I had already answered but I guess my answer never went through.

It's weird because it should be picking up your source code changes, it does it my personal projects using cargo creusot. Could you post exactly the command and set up of your project?

as a short term patch you can also do cargo clean -p crate-name to avoid cleaning everything that way only your final crate is cleaned.

[champignoom]

The problem seems to be reproduced only when creusot_contracts::* is not used, so:

extern crate creusot_contracts;
use creusot_contracts::*;

fn main() {
    // proof_assert!(true);
    let a = 9811111i32;
    let b = a*a;
}

With the proof_assert! commented out, cargo creusot ignores any change on the value of a and leaves the mlcfg file unchanged.

[xldenis]

Huh, that is odd? I'm not sure where to start digging. I think perhaps the best thing we could do is fully seperate the cargo creusot and cargo build directories. Could you try seeing if using CARGO_TARGET_DIR helps?

1. CARGO_TARGET_DIR=foo cargo creusot
2. Make change
3. CARGO_TARGET_DIR=foo cargo creusot
4. Updated output?

[champignoom]

Tried in vain.

And it's becoming weirder. It looks like the problem is only reproduced when using vscode to edit the source. If I edit it with sed -i or nvim for example, the problem disappears.

[champignoom]

OK, I'm not sure why but touch src/main.rs && cargo creusot fixes the problem.

[champignoom]

According to the result ofstat src/main.rs, vscode does update the atime and ctime when src/main.rs is edited, so touch src/main.rs shouldn't have made that much of a difference.

I'm not sure if this is a problem of macos or vscode or creusot, but cargo run does not suffer from this problem.

[xldenis]

Well, Creusot doesn't actually do dependency management itself, it uses cargo for that. It's possible we're doing something wonky but apart from sharing the target dir I have no idea what that could be.