[WIP] Agent

[joshlf]

---

This PR is on branch hermes.

• 　  [hermes] Parse Hermes attributes #3051
• 👉 [WIP] Agent #3050
• 　  [WIP] #3049
• 　  [hermes] Invoke Aeneas #3048
• 　  [hermes] More aggressively test hidden item rejection #3047
• 　  [hermes] Reject annotated items in blocks #3046
• 　  [hermes] Warn on #[cfg_attr(..., path = "...")] #3045
• 　  [hermes] Don't pass overly-long arguments to Charon #3044
• 　  [hermes] Harden against weird symlink layout #3043
• 　  [hermes] Clean up after removing shadow crate support #3038
• 　  [hermes] Finalize removal of shadow crate code #3037
• 　  [hermes] Remove diagnostic path mapping from shadow copy #3036
• 　  [hermes] Stop copying shadow crate; run in-place #3035
• 　  [hermes] Disable unsafe redaction #3034
• 　  [hermes] Take responsibility for all terminal UI #3019
• 　  [hermes] Get tests passing again #3018
• 　  [hermes] Add some tests for Charon invocation #3015
• 　  [hermes] Add Charon step #3014
• 　  [hermes] Isolate shadow crate from other artifacts #3013
• 　  [hermes] Add some trace/debug logging #3012
• 　  [hermes] Add one more UI test #3011
• 　  [hermes] Add fixture testing #3010
• 　  [hermes] Finish shadow crate creation #3009
• 　  [hermes] Discover mod foo; declarations #3008
• 　  [hermes] Resolve Cargo and Hermes target dirs #3007
• 　  [hermes] Add shadow copy creation #3006
• 　  [hermes] Add package/target/root resolution #3005
• 　  [hermes] Add source code transformation #3004
• 　  [hermes] Add UI testing #3003
• 　  [hermes] Initial commit of parser #3002

Latest Update: v3 — Compare vs v2

📚 Full Patch History

Links show the diff between the row version and the column version.

Version	v2	v1	Base
v3	vs v2	vs v1	vs Base
v2		vs v1	vs Base
v1			vs Base

⬇️ Download this PR

Branch

git fetch origin refs/heads/Gd55zt5pongyj3bujlmvo7grlayqh26b4 && git checkout -b pr-Gd55zt5pongyj3bujlmvo7grlayqh26b4 FETCH_HEAD

Checkout

git fetch origin refs/heads/Gd55zt5pongyj3bujlmvo7grlayqh26b4 && git checkout FETCH_HEAD

Cherry Pick

git fetch origin refs/heads/Gd55zt5pongyj3bujlmvo7grlayqh26b4 && git cherry-pick FETCH_HEAD

Pull

git pull origin refs/heads/Gd55zt5pongyj3bujlmvo7grlayqh26b4

Stacked PRs enabled by GHerrit.

[gemini-code-assist]

Summary of Changes

Hello @joshlf, I'm Gemini Code Assist¹! I'm currently reviewing this pull request and will post my feedback shortly. In the meantime, here's a summary to help you and other reviewers quickly get up to speed!

This pull request significantly refactors the parsing and attribute handling mechanisms within the Hermes tool. It introduces a new generic HermesDecorated struct to provide a more consistent and type-safe way of associating parsed items with their Hermes-specific attributes and documentation blocks. This change streamlines the ParsedItem enum and the process_item function, leading to more robust attribute extraction and improved error reporting. The updates also include modifications to various test fixtures to align with the new parsing logic.

Highlights

• Refactored ParsedItem Enum: The ParsedItem enum was refactored to use a new generic HermesDecorated struct, standardizing how items are associated with their Hermes attributes and blocks.
• Introduced HermesDecorated Struct: A new HermesDecorated<T, A> struct was introduced to encapsulate an item T and its HermesBlock<A>, improving type safety and consistency in attribute handling.
• Streamlined Attribute Processing: The process_item function was updated to directly accept attr::HermesBlock<attr::HermesAttr>, simplifying the attribute extraction logic and error handling.
• Centralized Doc Block Extraction: The extract_lean_block function was removed from parse.rs, and its functionality was likely consolidated or refactored into the attr module, with extract_hermes_block being made public.
• Updated Test Fixtures: Numerous test fixtures were updated to reflect the new attribute parsing mechanism, specifically by adding the , hermes tag to /// ```lean doc blocks and adjusting expected error messages.

🧠 New Feature in Public Preview: You can now enable Memory to help Gemini Code Assist learn from your team's feedback. This makes future code reviews more consistent and personalized to your project's style. Click here to enable Memory in your admin console.

Changelog

• tools/hermes/src/parse.rs
  • Refactored ParsedItem enum to use the new HermesDecorated struct for its variants.
  • Introduced the HermesDecorated struct to encapsulate an item and its HermesBlock.
  • Modified try_from_raw_reject_attr to accept HermesDecorated and handle attribute rejection.
  • Updated the process_item function signature and implementation to directly use attr::HermesBlock<attr::HermesAttr>.
  • Removed the extract_lean_block function, centralizing doc block extraction.
  • Adjusted name() and attrs() methods for ParsedItem to correctly access fields through HermesDecorated.
  • Added convert_block_infallible for converting Hermes blocks and handling attribute-related errors.
  • Added #[allow(dead_code)] attributes to lean_block and source_file fields in ParsedLeanItem.
• tools/hermes/src/scanner.rs
  • Updated process_file_recursive to correctly handle ParsedItem::Function variants (Impl, Trait, Free) when generating start_from paths.
  • Removed the use parse::ParsedItem::* statement due to the refactored ParsedItem structure.
• tools/hermes/tests/fixtures/broken_doc_block/expected_stderr.txt
  • Updated the expected error message for unclosed lean blocks to 'Unclosed Hermes block in documentation.'.
• tools/hermes/tests/fixtures/broken_doc_block/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/canonicalized_workspace/source/crates/app/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/cfg_blind_spot/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/collision/expected/crates/a/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/collision/expected/crates/b/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/collision/source/crates/a/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/collision/source/crates/b/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/complex_impl/expected/src/lib.rs
  • Updated doc blocks for impl methods to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/complex_impl/source/src/lib.rs
  • Updated doc blocks for impl methods to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/const_block_blind_spot/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/crlf_endings/expected/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/crlf_endings/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/custom_path_mod/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/cyclic_paths/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/deep_invocation/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/dir_mod/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/dirty_target_dir/expected/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/dirty_target_dir/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/double_mounted_mod/source/src/shared.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/duplicate_blocks/expected_stderr.txt
  • Updated the expected error message for duplicate lean blocks to 'Multiple Hermes blocks found on a single item.'.
• tools/hermes/tests/fixtures/duplicate_blocks/source/src/lib.rs
  • Updated doc blocks to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/empty_file/expected/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/empty_file/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/env_interleaved_stdout/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/external_path_dep/extra.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/feature_flags/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/file_mod/expected/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/file_mod/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/fs_missing_source/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/hermes_multiple_targets/source/src/bin/my_bin.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/hermes_multiple_targets/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/ignored_files/expected/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/ignored_files/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/impl_fallback_dedup/source/src/lib.rs
  • Updated doc blocks for methods within impl blocks to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/impl_path/expected/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/impl_path/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/inline_mod/expected/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/inline_mod/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/json_code_suggestions/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/json_linker_error/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/json_nested_children/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/large_assets/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/macro_blind_spot/source/src/hidden.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/map_external_dep/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/map_std_library/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/map_symlinked_file/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/missing_cfg_file/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/missing_cfg_mod/expected/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/missing_cfg_mod/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/mixed_workspace/expected/crates/app/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/mixed_workspace/source/crates/app/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/multi_artifact/expected/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/multi_artifact/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/multiple_errors/source/src/b.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/nested_file_mod/source/src/foo/bar.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/nested_item_error/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/nested_out_of_line_mod/source/src/hidden.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/nested_out_of_line_mod/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/non_standard_layout/expected/code/custom.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/non_standard_layout/source/code/custom.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/orphaned_entry/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/select_bin/expected/src/main.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/select_bin/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/select_bin/source/src/main.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/select_lib/expected/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/select_lib/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/select_lib/source/src/main.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/span_empty_unsafe_block/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/span_macro_expansion/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/span_mapping_basic/expected_stderr.txt
  • Updated the expected stderr output to reflect changes in span and error message.
