Add doc command

src/dep_tree.rs

@@ -1,7 +1,6 @@
 use indexmap::IndexMap;
 
 use crate::commands;
-use crate::helper::warn;
 use std::{
     collections::{HashMap, HashSet},
     process::Command,

src/doc.rs

@@ -0,0 +1,167 @@
+use crate::verus::{self, DynError, VerusTarget};
+use colored::Colorize;
+use std::path::Path;
+use std::process::Command;
+
+/// Generate documentation for verification targets
+pub fn exec_doc(target: &str, verus_conds: bool) -> Result<(), DynError> {
+    let target_to_use = verus::find_target(target)?;
+    generate_docs(&target_to_use, verus_conds)?;
+    Ok(())
+}
+
+/// Generate documentation for the target including all its dependencies
+fn generate_docs(target: &VerusTarget, verus_conds: bool) -> Result<(), DynError> {
+    info!(
+        "Generating documentation for {} with all dependencies...",
+        target.name
+    );
+
+    let root_dir = verus::get_workspace_root();
+    let doc_output_dir = root_dir.join("doc");
+
+    std::fs::create_dir_all(&doc_output_dir)?;
+
+    let deps = verus::get_local_dependency(target);
+
+    for (_name, dep_target) in deps.iter() {
+        if dep_target.name != target.name {
+            generate_single_target_doc(dep_target, verus_conds, &doc_output_dir)?;
+        }
+    }
+
+    generate_single_target_doc(target, verus_conds, &doc_output_dir)?;
+
+    if verus_conds {
+        run_verusdoc_postprocessor()?;
+    }
+
+    info!("{}", "Generation Complete!".bold().green(),);
+
+    Ok(())
+}
+
+/// Generate documentation for a single target using rustdoc
+fn generate_single_target_doc(
+    target: &VerusTarget,
+    verus_conds: bool,
+    doc_output_dir: &Path,
+) -> Result<(), DynError> {
+    info!(
+        "{} {}",
+        "Generating docs".bold().blue(),
+        target.name.white()
+    );
+
+    let verus_target_dir = verus::get_verus_target_dir();
+    let target_dir = verus::get_target_dir();
+    let mut cmd = Command::new("rustdoc");
+
+    // Set VERUSDOC environment variable based on verus_conds flag
+    let verus_doc_value = if verus_conds { "1" } else { "0" };
+    cmd.env("VERUSDOC", verus_doc_value);
+    cmd.env("RUSTC_BOOTSTRAP", "1");
+
+    // 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() {
+        if dep_target.name != target.name {
+            // Check if .rlib file exists for this dependency
+            let rlib_path =
+                target_dir.join(format!("lib{}.rlib", dep_target.name.replace('-', "_")));
+            if rlib_path.exists() {
+                let extern_name = dep_target.name.replace('-', "_");
+                cmd.arg("--extern")
+                    .arg(format!("{}={}", extern_name, rlib_path.display()));
+            } else {
+                return Err(format!(
+                    "Missing compiled dependency '{}' for target '{}'.\n\nPlease run:\n  cargo dv verify --targets {}",
+                    dep_target.name, target.name, target.name
+                ).into());
+            }
+        }
+    }
+
+    cmd.arg("-L").arg(format!("{}", verus_target_dir.display()));
+    cmd.arg("-L").arg(format!("{}", target_dir.display()));
+    cmd.arg("--edition=2021")
+        .arg("--cfg")
+        .arg("verus_keep_ghost")
+        .arg("--cfg")
+        .arg("verus_keep_ghost_body")
+        .arg("--cfg")
+        .arg("feature=\"std\"")
+        .arg("--cfg")
+        .arg("feature=\"alloc\"")
+        .arg("-Zcrate-attr=feature(stmt_expr_attributes)")
+        .arg("-Zcrate-attr=feature(register_tool)")
+        .arg("-Zcrate-attr=register_tool(verus)")
+        .arg("-Zcrate-attr=register_tool(verifier)")
+        .arg("-Zcrate-attr=register_tool(verusfmt)")
+        .arg("-Zcrate-attr=feature(rustc_attrs)")
+        .arg("-Zcrate-attr=feature(portable_simd)")
+        .arg("-Zcrate-attr=feature(negative_impls)")
+        .arg("--enable-index-page")
+        .arg("-Zunstable-options");
+
+    // Set crate type and name
+    cmd.arg("--crate-type=lib")
+        .arg(format!("--crate-name={}", target.name.replace('-', "_")));
+
+    // Set output directory
+    cmd.arg("-o").arg(&doc_output_dir);
+
+    // Add the source file
+    let source_file = target.root_file();
+    cmd.arg(&source_file);
+
+    debug!("Running rustdoc for {}: {:?}", target.name, cmd);
+
+    let status = cmd.status()?;
+    if !status.success() {
+        warn!(
+            "rustdoc failed for target: {}, but continuing...",
+            target.name
+        );
+        return Ok(()); // Continue with other targets instead of failing
+    }
+
+    info!(
+        "{} {} {}",
+        "Generated docs for".bold().green(),
+        target.name.white(),
+        "successfully".green()
+    );
+
+    Ok(())
+}
+
+fn run_verusdoc_postprocessor() -> Result<(), DynError> {
+    let verusdoc = verus::get_verusdoc();
+
+    info!("Running verusdoc post-processor...");
+    let status = Command::new(&verusdoc).status()?;
+
+    if !status.success() {
+        warn!("verusdoc post-processor failed");
+    } else {
+        info!("verusdoc post-processor completed successfully");
+    }
+
+    Ok(())
+}

