Workspace workflow not working without workarounds

[sarsko]

So the basis for this is the CreuSAT repo and making that up to date with current Creusot.

After setting up the repo for modern Creusot (why3find and the like):

If I run cargo creusot prove -- -p Friday I get:

why3find: Unknown file or directory "verif"
Error: 'why3find prove' failed

So I mkdir verif and try again:

❯ cargo creusot prove -- -p Friday
warning: virtual workspace defaulting to `resolver = "1"` despite one or more workspace members being on edition 2021 which implies `resolver = "2"`
note: to keep the current resolver, specify `workspace.resolver = "1"` in the workspace root's manifest
note: to use the edition 2021 resolver, specify `workspace.resolver = "2"` in the workspace root's manifest
note: for more details see https://doc.rust-lang.org/cargo/reference/resolver.html#resolver-versions
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.13s
Warning: found dangling files and directories:
  verif
Run 'cargo creusot clean' to remove them
Cache 0/0
Proofs ✔ (-) (none)
Provers 0ns

Which is obviously not correct. cding into Friday gives the same result.

If I now run cargo creusot why3 ide -- -p Friday, or cd Friday && cargo creusot why3 ide then the ide part doesnt work (shows blank), but verif/Friday_rlib/Friday gets populated.

I can now run

❯ cargo creusot prove -- -p Friday
warning: virtual workspace defaulting to `resolver = "1"` despite one or more workspace members being on edition 2021 which implies `resolver = "2"`
note: to keep the current resolver, specify `workspace.resolver = "1"` in the workspace root's manifest
note: to use the edition 2021 resolver, specify `workspace.resolver = "2"` in the workspace root's manifest
note: for more details see https://doc.rust-lang.org/cargo/reference/resolver.html#resolver-versions
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.07s
Library verif.Friday_rlib.Friday.M_set_next: ✔ (3)
Library verif.Friday_rlib.Friday.M_solve: ✔ (4)
Library verif.Friday_rlib.Friday.M_solver: ✔ (3)
Library verif.Friday_rlib.Friday.qyi12351366418665805374.M_eval: ✔ (4)
Library verif.Friday_rlib.Friday.qyi13632724450348951098.M_eval: ✔ (4)
Library verif.Friday_rlib.Friday.qyi28889722158515846.M_clone: ✔ (2)
Library verif.Friday_rlib.Friday.qyi28889722158515846.M_clone__refines: ✔ (1)
Library verif.Friday_rlib.Friday.qyi724589823354132597.M_clone: ✔ (3)
Library verif.Friday_rlib.Friday.qyi724589823354132597.M_clone__refines: ✔ (1)
Cache 34/34
Proofs ✔ (25)
 - fixed: 25
Provers 62ms (+62ms

Not that if I cd into Friday and try to verify just that then I get:

❯ cargo creusot why3 ide
warning: virtual workspace defaulting to `resolver = "1"` despite one or more workspace members being on edition 2021 which implies `resolver = "2"`
note: to keep the current resolver, specify `workspace.resolver = "1"` in the workspace root's manifest
note: to use the edition 2021 resolver, specify `workspace.resolver = "2"` in the workspace root's manifest
note: for more details see https://doc.rust-lang.org/cargo/reference/resolver.html#resolver-versions
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.07s
anomaly: Unix.Unix_error(Unix.ENOENT, "mkdir", "/Users/sarekhs/CreuSAT/Friday/./verif/Friday_rlib")

In other words: It seems to me that workspaces support has regressed a bit and has a bunch of sharp edges currently.

[sarsko]

Ran into some more issues after modernizing "Robinson" (the verified DPLL SAT solver):

❯ cargo creusot prove -i -- -p Robinson
warning: virtual workspace defaulting to `resolver = "1"` despite one or more workspace members being on edition 2021 which implies `resolver = "2"`
note: to keep the current resolver, specify `workspace.resolver = "1"` in the workspace root's manifest
note: to use the edition 2021 resolver, specify `workspace.resolver = "2"` in the workspace root's manifest
note: for more details see https://doc.rust-lang.org/cargo/reference/resolver.html#resolver-versions
    Checking Robinson v0.1.0 (/Users/sarekhs/CreuSAT/Robinson)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 1.16s
Library verif.Robinson_bin.Robinson.M_main: ✔ (1)
[Fibers] yield error (Sys_error("verif/Robinson_rlib/Robinson/assignments/qyi6009098895143538323/M_clone/why3session.xml: No such file or directory"))
[Fibers] yield error (Sys_error("verif/Robinson_rlib/Robinson/assignments/qyi6009098895143538323/M_new/why3session.xml: No such file or directory"))
[Fibers] yield error (Sys_error("verif/Robinson_rlib/Robinson/assignments/qyi6009098895143538323/M_find_unassigned/why3session.xml: No such file or directory"))
Library verif.Robinson_rlib.Robinson.assignments.qyi6009098895143538323.M_do_unit_propagation: ✔ (2)
why3find: verif/Robinson_rlib/Robinson/clause/qyi11616394435307458415/M_clause_from_vec/why3session.xml: No such file or directory
Error: 'why3find prove' failed

[sarsko]

This is what I get when I try do run the ide btw:

[sarsko]

Tried the "ide hack" again and got

❯ cargo creusot prove -i -- -p Robinson
warning: virtual workspace defaulting to `resolver = "1"` despite one or more workspace members being on edition 2021 which implies `resolver = "2"`
note: to keep the current resolver, specify `workspace.resolver = "1"` in the workspace root's manifest
note: to use the edition 2021 resolver, specify `workspace.resolver = "2"` in the workspace root's manifest
note: for more details see https://doc.rust-lang.org/cargo/reference/resolver.html#resolver-versions
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.09s
why3find: verif/Robinson_rlib/Robinson/assignments/qyi6009098895143538323/M_clone/why3session.xml: No such file or directory
Error: 'why3find prove' failed
~/CreuSAT creusot-upgrade* ❯ cargo creusot prove -i -- -p Robinson     

[Lysxia]

Does first running the command without -i avoid the "no such file ..." exception?

[sarsko]

That's what I do here right ?

[Lysxia]

1. I think verif wasn't being created because you had run cargo creusot previously (while upgrading your project), and then removed verif to clean up, and then ran cargo creusot again, which does nothing. You have to remove target/creusot to force a rebuild. Unfortunately that behavior comes from our piggy-backing on cargo, which doesn't provide an easy way to force rebuilds AFAIK.
2. cargo creusot why3 ide is indeed broken at the moment. (Fixed in #1521)
3. It's a bug in why3find that why3find prove -i fails when there are no pre-existing proof files. The current workaround is to first run cargo creusot prove without -i (possibly after removing target/creusot to force a rebuild), and then run cargo creusot prove -i to start the ide. (Fixed in https://git.frama-c.com/pub/why3find/-/merge_requests/174)
4. Another issue down the line is that Creusot should tell why3find to run only on packages selected by -p. A workaround for now is to also pass on the command line the verif/ subdirectory corresponding to the relevant crates.