• tools/hermes/tests/fixtures/span_mapping_basic/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/span_multibyte_offsets/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/split_artifact/expected/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/split_artifact/expected/src/main.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/split_artifact/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/split_artifact/source/src/main.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/split_personality_mod/source/src/a.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/start_patterns/source/src/lib.rs
  • Updated doc blocks to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/target_selection/expected/src/main.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/target_selection/source/src/main.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/ui_build_script_noise/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/ui_hanging_build/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/ui_phantom_success/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/ui_silent_panic/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/ui_the_flood/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/ui_visual_ghosting/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/unsafe_redaction/expected/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/unsafe_redaction/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/virtual_workspace/expected/crates/a/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/virtual_workspace/source/crates/a/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/warn_cfg_attr_path/source/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/weird_functions/expected/src/lib.rs
  • Updated doc blocks for various function types to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/weird_functions/source/src/lib.rs
  • Updated doc blocks for various function types to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/workspace_path_dep/expected/app/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.
• tools/hermes/tests/fixtures/workspace_path_dep/source/crates/app/src/lib.rs
  • Updated the doc block to include the hermes tag: /// ```lean, hermes.

Activity

• The pull request is currently marked as 'Work In Progress' ([WIP] Agent), indicating it is not yet ready for final review or merging.
• No specific human comments or reviews have been recorded for this pull request yet.

Using Gemini Code Assist

The full guide for Gemini Code Assist can be found on our documentation page, here are some quick tips.

Invoking Gemini

You can request assistance from Gemini at any point by creating a comment using either /gemini <command> or @gemini-code-assist <command>. Below is a summary of the supported commands on the current page.

Feature	Command	Description
Code Review	/gemini review	Performs a code review for the current pull request in its current state.
Pull Request Summary	/gemini summary	Provides a summary of the current pull request in its current state.
Comment	@gemini-code-assist	Responds in comments when explicitly tagged, both in pull request comments and review comments.
Help	/gemini help	Displays a list of available commands.

Customization

To customize Gemini Code Assist for GitHub experience, repository maintainers can create a configuration file and/or provide a custom code review style guide (such as PEP-8 for Python) by creating and adding files to a .gemini/ folder in the base of the repository. Detailed instructions can be found here.

Limitations & Feedback

Gemini Code Assist may make mistakes. Please leave feedback on any instances where its feedback is incorrect or counter productive. You can react with 👍 and 👎 on @gemini-code-assist comments. If you're interested in giving your feedback about your experience with Gemini Code Assist for Github and other Google products, sign up here.

You can also get AI-powered code generation, chat, as well as code reviews directly in the IDE at no cost with the Gemini Code Assist IDE Extension.

Footnotes

1. Review the Privacy Notices, Generative AI Prohibited Use Policy, Terms of Service, and learn how to configure Gemini Code Assist in GitHub here. Gemini can make mistakes, so double check it and use code with caution. ↩

[gemini-code-assist]

Code Review

This pull request introduces a significant and well-executed refactoring of the Hermes annotation parsing logic. The introduction of the HermesDecorated struct provides a more unified and cleaner representation for parsed items. The change to require an explicit hermes tag in the doc block info string is a good improvement for parsing robustness. The codebase is more maintainable as a result of these changes. I have one suggestion regarding some fields marked with #[allow(dead_code)] that could be cleaned up for better clarity.

[gemini-code-assist]

The fields lean_block and source_file are marked with #[allow(dead_code)], and the accompanying TODO for lean_block suggests they might be unused. A review of the call sites in scanner.rs confirms that these fields are not used in the main application logic after being populated, although lean_block is used in tests within this file.

• lean_block: This field contains the extracted Lean code, which is central to Hermes's purpose. If it's intended to be used later, the #[allow(dead_code)] should be removed. If not, and the code is extracted by a later stage, this field should be removed to avoid confusion.
• source_file: This seems redundant, as the file path information is already captured in the NamedSource used for error reporting.

To improve maintainability, it would be best to either integrate these fields into the application logic or remove them if they are indeed redundant.

[codecov-commenter]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 91.87%. Comparing base (cbe14fa) to head (c123e30).

Additional details and impacted files

@@                        Coverage Diff                         @@
##           Gr5hnlfzgkxvo5cdwir7s5hxfhlji6xjd    #3050   +/-   ##
==================================================================
  Coverage                              91.87%   91.87%           
==================================================================
  Files                                     20       20           
  Lines                                   6057     6057           
==================================================================
  Hits                                    5565     5565           
  Misses                                   492      492           

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[joshlf]

Squashed into #3051