[WIP] Parser + --allow-sorry #2969
Conversation
gherrit-pr-id: G101266ed5cfc0fe74d16aaae0785d9622e8da5be
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 introduces a significant architectural change to how Lean specifications and proofs are processed from Rust source code. By transitioning to an AST-based parser, the system gains improved reliability and maintainability. The addition of the 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. 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 introduces a new --allow-sorry flag and refactors the parser to use syn instead of regular expressions. This is a significant improvement, making the parser more robust and the tool more flexible. The implementation is solid, including updates to the build process to enforce the sorry policy and comprehensive test updates. I have a few minor suggestions to improve code clarity and test portability.
| // strip leading @ and space? | ||
| // User types `///@ ...` -> extracted `@ ...` | ||
| // If we just extract `@`, we get ` ...` | ||
| // The user might put `///@ ...`. | ||
| // If I strip `@`, I get ` ...`. | ||
| // I should probably strip the leading `@` and one optional space? | ||
| // `trimmed` starts with `@`. |
There was a problem hiding this comment.
These comments appear to be leftover development notes. They can be removed to improve code clarity.
| std::os::unix::fs::symlink(&shared_packages, &dest_packages) | ||
| .expect("Failed to symlink packages"); |
There was a problem hiding this comment.
The use of std::os::unix::fs::symlink makes these integration tests non-portable, as it will fail to compile on non-Unix platforms like Windows. If supporting tests on Windows is a goal, consider using conditional compilation (#[cfg(unix)] and #[cfg(windows)]) with std::os::windows::fs::symlink_dir for the Windows case.
| } | ||
| } | ||
| if !dest_build.exists() { | ||
| std::os::unix::fs::symlink(&shared_build, &dest_build).expect("Failed to symlink build"); |
There was a problem hiding this comment.
Similar to the other usage in this file, std::os::unix::fs::symlink is not portable to Windows. Consider a cross-platform approach if Windows test support is needed.
1 participant
Latest Update: v5 — Compare vs v4
📚 Full Patch History
Links show the diff between the row version and the column version.
⬇️ Download this PR
Branch
git fetch origin refs/heads/G101266ed5cfc0fe74d16aaae0785d9622e8da5be && git checkout -b pr-G101266ed5cfc0fe74d16aaae0785d9622e8da5be FETCH_HEADCheckout
git fetch origin refs/heads/G101266ed5cfc0fe74d16aaae0785d9622e8da5be && git checkout FETCH_HEADCherry Pick
git fetch origin refs/heads/G101266ed5cfc0fe74d16aaae0785d9622e8da5be && git cherry-pick FETCH_HEADPull
Stacked PRs enabled by GHerrit.