[hermes] Harden against weird symlink layout

tools/hermes/src/parse.rs

@@ -118,7 +118,7 @@ where
     F: FnMut(&str, Result<ParsedLeanItem, HermesError>),
 {
     log::trace!("read_file_and_scan_compilation_unit({:?})", path);
-    let source = fs::read_to_string(path).expect("Failed to read file");
+    let source = fs::read_to_string(path)?;
     let unloaded_modules = scan_compilation_unit(&source, f);
     Ok((source, unloaded_modules))
 }

tools/hermes/src/resolve.rs

@@ -1,5 +1,5 @@
 use std::{
-    env,
+    env, fs,
     hash::{Hash as _, Hasher as _},
     path::PathBuf,
 };
@@ -341,7 +341,9 @@ fn resolve_targets<'a>(
 /// is found.
 pub fn check_for_external_deps(metadata: &Metadata) -> Result<()> {
     log::trace!("check_for_external_deps");
-    let workspace_root = metadata.workspace_root.as_std_path();
+    // Canonicalize workspace root to handle symlinks correctly
+    let workspace_root = fs::canonicalize(&metadata.workspace_root)
+        .context("Failed to canonicalize workspace root")?;
 
     for pkg in &metadata.packages {
         // We only care about packages that are "local" (source is None).
@@ -350,8 +352,12 @@ pub fn check_for_external_deps(metadata: &Metadata) -> Result<()> {
         if pkg.source.is_none() {
             let pkg_path = pkg.manifest_path.as_std_path();
 
+            // Canonicalize the package path for comparison
+            let canonical_pkg_path = fs::canonicalize(pkg_path)
+                .with_context(|| format!("Failed to canonicalize path for package {}", pkg.name))?;
+
             // Check if the package lives outside the workspace tree
-            if !pkg_path.starts_with(workspace_root) {
+            if !canonical_pkg_path.starts_with(&workspace_root) {
                 anyhow::bail!(
                     "Unsupported external dependency: '{}' at {:?}.\n\
                      Hermes currently only supports verifying workspaces where all local \

tools/hermes/src/scanner.rs

@@ -1,5 +1,6 @@
 use std::{
     collections::HashMap,
+    ffi::OsStr,
     hash::{Hash, Hasher as _},
     path::{Path, PathBuf},
     sync::mpsc::{self, Sender},
@@ -141,14 +142,28 @@ fn process_file_recursive<'a>(
     name: HermesTargetName,
 ) {
     log::trace!("process_file_recursive(src_path: {:?})", src_path);
-    if !visited.insert(src_path.to_path_buf()) {
+
+    // Canonicalize the path to ensure we don't process the same file multiple
+    // times (e.g. via symlinks or different relative paths).
+    let src_path = match std::fs::canonicalize(src_path) {
+        Ok(p) => p,
+        Err(e) => {
+            // It is valid for a module to be declared but not exist (e.g., if
+            // it is cfg-gated for another platform). In strict Rust, we would
+            // check the cfg attributes, but since we are just scanning, it is
+            // safe to warn and return.
+            log::debug!("Skipping unreachable or missing file {:?}: {}", src_path, e);
+            return;
+        }
+    };
+
+    if !visited.insert(src_path.clone()) {
         return;
     }
 
-    // Walking the AST is enough to collect new modules.
     // Walk the AST, collecting new modules to process.
     let (_source_code, unloaded_modules) =
-        match parse::read_file_and_scan_compilation_unit(src_path, |_src, item_result| {
+        match parse::read_file_and_scan_compilation_unit(&src_path, |_src, item_result| {
             match item_result {
                 Ok(parsed_item) => {
                     if let Some(item_name) = parsed_item.item.name() {
@@ -177,11 +192,23 @@ fn process_file_recursive<'a>(
             }
         };
 
+    // Determine the directory to search for child modules in.
+    // - For `mod.rs`, `lib.rs`, `main.rs`, children are in the parent directory.
+    //   e.g. `src/lib.rs` -> `mod foo` -> `src/foo.rs`
+    // - For `my_mod.rs`, children are in a sibling directory of the same name.
+    //   e.g. `src/my_mod.rs` -> `mod sub` -> `src/my_mod/sub.rs`
+    let file_stem = src_path.file_stem().and_then(OsStr::to_str).unwrap_or("");
+    let base_dir = if matches!(file_stem, "mod" | "lib" | "main") {
+        src_path.parent().unwrap_or(&src_path).to_path_buf()
+    } else {
+        // e.g. src/foo.rs -> src/foo/
+        src_path.with_extension("")
+    };
+
     // Resolve and queue child modules for processing.
-    let base_dir = src_path.parent().unwrap();
     for module in unloaded_modules {
         if let Some(mod_path) =
-            resolve_module_path(base_dir, &module.name, module.path_attr.as_deref())
+            resolve_module_path(&base_dir, &module.name, module.path_attr.as_deref())
         {
             // Spawn new tasks for discovered modules.
             let (err_tx, path_tx) = (err_tx.clone(), path_tx.clone());

tools/hermes/tests/fixtures/canonicalized_workspace/expected_status.txt

@@ -0,0 +1 @@
+success

tools/hermes/tests/fixtures/canonicalized_workspace/source/Cargo.toml

@@ -0,0 +1,3 @@
+[workspace]
+members = ["crates/app", "crates/lib"]
+resolver = "2"

tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/app/Cargo.toml

@@ -0,0 +1,10 @@
+[package]
+name = "app"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+# Intentionally messy relative path that traverses up and down
+# ../../crates/lib is inside the workspace, but we structure it to ensure
+# canonicalization is required to match it correctly.
+my_lib = { path = "../../crates/lib" }

tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/app/src/lib.rs

@@ -0,0 +1,4 @@
+/// ```lean
+/// theorem main_proof : True := trivial
+/// ```
+pub fn main_proof() {}

tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/lib/Cargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "my_lib"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]

tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/lib/src/lib.rs

@@ -0,0 +1 @@
+pub fn shared() {}

tools/hermes/tests/fixtures/cyclic_paths/expected_status.txt

@@ -0,0 +1 @@
+failure

tools/hermes/tests/fixtures/cyclic_paths/source/Cargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "cyclic_paths"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]

tools/hermes/tests/fixtures/cyclic_paths/source/src/lib.rs

@@ -0,0 +1,9 @@
+// This simulates a symlink loop by pointing a module declaration back at itself.
+// Without canonicalization, this causes a stack overflow.
+#[path = "lib.rs"]
+mod self_loop;
+
+/// ```lean
+/// theorem valid : True := trivial
+/// ```
+pub fn valid() {}

tools/hermes/tests/fixtures/missing_cfg_file/expected_status.txt

@@ -0,0 +1 @@
+success

tools/hermes/tests/fixtures/missing_cfg_file/source/Cargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "missing_cfg_file"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]

tools/hermes/tests/fixtures/missing_cfg_file/source/src/lib.rs

@@ -0,0 +1,7 @@
+#[cfg(target_os = "windows")]
+mod windows_sys; // This file will intentionally not exist
+
+/// ```lean
+/// theorem demo : True := trivial
+/// ```
+pub fn demo() {}

tools/hermes/tests/fixtures/nested_file_mod/expected_config.toml

@@ -0,0 +1,3 @@
+[[command]]
+args = ["--start-from", "crate::foo::bar::deep_proof"]
+should_not_exist = false

tools/hermes/tests/fixtures/nested_file_mod/expected_status.txt

@@ -0,0 +1 @@
+success

tools/hermes/tests/fixtures/nested_file_mod/source/Cargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "nested_file_mod"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]

tools/hermes/tests/fixtures/nested_file_mod/source/src/foo.rs

@@ -0,0 +1 @@
+mod bar;

tools/hermes/tests/fixtures/nested_file_mod/source/src/foo/bar.rs

@@ -0,0 +1,4 @@
+/// ```lean
+/// theorem deep_proof : True := trivial
+/// ```
+pub fn deep_proof() {}

tools/hermes/tests/fixtures/nested_file_mod/source/src/lib.rs

@@ -0,0 +1 @@
+mod foo;