Skip to content

Conversation

@jaylorch
Copy link
Member

@jaylorch jaylorch commented Dec 1, 2025

No description provided.

@hayley-leblanc
Copy link
Collaborator

I'm testing this on WSL with cargo verus verify and running into errors on all three of CapybaraKV, multilog, and pmemlog. I tried cargo clean, rustup update, and updating the rust-toolchain.toml file for CapybaraKV to use the nightly-2025-09-01 toolchain version (which corresponds to Rust 1.91.0, which I think is the current version used by Verus?) but none resolved the errors.

The errors are all either missing traits or unresolved imports for types in core::marker. E.g.:

error[E0432]: unresolved import `core::marker::PointeeSized`
 --> /home/hayley/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/vstd-0.0.0-2025-11-30-0053/std_specs/cmp.rs:6:5
  |
6 | use core::marker::PointeeSized;
  |     ^^^^^^^^^^^^^^------------
  |     |             |
  |     |             help: a similar name exists in the module: `PointerLike`
  |     no `PointeeSized` in `marker`

and

error[E0405]: cannot find trait `MetaSized` in module `core::marker`
   --> /home/hayley/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/vstd-0.0.0-2025-11-30-0053/std_specs/ops.rs:53:31
    |
53  |               pub trait $extrait<Rhs = Self> {
    |                                 ^^^^^^^^^^^^ not found in `core::marker`
...
109 | / def_bin_ops_spec!(
110 | |     core::ops::Sub,
111 | |     ExSub,
112 | |     SubSpec,
...   |
117 | |     sub_spec
118 | | );
    | |_- in this macro invocation
    |
    = note: this error originates in the macro `def_bin_ops_spec` (in Nightly builds, run with -Z macro-backtrace for more info)

Did you run into these when updating the Verus version for this PR?

@jaylorch
Copy link
Member Author

jaylorch commented Dec 1, 2025

Ah, thanks, I was missing some other places where the Rust version was specified as 1.88.0 rather than the 1.91.0 that modern Verus uses. It now works for me on WSL. Could you please try again?

@hayley-leblanc
Copy link
Collaborator

As a note for anyone who may come across this in the future: I had to run cargo update and pull/rebuild my local version of Verus to get this to work.

@jaylorch jaylorch merged commit e39a2a2 into main Dec 1, 2025
5 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants