[hermes] Parse Hermes attributes

tools/hermes/src/scanner.rs

@@ -188,15 +188,28 @@ fn process_file_recursive<'a>(
                 let mut full_path = current_prefix.clone();
                 full_path.extend(item.module_path);
 
-                use parse::ParsedItem::*;
                 match &item.item {
                     // Unreliable syntaxes: we have no way of reliably naming
                     // these in Charon's `--start-from` argument, so we fall
                     // back to naming the parent module.
-                    Impl(_) | ImplItemFn(_) | TraitItemFn(_) => {
+                    parse::ParsedItem::Impl(_) => {
                         let start_from = full_path.join("::");
                         path_tx.send((name.clone(), start_from)).unwrap();
                     }
+                    parse::ParsedItem::Function(f) => match &f.item {
+                        parse::FunctionItem::Impl(_) | parse::FunctionItem::Trait(_) => {
+                            let start_from = full_path.join("::");
+                            path_tx.send((name.clone(), start_from)).unwrap();
+                        }
+                        parse::FunctionItem::Free(_) => {
+                            if let Some(item_name) = item.item.name() {
+                                full_path.push(item_name);
+                                let start_from = full_path.join("::");
+                                log::debug!("Found entry point: {}", start_from);
+                                path_tx.send((name.clone(), start_from)).unwrap();
+                            }
+                        }
+                    },
                     // Reliable syntaxes: target the specific item.
                     _ => {
                         if let Some(item_name) = item.item.name() {

tools/hermes/tests/fixtures/broken_doc_block/expected_stderr.txt

@@ -1 +1 @@
-Unclosed ```lean block
+Unclosed Hermes block in documentation.

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

@@ -1,3 +1,3 @@
-/// ```lean
+/// ```lean, hermes
 /// unclosed block
 fn foo() {}

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

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

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

@@ -1,6 +1,6 @@
 #[cfg(target_os = "haiku")]
 mod ghost {
-    /// ```lean
+    /// ```lean, hermes
     /// ```
     pub fn hidden() {}
 }

tools/hermes/tests/fixtures/collision/expected/crates/a/src/lib.rs

@@ -1,3 +1,3 @@
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn utils_a() {}

tools/hermes/tests/fixtures/collision/expected/crates/b/src/lib.rs

@@ -1,3 +1,3 @@
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn utils_b() {}

tools/hermes/tests/fixtures/collision/source/crates/a/src/lib.rs

@@ -1,3 +1,3 @@
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn utils_a() {}

tools/hermes/tests/fixtures/collision/source/crates/b/src/lib.rs

@@ -1,3 +1,3 @@
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn utils_b() {}

tools/hermes/tests/fixtures/complex_impl/expected/src/lib.rs

@@ -5,21 +5,21 @@ pub trait T3 { fn m3(); }
 
 // Case 1: Raw Pointer (*const Foo)
 impl T1 for *const Foo {
-    /// ```lean
+    /// ```lean, hermes
     /// ```
     fn m1() {}
 }
 
 // Case 2: Slice ([Foo])
 impl T2 for [Foo] {
-    /// ```lean
+    /// ```lean, hermes
     /// ```
     fn m2() {}
 }
 
 // Case 3: Array ([Foo; 5])
 impl T3 for [Foo; 5] {
-    /// ```lean
+    /// ```lean, hermes
     /// ```
     fn m3() {}
 }

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

@@ -5,21 +5,21 @@ pub trait T3 { fn m3(); }
 
 // Case 1: Raw Pointer (*const Foo)
 impl T1 for *const Foo {
-    /// ```lean
+    /// ```lean, hermes
     /// ```
     fn m1() {}
 }
 
 // Case 2: Slice ([Foo])
 impl T2 for [Foo] {
-    /// ```lean
+    /// ```lean, hermes
     /// ```
     fn m2() {}
 }
 
 // Case 3: Array ([Foo; 5])
 impl T3 for [Foo; 5] {
-    /// ```lean
+    /// ```lean, hermes
     /// ```
     fn m3() {}
 }

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

@@ -1,5 +1,5 @@
 const _: () = {
-    /// ```lean
+    /// ```lean, hermes
     /// theorem hidden_impl : True := trivial
     /// ```
     pub fn hidden_impl() {}

tools/hermes/tests/fixtures/crlf_endings/expected/src/lib.rs

@@ -1,5 +1,5 @@
 fn windows() {}
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn _hermes_dummy() {}

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

@@ -1,5 +1,5 @@
 fn windows() {}
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn _hermes_dummy() {}

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

@@ -2,6 +2,6 @@
 mod sys;
 
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn _hermes_dummy() {}

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

@@ -1,7 +1,7 @@
 #[path = "lib.rs"]
 mod self_loop;
 
-/// ```lean
+/// ```lean, hermes
 /// theorem valid : True := trivial
 /// ```
 pub fn valid() {}

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

@@ -1,6 +1,6 @@
 pub mod nested;
 
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn _hermes_dummy() {}

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

@@ -1,6 +1,6 @@
 mod bar;
 
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn _hermes_dummy() {}

tools/hermes/tests/fixtures/dirty_target_dir/expected/src/lib.rs

@@ -1,6 +1,6 @@
 fn clean() {}
 
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn _hermes_dummy() {}

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

@@ -1,6 +1,6 @@
 fn clean() {}
 
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn _hermes_dummy() {}

tools/hermes/tests/fixtures/double_mounted_mod/source/src/shared.rs

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

tools/hermes/tests/fixtures/duplicate_blocks/expected_stderr.txt

@@ -1 +1 @@
-Multiple lean blocks found
+Multiple Hermes blocks found on a single item.

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

@@ -1,7 +1,7 @@
-/// ```lean
+/// ```lean, hermes
 /// block 1
 /// ```
-/// ```lean
+/// ```lean, hermes
 /// block 2
 /// ```
 fn double_doc() {}

tools/hermes/tests/fixtures/empty_file/expected/src/lib.rs

@@ -1,4 +1,4 @@
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn _hermes_dummy() {}

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

@@ -1,4 +1,4 @@
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn _hermes_dummy() {}

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

@@ -1,5 +1,5 @@
 pub fn foo() {}
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 pub fn dummy() {}

tools/hermes/tests/fixtures/external_path_dep/extra.rs

@@ -1,3 +1,3 @@
-/// ```lean
+/// ```lean, hermes
 /// ```
 pub fn foo() {}

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

@@ -1,3 +1,3 @@
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn my_func() {}

tools/hermes/tests/fixtures/file_mod/expected/src/lib.rs

@@ -1,6 +1,6 @@
 mod foo;
 
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn _hermes_dummy() {}

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

@@ -1,6 +1,6 @@
 mod foo;
 
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn _hermes_dummy() {}

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

@@ -1,5 +1,5 @@
 pub fn foo() {}
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 pub fn dummy() {}

tools/hermes/tests/fixtures/hermes_multiple_targets/source/src/bin/my_bin.rs

@@ -1,5 +1,5 @@
 fn main() {}
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 pub fn dummy() {}

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

@@ -1,5 +1,5 @@
 pub fn lib_fn() {}
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 pub fn dummy() {}

tools/hermes/tests/fixtures/ignored_files/expected/src/lib.rs

@@ -1,6 +1,6 @@
 fn keep() {}
 
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn _hermes_dummy() {}

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

@@ -1,6 +1,6 @@
 fn keep() {}
 
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn _hermes_dummy() {}

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

@@ -2,19 +2,19 @@ pub mod my_module {
     pub struct Foo;
 
     impl Foo {
-        /// ```lean
+        /// ```lean, hermes
         /// theorem meth_one : True := trivial
         /// ```
         pub fn method_one() {}
 
-        /// ```lean
+        /// ```lean, hermes
         /// theorem meth_two : True := trivial
         /// ```
         pub fn method_two() {}
     }
 
     pub trait Bar {
-        /// ```lean
+        /// ```lean, hermes
         /// theorem trait_meth : True := trivial
         /// ```
         fn trait_method();

tools/hermes/tests/fixtures/impl_path/expected/src/lib.rs

@@ -1,7 +1,7 @@
 pub struct Foo;
 
 impl Foo {
-    /// ```lean
+    /// ```lean, hermes
     /// ```
     pub fn bar() {}
 }

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

@@ -1,7 +1,7 @@
 pub struct Foo;
 
 impl Foo {
-    /// ```lean
+    /// ```lean, hermes
     /// ```
     pub fn bar() {}
 }

tools/hermes/tests/fixtures/inline_mod/expected/src/lib.rs

@@ -3,6 +3,6 @@ mod foo {
 }
 
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn _hermes_dummy() {}

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

@@ -3,6 +3,6 @@ mod foo {
 }
 
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn _hermes_dummy() {}

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

@@ -1,5 +1,5 @@
 pub fn foo() {}
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 pub fn dummy() {}

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

@@ -1,5 +1,5 @@
 pub fn foo() {}
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 pub fn dummy() {}

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

@@ -1,5 +1,5 @@
 pub fn foo() {}
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 pub fn dummy() {}

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

@@ -1,6 +1,6 @@
 fn code() {}
 
 
-/// ```lean
+/// ```lean, hermes
 /// ```
 fn _hermes_dummy() {}

tools/hermes/tests/fixtures/macro_blind_spot/source/src/hidden.rs

@@ -1,3 +1,3 @@
-/// ```lean
+/// ```lean, hermes
 /// ```
 pub fn foo() {}

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

@@ -1,4 +1,4 @@
-/// ```lean
+/// ```lean, hermes
 /// model demo 
 /// ```
 pub fn demo() {}