[WIP] Parser + --allow-sorry#2969
[WIP] Parser + --allow-sorry#2969joshlf wants to merge 1 commit intoGb0d4d182a8f82f845a81ba9cd36038cef442a30efrom
Conversation
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.
gherrit-pr-id: G101266ed5cfc0fe74d16aaae0785d9622e8da5be
joshlf
force-pushed
the
Gb0d4d182a8f82f845a81ba9cd36038cef442a30e
branch
from
c981d5b to
638d2d4
Compare
joshlf
force-pushed
the
G101266ed5cfc0fe74d16aaae0785d9622e8da5be
branch
from
fc5689c to
66869c5
Compare
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## Gb0d4d182a8f82f845a81ba9cd36038cef442a30e #2969 +/- ##
==========================================================================
Coverage 92.02% 92.02%
==========================================================================
Files 19 19
Lines 6029 6029
==========================================================================
Hits 5548 5548
Misses 481 481 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
2 participants
Latest Update: v6 — Compare vs v5
📚 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.