Add cargo-verus tool and split out verus-driver

source/Cargo.toml

@@ -4,22 +4,23 @@ members = [
   "air",
   "builtin",
   "builtin_macros",
+  "cargo-verus",
   "vir",
   "vir_macros",
   "rust_verify",
   "verus",
+  "verus-driver",
+  "verus-sysroot-dummy",
   "rust_verify_test",
   "rust_verify_test_macros",
   "state_machines_macros",
   "verusdoc",
+  "vstd",
   "vstd_build",
   "tools/internals_interface",
   "tools/line_count",
   "tools/qi-graph",
 ]
-exclude = [
-  "vstd",
-]
 
 # do not modify the following two lines
 [workspace.metadata.vargo]

source/builtin/Cargo.toml

@@ -3,3 +3,6 @@ name = "builtin"
 version = "0.1.0"
 edition = "2018"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[package.metadata.verus]
+is-builtin = true

source/builtin_macros/Cargo.toml

@@ -13,3 +13,6 @@ synstructure = "0.12"
 syn = "1.0"
 syn_verus = { path="../../dependencies/syn", features = ["full", "visit", "visit-mut", "extra-traits"] }
 prettyplease_verus = { path="../../dependencies/prettyplease" }
+
+[package.metadata.verus]
+is-builtin-macros = true

source/cargo-verus/Cargo.toml

@@ -0,0 +1,15 @@
+[package]
+name = "cargo-verus"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+cargo_metadata = "0.18.1"
+rustc_tools_util = "0.3.0"
+serde = { version = "1.0", features = ["derive"] }
+serde_json = "1.0"
+sha2 = "0.10.8"
+hex = "0.4.3"
+
+[build-dependencies]
+rustc_tools_util = "0.3.0"

source/cargo-verus/build.rs

@@ -0,0 +1,12 @@
+//
+// Copyright (c) 2024 The Verus Contributors
+//
+// SPDX-License-Identifier: MIT
+//
+
+fn main() {
+    rustc_tools_util::setup_version_info!();
+
+    // See https://doc.rust-lang.org/cargo/reference/build-scripts.html#rerun-if-changed
+    println!("cargo:rerun-if-changed=build.rs");
+}