Frustrating experience on first install

[xldenis]

I've been trying to get Creusot working on a fresh computer (see #1332, which was solved by installing Rosetta 2).

I created a new rust project and attempted to run creusot and got:

λ(church) balancing-proof → git master cargo creusot
Error: Why3 has version 1.8.0, expected version is 1.7.2
Error: why3find has version 1.1.1, expected version is 1.0.0
Error: Please run 'cargo creusot setup status' to diagnostic and fix the issue(s)
λ(church) balancing-proof → git master cargo creusot setup status
Creusot installation found.
=== INSTALLATION
Why3:
- path: /Users/xavier/.opam/default/bin/why3
- check_version: true
Alt-Ergo:
- mode: builtin
- check_version: true
Z3:
- mode: builtin
- check_version: true
CVC4:
- mode: builtin
- check_version: true
CVC5:
- mode: builtin
- check_version: true
=== PATHS
config: /Users/xavier/Library/Application Support/creusot.creusot
data:   /Users/xavier/Library/Application Support/creusot.creusot
cache:  /Users/xavier/Library/Caches/creusot.creusot

Error: Why3 has version 1.8.0, expected version is 1.7.2
Error: why3find has version 1.1.1, expected version is 1.0.0

I check my opam env, no issue:

opam install . --deps-only
[WARNING] Failed checks on creusot-deps package definition from source at git+file:///Users/xavier/Code/creusot#closure-infer-new-new-new:
  warning 35: Missing field 'homepage'
  warning 36: Missing field 'bug-reports'
  warning 68: Missing field 'license'
Nothing to do.

Out of ideas I rebuild cargo-creusot which fixes it for some reason? I go back to my project and:

λ(church) balancing-proof → git master cargo creusot
creusot-rustc not found (expected at "/Users/xavier/Library/Application Support/creusot.creusot/toolchains/nightly-2024-07-25/bin/creusot-rustc")
Run 'cargo creusot setup install' in the source directory of Creusot to install creusot-rustc

Running the command in the creusot source directory has no effect.

[xldenis]

The issue seems to be that creusot-rustc was never installed at all, in fact the toolchains/ directory wasn't even created?

[xldenis]

Manually running the correct cargo install --path creusot-rustc seemed to have solved the issue.

[xldenis]

λ(church) balancing-proof → git master * cargo creusot init
File 'Cargo.toml' already exists. (Skipped)
File 'rust-toolchain' already exists. (Skipped)
λ(church) balancing-proof → git master * cargo creusot
    Checking balancing-proof v0.1.0 (/Users/xavier/Code/balancing-proof)
error[E0432]: unresolved import `creusot_contracts`
 --> src/lib.rs:2:5
  |
2 | use creusot_contracts::*;
  |     ^^^^^^^^^^^^^^^^^ use of undeclared crate or module `creusot_contracts`

error: cannot find attribute `requires` in this scope
 --> src/lib.rs:4:3
  |
4 | #[requires(a@ < i64::MAX@)]
  |   ^^^^^^^^

error: cannot find attribute `ensures` in this scope
 --> src/lib.rs:5:3
  |
5 | #[ensures(result@ == a@ + 1)]
  |   ^^^^^^^

warning: unexpected `cfg` condition name: `creusot`
 --> src/lib.rs:1:17
  |
1 | #![cfg_attr(not(creusot), feature(stmt_expr_attributes, proc_macro_hygiene))]
  |                 ^^^^^^^
  |
  = help: expected names are: `clippy`, `debug_assertions`, `doc`, `docsrs`, `doctest`, `feature`, `miri`, `overflow_checks`, `panic`, `proc_macro`, `relocation_model`, `rustfmt`, `sanitize`, `sanitizer_cfi_generalize_pointers`, `sanitizer_cfi_normalize_integers`, `target_abi`, `target_arch`, `target_endian`, `target_env`, `target_family`, `target_feature`, `target_has_atomic`, `target_has_atomic_equal_alignment`, `target_has_atomic_load_store`, `target_os`, `target_pointer_width`, `target_thread_local`, `target_vendor`, `test`, `ub_checks`, `unix`, and `windows`
  = help: consider using a Cargo feature instead
  = help: or consider adding in `Cargo.toml` the `check-cfg` lint config for the lint:
           [lints.rust]
           unexpected_cfgs = { level = "warn", check-cfg = ['cfg(creusot)'] }
  = help: or consider adding `println!("cargo::rustc-check-cfg=cfg(creusot)");` to the top of the `build.rs`
  = note: see <https://doc.rust-lang.org/nightly/rustc/check-cfg/cargo-specifics.html> for more information about checking conditional configuration
  = note: `#[warn(unexpected_cfgs)]` on by default

For more information about this error, try `rustc --explain E0432`.
warning: `balancing-proof` (lib) generated 1 warning
error: could not compile `balancing-proof` (lib) due to 3 previous errors; 1 warning emitted

cargo creusot init generates a lib.rs which is undesired.

[xldenis]

cargo creusot does something without error but cargo creusot prove says

    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.00s
why3find: Unknown file or directory "verif"
Error: 'why3find prove' failed

[xldenis]

On the suspicion this was caused by the creusot_contracts crate not being present, I added it to the dependencies and got:

error: The `creusot_contracts` crate is loaded, but the following items are missing: creusot_invariant_internal, creusot_resolve, creusot_structural_resolve, creusot_invariant_user, creusot_resolve_method, snapshot_new, snapshot_from_fn, snapshot_inner, snapshot_deref, ghost_box_new, ghost_from_fn, ghost_box_into_inner, ghost_box_inner_logic, ghost_box_deref, ghost_box_deref_mut, creusot_index_logic_method, fn_once_impl_precond, fn_once_impl_postcond, fn_mut_impl_postcond, fn_mut_impl_unnest, fn_impl_postcond, creusot_int, snapshot_ty, ghost_box. Maybe your version of `creusot-contracts` is wrong?

[xldenis]

I suspect that the issue with cargo creusot setup install has to do with paths in spaces which is the case for macOS (since that's where creusot files get stored).

[xldenis]

Ok the issue was actually because I didn't use creusot_contracts::* anywhere so it wasn't actually being loaded by rustc.

[xldenis]

Now that I've gotten things compiling, I'm greeted by a ton of errors arising from extern_specs. It really makes me wish that we could make these "optional" so you don't get the spec if the conditions aren't met but you don't get 100000 errors. I just wanted to see something run.

It especially frustrating because here the issue is a missing DeepModel but I don't actually care about specifying that, I just want to say there exists some order on this type.

[Lysxia]

Running the command in the creusot source directory has no effect.

I'd like to have a closer look here because I would expect something to happen, at least an error message. So that's a bug.

The other issues from cargo creusot init onwards are TODOs.