From 843957a534afab26dac8f60bdccd6554ab0a7dd8 Mon Sep 17 00:00:00 2001
From: rikosellic <64517311+rikosellic@users.noreply.github.com>
Date: Mon, 19 Jan 2026 17:34:55 +0800
Subject: [PATCH 1/2] Add dependencies in `dv doc`

---
 src/doc.rs | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/doc.rs b/src/doc.rs
index 173bd7c..30dade6 100644
--- a/src/doc.rs
+++ b/src/doc.rs
@@ -62,6 +62,19 @@ fn generate_single_target_doc(
     cmd.env("VERUSDOC", verus_doc_value);
     cmd.env("RUSTC_BOOTSTRAP", "1");
 
+    // Add extern dependencies for verus_builtin
+    let builtin_path = verus_target_dir.join("libverus_builtin.rlib");
+    cmd.arg("--extern")
+        .arg(format!("verus_builtin={}", builtin_path.display()));
+
+    // Add extern dependencies for verus_builtin_macros
+    let builtin_macros_path =
+        verus_target_dir.join(format!("verus_builtin_macros{}", verus::DYN_LIB));
+    cmd.arg("--extern").arg(format!(
+        "verus_builtin_macros={}",
+        builtin_macros_path.display()
+    ));
+
     // Add extern dependencies for vstd
     let vstd_path = verus_target_dir.join("libvstd.rlib");
     cmd.arg("--extern")

From eed556a29239d08bccfffccde84887b95bfaf0a8 Mon Sep 17 00:00:00 2001
From: rikosellic <64517311+rikosellic@users.noreply.github.com>
Date: Mon, 19 Jan 2026 17:49:43 +0800
Subject: [PATCH 2/2] Adjust dependency

---
 src/doc.rs | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

diff --git a/src/doc.rs b/src/doc.rs
index 30dade6..09ce839 100644
--- a/src/doc.rs
+++ b/src/doc.rs
@@ -75,21 +75,19 @@ fn generate_single_target_doc(
         builtin_macros_path.display()
     ));
 
+    // Add extern dependencies for verus_state_machine_macros
+    let state_machine_macros_path =
+        verus_target_dir.join(format!("verus_state_machine_macros{}", verus::DYN_LIB));
+    cmd.arg("--extern").arg(format!(
+        "verus_state_machine_macros={}",
+        state_machine_macros_path.display()
+    ));
+
     // Add extern dependencies for vstd
     let vstd_path = verus_target_dir.join("libvstd.rlib");
     cmd.arg("--extern")
         .arg(format!("vstd={}", vstd_path.display()));
 
-    // Add state_machines_macros dependency (proc-macro)
-    let state_machines_macros_path =
-        verus_target_dir.join(format!("verus_state_machines_macros{}", verus::DYN_LIB));
-    if state_machines_macros_path.exists() {
-        cmd.arg("--extern").arg(format!(
-            "verus_state_machines_macros={}",
-            state_machines_macros_path.display()
-        ));
-    }
-
     // Add dependencies that this target actually needs
     let deps = verus::get_local_dependency(target);
     for (_name, dep_target) in deps.iter() {