src/generator.rs

@@ -1,5 +1,4 @@
 use crate::files;
-use crate::helper::{error, info};
 use askama::Template;
 use std::io::Write;
 use std::path::Path;

src/lib.rs

@@ -7,6 +7,7 @@ pub mod console;
 pub mod commands;
 pub mod config;
 pub mod dep_tree;
+pub mod doc;
 pub mod fingerprint;
 pub mod format;
 pub mod generator;

src/main.rs

@@ -191,12 +191,17 @@ struct VerifyArgs {
 struct DocArgs {
     #[arg(
         short = 't',
-        long = "targets", 
-        value_parser = verus::find_target,
-        help = "The targets to generate document", 
-        num_args = 0..,
-        action = ArgAction::Append)]
-    targets: Vec<VerusTarget>,
+        long = "target",
+        help = "The target to generate documentation for (along with its dependencies)"
+    )]
+    target: String,
+
+    #[arg(
+        long = "verus-conds",
+        help = "Include Verus pre/post conditions in generated docs",
+        default_value = "false",
+        action = ArgAction::SetTrue)]
+    verus_conds: bool,
 }
 
 #[derive(Parser, Debug)]
@@ -417,8 +422,8 @@ fn verify(args: &VerifyArgs) -> Result<(), DynError> {
     verus::exec_verify(&targets, &imports, &options)
 }
 
-fn doc(_args: &DocArgs) -> Result<(), DynError> {
-    error!("The doc command is not implemented yet");
+fn doc(args: &DocArgs) -> Result<(), DynError> {
+    doc::exec_doc(&args.target, args.verus_conds)
 }
 
 fn bootstrap(args: &BootstrapArgs) -> Result<(), DynError> {

src/verus.rs

@@ -63,6 +63,10 @@ pub const Z3_HINT: &str = "tools/verus/source";
 pub const Z3_EVN: &str = "VERUS_Z3_PATH";
 
 pub const RUSTDOC_BIN: &str = "rustdoc";
+
+#[cfg(target_os = "windows")]
+pub const VERUSDOC_BIN: &str = "verusdoc.exe";
+#[cfg(not(target_os = "windows"))]
 pub const VERUSDOC_BIN: &str = "verusdoc";
 pub const VERUSDOC_HINT_RELEASE: &str = "tools/verus/source/target/release";
 pub const VERUSDOC_HINT: &str = "tools/verus/source/target/debug";
@@ -117,14 +121,12 @@ pub fn get_rustdoc() -> PathBuf {
 }
 
 #[memoize]
-pub fn get_verusdoc(release: bool) -> PathBuf {
-    executable::locate(
-            VERUSDOC_BIN,
-            None,
-            if release { &[VERUSDOC_HINT_RELEASE] } else { &[VERUSDOC_HINT] },
-        ).unwrap_or_else(|| {
-            error!("Cannot find the verusdoc binary, please install it using `cargo xtask bootstrap verusdoc`");
-        })
+pub fn get_verusdoc() -> PathBuf {
+    executable::locate(VERUSDOC_BIN, None, &[VERUSDOC_HINT_RELEASE, VERUSDOC_HINT]).unwrap_or_else(
+        || {
+            error!("Cannot find the verusdoc binary, please try `cargo dv bootstrap --upgrade`");
+        },
+    )
 }
 
 #[memoize]
@@ -136,6 +138,15 @@ pub fn get_target_dir() -> PathBuf {
     metadata.target_directory.into_std_path_buf()
 }
 
+#[memoize]
+pub fn get_workspace_root() -> PathBuf {
+    let metadata = cargo_metadata::MetadataCommand::new()
+        .no_deps()
+        .exec()
+        .expect("Failed to get metadata");
+    metadata.workspace_root.into_std_path_buf()
+}
+
 #[memoize]
 pub fn get_verus_target_dir() -> PathBuf {
     let verus_dir = install::verus_dir();
@@ -1458,6 +1469,17 @@ pub mod install {
         cmd.status().unwrap_or_else(|e| {
             error!("Failed to build verus: {}", e);
         });
+
+        let mut verusdoc_cmd = executable::get_powershell_command()?;
+        verusdoc_cmd
+            .current_dir(verus_source_dir())
+            .arg("/c")
+            .arg("& '..\\tools\\activate.ps1'; vargo build -p verusdoc");
+        debug!("{:?}", verusdoc_cmd);
+        verusdoc_cmd.status().unwrap_or_else(|e| {
+            error!("Failed to build verusdoc: {}", e);
+        });
+
         status!("Verus build complete");
         Ok(())
     }
@@ -1480,6 +1502,19 @@ pub mod install {
         cmd.status().unwrap_or_else(|e| {
             error!("Failed to build verus: {}", e);
         });
+
+        let verusdoc_cmd = &mut Command::new("bash");
+        verusdoc_cmd
+            .current_dir(verus_source_dir())
+            .env_remove("RUSTUP_TOOLCHAIN")
+            .env("RUSTUP_TOOLCHAIN", toolchain_name)
+            .arg("-c")
+            .arg("source ../tools/activate; vargo build -p verusdoc");
+        debug!("{:?}", verusdoc_cmd);
+        verusdoc_cmd.status().unwrap_or_else(|e| {
+            error!("Failed to build verusdoc: {}", e);
+        });
+
         status!("Verus build complete");
         Ok(())
     }