[WIP] More cleanup #2980
[WIP] More cleanup #2980
Conversation
gherrit-pr-id: Gb76183f21575d7d2bd0229e4b027d491dae4f5c2
Summary of ChangesHello @joshlf, I'm Gemini Code Assist1! 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 focuses on a series of cleanup and enhancement tasks across the Hermes verification tool. The changes aim to improve the internal architecture, particularly how Rust code is parsed and translated into Lean specifications, and to enhance the user experience through clearer CLI documentation and more robust module handling. Key improvements include a more structured approach to parsing Lean directives, better tracking of module paths for accurate Lean generation, and the introduction of 'verification roots' for selective analysis. The overall impact is a more maintainable, understandable, and powerful verification pipeline. Highlights
🧠 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
Activity
Using Gemini Code AssistThe 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
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 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
|
![gemini-code-assist[bot]](https://avatars.githubusercontent.com/in/956858?s=60&v=4){kind=small}
There was a problem hiding this comment.
Code Review
This pull request is a significant and valuable cleanup of the Hermes codebase. The refactoring greatly improves code clarity, maintainability, and documentation across multiple modules, especially in desugar.rs, parser.rs, and pipeline.rs. The introduction of features like selective extraction via verification roots (--start-from) and the improved testing infrastructure are excellent additions. The code is now more idiomatic and easier to follow. I've identified a few areas for improvement, including a potential regression in how structs are parsed and some minor code cleanup opportunities.
| let invariant = | ||
| if !invariant_lines.is_empty() { Some(invariant_lines.join("\n")) } else { None }; | ||
|
|
||
| if let Some(inv) = invariant { | ||
| self.structs.push(ParsedStruct { | ||
| ident: node.ident.clone(), | ||
| generics: node.generics.clone(), | ||
| invariant, | ||
| invariant: Some(inv), | ||
| path: self.current_path.clone(), | ||
| }); | ||
| } |
There was a problem hiding this comment.
This change appears to be a regression. The new logic only collects structs that have an explicit ///@ lean invariant. The previous implementation collected all structs, which is necessary because even structs without a custom invariant may require a default Verifiable instance for proofs involving them to compile. It's recommended to restore the behavior of collecting all structs to avoid potential compilation errors in the generated Lean code.
if !self.structs.iter().any(|s| s.ident == node.ident && s.path == self.current_path) {
self.structs.push(ParsedStruct {
ident: node.ident.clone(),
generics: node.generics.clone(),
invariant,
path: self.current_path.clone(),
});
}| // This file may not be copied, modified, or distributed except according to | ||
| // those terms. | ||
|
|
||
| use anyhow::{Context, Result, anyhow}; |
There was a problem hiding this comment.
The Context and anyhow imports are not used in this file and can be removed to keep the imports clean.
| use anyhow::{Context, Result, anyhow}; | |
| use anyhow::Result; |
| if !content.is_empty() { | ||
| invariant_lines.push(content.to_string()); | ||
| } | ||
| } else { | ||
| match current_mode { | ||
| Some("invariant") => { | ||
| let content = trimmed[1..].trim(); | ||
| invariant_lines.push(content.to_string()); | ||
| } | ||
| None => { | ||
| self.errors.push(anyhow::anyhow!( | ||
| "Found `///@` line without preceding `lean invariant` on struct '{}'", | ||
| node.ident | ||
| )); | ||
| } | ||
| _ => {} | ||
| invariant = Some(content.to_string()); | ||
| // We assume only one invariant block for now or take the last? | ||
| // Or we could join them? Hermes usually expects one block. | ||
| // Let's just break after finding one for simplicity or join if multiline logic needed? | ||
| // But `iter_hermes_lines` yields *lines*. | ||
| // If the user writes: | ||
| // ///@ lean invariant | ||
| // ///@ x > 0 | ||
| // ///@ y > 0 | ||
| // We need to capture subsequent lines. | ||
| // The `parse_hermes_tag` only handles match on the SAME line or activation. | ||
| } | ||
| } else if invariant.is_some() { | ||
| // Append continuation lines if we are in invariant mode? | ||
| // But `iter_hermes_lines` loop doesn't maintain state easily across iterations if we don't track it. | ||
| // We need `current_mode` state tracking like in `visit_item_fn`. | ||
| } | ||
| } |
There was a problem hiding this comment.
This block of code and its associated comments appear to be leftovers from a previous refactoring attempt. The logic here is flawed (as noted in the comments themselves) and is superseded by the correct implementation that follows. This should be removed to avoid confusion for future readers.
| funs_external_content.push_str(" Result.ok (Classical.choose h)\n"); | ||
| } | ||
| funs_external_content.push_str(" else\n Result.fail Error.panic\n\n"); | ||
| funs_external_content.push_str(" else\n Result.fail Error.panic\n"); |
There was a problem hiding this comment.
For better readability in the generated FunsExternal.lean file, consider adding an extra newline after this line. This will visually separate the model definition from the end namespace statements that follow.
| funs_external_content.push_str(" else\n Result.fail Error.panic\n"); | |
| funs_external_content.push_str(" else\n Result.fail Error.panic\n\n"); |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
2 participants
⬇️ Download this PR
Branch
git fetch origin refs/heads/Gb76183f21575d7d2bd0229e4b027d491dae4f5c2 && git checkout -b pr-Gb76183f21575d7d2bd0229e4b027d491dae4f5c2 FETCH_HEADCheckout
git fetch origin refs/heads/Gb76183f21575d7d2bd0229e4b027d491dae4f5c2 && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/Gb76183f21575d7d2bd0229e4b027d491dae4f5c2 && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.