Merge branch 'main' into release

Author: parno

CONTRIBUTING.md

@@ -30,7 +30,10 @@ JSON file to see where the automatically copied portion appears.
 
 If you update the config! settings in `crates/rust-analyzer/src/config.rs`, you
 need to run:
-`cargo test -p rust-analyzer generate_package_json_config generate_config_documentation`
+```
+cargo test -p rust-analyzer generate_package_json_config
+cargo test -p rust-analyzer generate_config_documentation
+```
 to update the `package.json` file and the documentation (which we don't currently publish).
 
 

README.md

@@ -87,7 +87,7 @@ where the quoted string is a list of space-separated Verus arguments, e.g., `ext
 
 #### Using `cargo verus`
 
-By default, `verus-analyzer` direclyt invokes the Verus executable on the root of your crate. If you would
+By default, `verus-analyzer` directly invokes the Verus executable on the root of your crate. If you would
 instead prefer to have it invoke `cargo verus`, toggle the setting: "Verus-analyzer › Cargo: Verus Enable".
 
 #### Advanced Verus Developments

crates/flycheck/src/lib.rs

@@ -97,6 +97,7 @@ pub enum FlycheckConfig {
         verus_args: Vec<String>,
         cargo_verus_enable: bool,
         cargo_options: CargoOptions,
+        report_all_errors: bool,
     },
 }
 
@@ -107,8 +108,8 @@ impl fmt::Display for FlycheckConfig {
             FlycheckConfig::CustomCommand { command, args, .. } => {
                 write!(f, "{command} {}", args.join(" "))
             }
-            FlycheckConfig::VerusCommand { verus_args, cargo_verus_enable, cargo_options } => {
-                write!(f, "verus {} (cargo_verus enabled: {}, cargo_verus options {:?})", verus_args.join(" "), cargo_verus_enable, cargo_options)
+            FlycheckConfig::VerusCommand { verus_args, cargo_verus_enable, cargo_options, report_all_errors } => {
+                write!(f, "verus {} (cargo_verus enabled: {}, cargo_verus options {:?}, report all errors: {})", verus_args.join(" "), cargo_verus_enable, cargo_options, report_all_errors)
             }
         }
     }
@@ -546,7 +547,7 @@ impl FlycheckActor {
     }
 
     // copied from above check_command
-    fn run_cargo_verus(&self, file: String, verus_args: &Vec<String>, cargo_options: &CargoOptions) -> Command {
+    fn run_cargo_verus(&self, file: String, verus_args: &Vec<String>, cargo_options: &CargoOptions, report_all_errors: bool) -> Command {
         // Find the `cargo-verus` binary
         let verus_binary_str = match std::env::var("VERUS_BINARY_PATH") {
             Ok(path) => path,
@@ -627,21 +628,27 @@ impl FlycheckActor {
             module_args.push("--verify-root".to_string());
         }
 
+        // Cargo command
         cmd.arg("verify".to_string());
+        // Provide the cargo arguments
         cmd.arg("--message-format=json".to_string());
         cargo_options.apply_on_command(&mut cmd);
+        cmd.args(&cargo_options.extra_args);
+        // Provide the Verus arguments
         cmd.arg("--".to_string());
         cmd.args(verus_args);
         cmd.args(extra_args_from_toml);
-        cmd.args(module_args);
+        if !report_all_errors {
+            cmd.args(module_args);
+        }
 
         cmd.current_dir(&self.root);
         dbg!(&self.root);
         cmd
     }
 
     // copied from above check_command
-    fn run_verus_direct(&self, file: String, verus_args: &Vec<String>) -> Command {
+    fn run_verus_direct(&self, file: String, verus_args: &Vec<String>, report_all_errors: bool) -> Command {
         let verus_binary_str = match std::env::var("VERUS_BINARY_PATH") {
             Ok(path) => path,
             Err(_) => {
@@ -696,15 +703,16 @@ impl FlycheckActor {
             }
         }
 
-        // We may need to add additional arguments
-        let mut args = verus_args.to_vec();
+        // We may need to add additional configuration arguments
+        let mut config_args = vec![];   // File name and crate type
+        let mut module_args = vec![];   // Arguments to restrict verification to the file currently being edited
         match toml_dir {
             None => {
                 // This file doesn't appear to be part of a larger project
                 // Try to invoke Verus on it directly, but try to avoid
                 // complaints about missing `fn main()`
-                args.push("--crate-type".to_string());
-                args.push("lib".to_string());
+                config_args.push("--crate-type".to_string());
+                config_args.push("lib".to_string());
             }
             Some(toml_dir) => {
                 // This file appears to be part of a Rust project.
@@ -713,8 +721,8 @@ impl FlycheckActor {
                 let root_file = if toml_dir.join("src").join("main.rs").exists() {
                     Some(toml_dir.join("src").join("main.rs"))
                 } else if toml_dir.join("src").join("lib.rs").exists() {
-                    args.push("--crate-type".to_string());
-                    args.push("lib".to_string());
+                    config_args.push("--crate-type".to_string());
+                    config_args.push("lib".to_string());
                     Some(toml_dir.join("src").join("lib.rs"))
                 } else {
                     None
@@ -735,32 +743,39 @@ impl FlycheckActor {
                             .trim_end_matches("::mod")
                             .to_string();
 
-                        args.insert(0, root_file.to_str().unwrap().to_string());
+                        config_args.insert(0, root_file.to_str().unwrap().to_string());
                         if file == root_file {
                             tracing::info!("file == root_file");
                         } else {
                             tracing::info!(?root_file, "root_file");
-                            args.insert(1, "--verify-module".to_string());
-                            args.insert(2, file_as_module);
+                            module_args.push("--verify-module".to_string());
+                            module_args.push(file_as_module);
                         }
                     }
                     None => {
                         // Puzzling -- we found a Cargo.toml but no root file.
                         // Do our best by trying to run directly on the file supplied
-                        args.insert(0, file.to_str().unwrap().to_string());
-                        args.push("--crate-type".to_string());
-                        args.push("lib".to_string());
+                        config_args.insert(0, file.to_str().unwrap().to_string());
+                        config_args.push("--crate-type".to_string());
+                        config_args.push("lib".to_string());
                     }
                 }
             }
         }
+        
+        // Apply all of the argument collections
+        cmd.args(verus_args);
+        cmd.args(config_args);
+        cmd.args(extra_args_from_toml);
+        if !report_all_errors {
+            cmd.args(module_args);
+        }
 
-        args.append(&mut extra_args_from_toml);
-        args.push("--".to_string());
-        args.push("--error-format=json".to_string());
+        // Apply arguments that go to rustc instead of Verus
+        cmd.arg("--".to_string());
+        cmd.arg("--error-format=json".to_string());
 
         cmd.current_dir(&self.root);
-        cmd.args(args);
         cmd
     }
 
@@ -772,11 +787,11 @@ impl FlycheckActor {
             FlycheckConfig::CustomCommand { .. } => {
                 panic!("verus analyzer does not yet support custom commands")
             }
-            FlycheckConfig::VerusCommand { verus_args, cargo_verus_enable, cargo_options } => {
+            FlycheckConfig::VerusCommand { verus_args, cargo_verus_enable, cargo_options, report_all_errors } => {
                 if *cargo_verus_enable {
-                    self.run_cargo_verus(file, verus_args, cargo_options)
+                    self.run_cargo_verus(file, verus_args, cargo_options, *report_all_errors)
                 } else {
-                    self.run_verus_direct(file, verus_args)
+                    self.run_verus_direct(file, verus_args, *report_all_errors)
                 }
             }
         };

crates/rust-analyzer/src/config.rs

@@ -171,6 +171,10 @@ config_data! {
         cargo_targetDir | rust_analyzerTargetDir: Option<TargetDirectory> = None,
         /// Run `cargo verus` instead of running the `verus` binary directly.
         cargo_verusEnable: bool = false,
+        /// Extra Verus arguments passed to each invocation of `verus` performed either via Cargo or directly.
+        verus_extraArgs: Vec<String> = vec![],
+        /// Setting this to true causes verus-analyzer to report errors in all files, not just the one you are editing.
+        verus_reportAllErrorsEnable: bool = false,
 
         /// Run the check command for diagnostics on save.
         checkOnSave | checkOnSave_enable: bool                         = true,
@@ -1941,7 +1945,12 @@ impl Config {
                     },
                 }
             }
-            Some(_) | None => FlycheckConfig::VerusCommand { verus_args: self.check_extra_args(), cargo_verus_enable: *self.cargo_verusEnable(), cargo_options: self.cargo_test_options() },
+            Some(_) | None => FlycheckConfig::VerusCommand {
+                verus_args: self.verus_extraArgs().clone(),
+                cargo_verus_enable: *self.cargo_verusEnable(),
+                cargo_options: self.cargo_test_options(),
+                report_all_errors: *self.verus_reportAllErrorsEnable(),
+            },
         }
     }
 

docs/user/generated_config.adoc

@@ -995,6 +995,16 @@ Show documentation.
 --
 Whether to insert closing angle brackets when typing an opening angle bracket of a generic argument list.
 --
+[[rust-analyzer.verus.extraArgs]]rust-analyzer.verus.extraArgs (default: `[]`)::
++
+--
+Extra Verus arguments passed to each invocation of `verus` performed either via Cargo or directly.
+--
+[[rust-analyzer.verus.reportAllErrorsEnable]]rust-analyzer.verus.reportAllErrorsEnable (default: `false`)::
++
+--
+Setting this to true causes verus-analyzer to report errors in all files, not just the one you are editing.
+--
 [[rust-analyzer.workspace.symbol.search.kind]]rust-analyzer.workspace.symbol.search.kind (default: `"only_types"`)::
 +
 --

editors/code/package.json

@@ -2568,6 +2568,29 @@
                     }
                 }
             },
+            {
+                "title": "verus",
+                "properties": {
+                    "verus-analyzer.verus.extraArgs": {
+                        "markdownDescription": "Extra Verus arguments passed to each invocation of `verus` performed either via Cargo or directly.",
+                        "default": [],
+                        "type": "array",
+                        "items": {
+                            "type": "string"
+                        }
+                    }
+                }
+            },
+            {
+                "title": "verus",
+                "properties": {
+                    "verus-analyzer.verus.reportAllErrorsEnable": {
+                        "markdownDescription": "Setting this to true causes verus-analyzer to report errors in all files, not just the one you are editing.",
+                        "default": false,
+                        "type": "boolean"
+                    }
+                }
+            },
             {
                 "title": "workspace",
                 "properties": {