cargo creusot why3 ide does not launch after a successful cargo creusot

[Armael]

If I run cargo creusot and it terminates successfully, then running cargo creusot why3 ide immediately terminates "successfully" without launching why3ide.
This had me scrambling for a while trying to understand what was wrong with my installation of why3ide.

I guess this is caused by caching of build results performed by cargo, but I don't know where to start looking to fix the issue.

[xldenis]

I guess this is caused by caching of build results performed by cargo, but I don't know where to start looking to fix the issue.

Yea, there is a lot that needs improving here. Off the top of my head some things I think we should do:

1. Set a custom cargo target so that creusot artifacts are not built in target/debug but instead in creusot/debug or even potentially target/creusot (if we can figure out that second one). This would also potentially avoid trashing the cargo cache as often and make creusot-contracts more reliable when switching between rustc and creusot modes.
2. To better control caching of cargo, we can leverage the various cargo instructions which can be passed back up: https://doc.rust-lang.org/cargo/reference/build-scripts.html

[laurentder]

Currently, calling cargo creusot why3 ide will execute the cargo check command.

• On the first call, cargo check will execute creusot-rustc, which will launch why3 ide.
• On subsequent calls, if the source has not been modified, cargo check will not call creusot-rustc (you can see documention here). If creusot-rustc is not called, why3 ide will not be launched.

If the goal is to launch why3 ide, the approach of executing the cargo check command may not be the right one. Another approach might be to modify cargo creusot, when calling cargo creusot why3 ide. We could do this in two stages

• first run cargo check.
• then launch from cargo creusot why3 ide.

@xldenis, Is this approach right for you? Currently, when creusot-rustc launches why3 ide, it uses context information from its compilation (TranslationCtx, etc.). Is this information necessary to launch why3 ide?

To better control caching of cargo, we can leverage the various cargo instructions which can be passed back up: https://doc.rust-lang.org/cargo/reference/build-scripts.html

Cargo can compile a script and execute it just before building the package. This script (build.rs) can communicate with cargo by writing commands for cargo to its standard output. This allows cargo, for example, to determine whether it should rerun the script. However, this mechanism is executed before compilation. Here we would like to run it after compilation. I don't think Cargo has a script for the post-build stage

[xldenis]

Hmm I think cargo-creusot should be the one to run why3 ide, I would like creusot-rustc to have no particular knowledge of the ide or anything. Its responsibility is generating a text file, that's it. The workflow we want to build should be encapsulated by cargo creusot instead.

Do you think that would be possible?

[xldenis]

Reading over the implementation of run_why3 I think it should be possible, that file only uses ctx to do error reporting so we should be able to extract this into cargo-creusot instead.

[laurentder]

Do you think that would be possible?

It's too early to say, but I can start in this direction.

Reading over the implementation of run_why3 I think it should be possible, that file only uses ctx to do error reporting so we should be able to extract this into cargo-creusot instead.

Ok, I'll see what I can do about that.

[laurentder]

I just finished a first solution to this issue here.

• cargo-creusot can launch why3 now. For the moment, only in Ide mode. Prove and Replay mode are always launched via creusot-rustc. This maintains compatibility with these execution modes.

• The path to the generated mlcfg file has been modified. It is now placed at the root of the target directory, there is no longer any distinction between release and debug.
  Why: This path was built in creusot-rustc, we must now build it in cargo-creusot. cargo-creusot doesn't have as easy access to compilation information as creusot-rustc. Moreover we wanted to generate a file in the same location whether we are in Debug or Release.

[laurentder]

We added some changes to.

We have a problem if cargo-creusot set an mlcfg_filename with relative span_mode. In this situation, the relative path to the rust source file is misinterpreted by cargo-rustc, and why3 can't work fine.

creusot-rustc build the relative path in the relative_to_output function of the creusot/src/options.rs file.
With our modification, cargo-creusot call cargo-rustc with an output_file, not None as before.
The function relative_to_output doesn't seem to build the correct relative path in this situation.

We added a change in cargo-creusot to call creusot-rustc with absolute span_mode for now.

[jhjourdan]

Do we still want that proof and replay are launched by cargo-rustc? My understanding is that they would suffer from the same problem of caching as ide. Clearly, that's not what we want for replay, and probably not either for proof.

[jhjourdan]

The path to the generated mlcfg file has been modified. It is now placed at the root of the target directory, there is no longer any distinction between release and debug.

Does that mean that creusot should no longer be aware of the compilation mode? This is a bit weird, given that the compilation mode can semantically change the behavior of the compiler.

So, what do we prove? The program in debug or release mode?

[Armael]

Triage after the creusot meeting this morning:

• I'd be good indeed to move the prove and replay subcommands to be handled by cargo-creusot, following the refactoring done for ide. I'll open a separate issue to track this.
• regarding the debug/release compilation modes: the current status is that the .mlcfg file generated indeed may depend on the mode if the user used conditional compilation attributes that depend on this mode... But it's not completely clear how we would want to handle this in creusot or whether this is a reasonable usecase, so for now let's keep things as they are currently.