[cargo-verus] docs: improve instructions about migrating an existing project (#2632)

Author: mkovaxx

source/docs/guide/src/cargo_verus.md

@@ -33,21 +33,47 @@ This creates a new directory with a correctly-configured `Cargo.toml`, an initia
 
 ## Updating an existing Rust project to support Verus
 
-To enable verification for one or more of the crates in your project,
-add the following to each of their `Cargo.toml` files:
+To enable verification for one or more of the crates in your project, add `vstd` as a
+dependency as follows:
+
+```sh
+cargo add vstd
+```
+
+Then import the Verus prelude in each root module (e.g. `lib.rs` or `main.rs`):
+
+```rust
+use vstd::prelude::*;
+```
+
+To opt a crate into verification, include the following in its `Cargo.toml`:
 
 ```toml
 [package.metadata.verus]
 verify = true
+```
+
+If the crate is not in a workspace, also add the following to suppress warnings
+about `cfg(verus_only)`:
 
+```toml
 [lints.rust]
 unexpected_cfgs = { level = "warn", check-cfg = ['cfg(verus_only)'] }
 ```
+
 See below for more details.
 
 Note that you can still use normal `cargo` commands (e.g., `cargo build`) on
 crates and projects that include Verus annotations.
 
+## The Verus prelude
+
+Each verified crate needs to import the Verus prelude as follows:
+
+```rust
+use vstd::prelude::*;
+```
+
 ## Cargo.toml configuration
 
 Crates that should be verified must opt in by adding a `[package.metadata.verus]`
@@ -72,6 +98,21 @@ unexpected_cfgs = { level = "warn", check-cfg = ['cfg(verus_only)'] }
 `cargo verus new` adds this automatically. See [Ghost Erasure](./erasure.md) for a full
 explanation of `verus_only` and when to use it.
 
+In a Cargo workspace, you should instead include the following in the root `Cargo.toml`:
+
+```toml
+[workspace.lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(verus_only)'] }
+```
+
+Then ensure that each member crate's `Cargo.toml` has the following (which e.g. `cargo new` adds
+automatically):
+
+```toml
+[lints.rust]
+workspace = true
+```
+
 ## Subcommands
 
 ### `cargo verus verify`
@@ -124,7 +165,7 @@ Note that Verus-annotated code can also be built with a normal `cargo build` com
 
 Arguments are split around `--`:
 
-- **Before `--`**: forwarded to `cargo` 
+- **Before `--`**: forwarded to `cargo`
 - **After `--`**: forwarded to every `verus` invocation
 
 ```bash

source/rust_verify/src/util.rs

@@ -364,7 +364,7 @@ where
 
 pub(crate) fn no_builtin_err(span: &vir::messages::Span) -> VirErr {
     vir::messages::error(span,
-        "Error: The verus_builtin crate was not imported. This is usually imported via `vstd`, and it is necessary to run Verus.")
+        "Error: The verus_builtin crate was not imported but it is necessary to run Verus. You likely need to add `use vstd::prelude::*;` at the top of a lib.rs or main.rs file.")
     .help("For getting started with Verus, see: https://verus-lang.github.io/verus/guide/getting_started.html")
 }