From 398dc36f3fc262db4a90a81e7f56bdfd94b13ef9 Mon Sep 17 00:00:00 2001
From: Joshua Liebow-Feeser <joshlf@google.com>
Date: Thu, 12 Feb 2026 14:13:09 +0000
Subject: [PATCH] [hermes] Finalize removal of shadow crate code

gherrit-pr-id: Gtzihj5ol6a2xgdnfdresbbnwzaw25quk
---
 tools/hermes/src/charon.rs                 |  2 +-
 tools/hermes/src/main.rs                   |  8 ++---
 tools/hermes/src/resolve.rs                |  4 ---
 tools/hermes/src/{shadow.rs => scanner.rs} | 36 ++++------------------
 4 files changed, 11 insertions(+), 39 deletions(-)
 rename tools/hermes/src/{shadow.rs => scanner.rs} (88%)

diff --git a/tools/hermes/src/charon.rs b/tools/hermes/src/charon.rs
index 6798fb533c..e4c2b91b07 100644
--- a/tools/hermes/src/charon.rs
+++ b/tools/hermes/src/charon.rs
@@ -8,7 +8,7 @@ use cargo_metadata::{diagnostic::DiagnosticLevel, Message};
 
 use crate::{
     resolve::{Args, HermesTargetKind, Roots},
-    shadow::HermesArtifact,
+    scanner::HermesArtifact,
 };
 
 pub fn run_charon(args: &Args, roots: &Roots, packages: &[HermesArtifact]) -> Result<()> {
diff --git a/tools/hermes/src/main.rs b/tools/hermes/src/main.rs
index 30b5e03d5f..3ea66b64fa 100644
--- a/tools/hermes/src/main.rs
+++ b/tools/hermes/src/main.rs
@@ -3,7 +3,7 @@ mod diagnostics;
 mod errors;
 mod parse;
 mod resolve;
-mod shadow;
+mod scanner;
 
 mod ui_test_shim;
 
@@ -35,11 +35,11 @@ fn main() -> anyhow::Result<()> {
     match args.command {
         Commands::Verify(resolve_args) => {
             let roots = resolve::resolve_roots(&resolve_args)?;
-            let entry_points = shadow::build_shadow_crate(&roots)?;
-            if entry_points.is_empty() {
+            let packages = scanner::scan_workspace(&roots)?;
+            if packages.is_empty() {
                 anyhow::bail!("No Hermes annotations (/// ```lean ...) found in the selected targets. Nothing to verify.");
             }
-            charon::run_charon(&resolve_args, &roots, &entry_points)
+            charon::run_charon(&resolve_args, &roots, &packages)
         }
     }
 }
diff --git a/tools/hermes/src/resolve.rs b/tools/hermes/src/resolve.rs
index d202689fd4..bcff354367 100644
--- a/tools/hermes/src/resolve.rs
+++ b/tools/hermes/src/resolve.rs
@@ -122,10 +122,6 @@ pub struct Roots {
 }
 
 impl Roots {
-    pub fn shadow_root(&self) -> PathBuf {
-        self.hermes_run_root.join("shadow")
-    }
-
     pub fn charon_root(&self) -> PathBuf {
         self.hermes_run_root.join("charon")
     }
diff --git a/tools/hermes/src/shadow.rs b/tools/hermes/src/scanner.rs
similarity index 88%
rename from tools/hermes/src/shadow.rs
rename to tools/hermes/src/scanner.rs
index e7459a108f..629dce0900 100644
--- a/tools/hermes/src/shadow.rs
+++ b/tools/hermes/src/scanner.rs
@@ -1,6 +1,5 @@
 use std::{
-    collections::{HashMap, HashSet},
-    fs,
+    collections::HashMap,
     hash::{Hash, Hasher as _},
     path::{Path, PathBuf},
     sync::mpsc::{self, Sender},
@@ -8,7 +7,6 @@ use std::{
 
 use anyhow::{Context, Result};
 use dashmap::DashSet;
-use walkdir::WalkDir;
 
 use crate::{
     parse,
@@ -45,13 +43,10 @@ impl HermesArtifact {
     }
 }
 
-/// The main entry point for creating the shadow crate.
-///
-/// 1. Scans and transforms all reachable source files, printing any errors
+/// 1. Scans and rules all reachable source files, printing any errors
 ///    encountered. Collects all items with Hermes annotations.
-/// 2. Creates symlinks for the remaining skeleton.
-pub fn build_shadow_crate(roots: &Roots) -> Result<Vec<HermesArtifact>> {
-    log::trace!("build_shadow_crate({:?})", roots);
+pub fn scan_workspace(roots: &Roots) -> Result<Vec<HermesArtifact>> {
+    log::trace!("scan_workspace({:?})", roots);
 
     let visited_paths = DashSet::new();
     let (err_tx, err_rx) = mpsc::channel();
@@ -164,25 +159,10 @@ fn process_file_recursive<'a>(
         return;
     }
 
-    // shadow_root + (src_path - workspace_root)
-    let relative_path = match src_path.strip_prefix(&config.workspace) {
-        Ok(p) => p,
-        Err(e) => {
-            let _ = err_tx.send(anyhow::anyhow!("Source file outside workspace: {:?}", e));
-            return;
-        }
-    };
-    let dest_path = config.shadow_root().join(relative_path);
-
+    // Walking the AST is enough to collect new modules.
     let result = (|| -> Result<Vec<(PathBuf, String)>> {
-        if let Some(parent) = dest_path.parent() {
-            // NOTE: `create_dir_all` is robust against TOCTOU, so it's fine
-            // that we're racing with other threads.
-            fs::create_dir_all(parent)?;
-        }
-
         // Walk the AST, collecting new modules to process.
-        let (source_code, unloaded_modules) =
+        let (_source_code, unloaded_modules) =
             parse::read_file_and_scan_compilation_unit(src_path, |_src, item_result| {
                 match item_result {
                     Ok(parsed_item) => {
@@ -206,10 +186,6 @@ fn process_file_recursive<'a>(
             })
             .context(format!("Failed to parse {:?}", src_path))?;
 
-        let buffer = source_code.into_bytes();
-        fs::write(&dest_path, &buffer)
-            .context(format!("Failed to write shadow file {:?}", dest_path))?;
-
         // Resolve and queue child modules for processing.
         let base_dir = src_path.parent().unwrap();
         let mut next_paths = Vec::new();