Use vstd only with --features verus

Author: jaylorch

.dir-locals.el

@@ -0,0 +1,12 @@
+;;; Directory Local Variables            -*- no-byte-compile: t; -*-
+;;; For more information see (info "(emacs) Directory Variables")
+
+;; Regorus is a cargo-verus project (package.metadata.verus.verify = true), so
+;; verus-mode.el runs `cargo verus verify' rather than the raw `verus' binary.
+;; The cargo-verus path ignores `package.metadata.verus.ide.extra_args' and
+;; instead reads `verus-cargo-verus-arguments'. We set it here so that Verus is
+;; invoked with the `verus' Cargo feature enabled.
+;;
+;; Everything before `--' is passed to cargo-verus; everything after `--' is
+;; forwarded to the Verus binary. The `--' is required by verus-mode.el.
+((verus-mode . ((verus-cargo-verus-arguments . ("--features" "verus" "--")))))

.github/workflows/verus.yml

@@ -74,4 +74,4 @@ jobs:
         export PATH="$(cd "$(dirname "$cargo_verus_bin")" && pwd):$(cd "$(dirname "$verus_bin")" && pwd):$PATH"
         cargo verus --help
         cargo fetch --locked
-        cargo verus verify --locked
+        cargo verus verify --locked --features verus

Cargo.toml

@@ -26,6 +26,7 @@ doctest = false
 
 [features]
 default = ["full-opa", "arc", "rvm"]
+verus = ["dep:vstd"]
 
 arc = []
 ast = []
@@ -48,7 +49,7 @@ cache = ["dep:lru"]
 rvm = ["dep:postcard", "dep:indexmap"]
 semver = ["dep:semver"]
 allocator-memory-limits = ["std", "mimalloc", "mimalloc/allocator-memory-limits"]
-std = ["rand/std", "rand/std_rng", "serde_json/std", "indexmap?/std", "msvc_spectre_libs", "dep:parking_lot", "vstd/std" ]
+std = ["rand/std", "rand/std_rng", "serde_json/std", "indexmap?/std", "msvc_spectre_libs", "dep:parking_lot", "vstd?/std" ]
 time = ["dep:chrono", "dep:chrono-tz"]
 uuid = ["dep:uuid"]
 urlquery = ["dep:url"]
@@ -142,7 +143,7 @@ postcard = { version = "1.1.3", default-features = false, features = ["alloc"],
 # Verus-related dependencies.
 # vstd is always enabled. In no_std builds only the `alloc` feature is used; the
 # crate's `std` feature enables `vstd/std` (which matches vstd's default features).
-vstd = { version = "=0.0.0-2026-06-14-0213", default-features = false, features = ["alloc"] }
+vstd = { version = "=0.0.0-2026-06-14-0213", optional = true, default-features = false, features = ["alloc"] }
 
 [dev-dependencies]
 anyhow = "1.0.102"