diff --git a/src/dep_tree.rs b/src/dep_tree.rs index 1a4b742..e1d4994 100644 --- a/src/dep_tree.rs +++ b/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, diff --git a/src/doc.rs b/src/doc.rs new file mode 100644 index 0000000..173bd7c --- /dev/null +++ b/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(()) +} diff --git a/src/generator.rs b/src/generator.rs index ef9c753..de31780 100644 --- a/src/generator.rs +++ b/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; diff --git a/src/lib.rs b/src/lib.rs index 269c68b..5d5b739 100644 --- a/src/lib.rs +++ b/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; diff --git a/src/main.rs b/src/main.rs index 6257ba4..3c407aa 100644 --- a/src/main.rs +++ b/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, + 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> { diff --git a/src/verus.rs b/src/verus.rs index 318dc52..8a43e8b 100644 --- a/src/verus.rs +++ b/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(()) }