ci: include Verity file types in OCR#2129
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_2dc68999-da13-4785-ab95-03e12581c8e6) |
|
@codex review |
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_bcdac9f0-dc68-4e26-b0af-0fe3947fae12) |
|
@codex review |
|
/ocr review |
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 73c70cb692
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
|
|
||
| concurrency: | ||
| group: ocr-review-${{ github.event.pull_request.number || github.event.issue.number || inputs.pr_number }} | ||
| group: ocr-review-${{ github.event.pull_request.number || github.event.issue.number || inputs.pr_number }}-${{ github.event_name }} |
There was a problem hiding this comment.
When a /ocr review comment or workflow_dispatch is fired while the automatic pull_request_target run for the same PR/commit is still running, appending github.event_name puts those runs in different concurrency groups, so cancel-in-progress no longer serializes or cancels them. The posting script only checks for an existing success tag before publishing (.github/scripts/post-ocr-review.js lines 20-24), so two concurrent runs can both pass that check and publish duplicate inline reviews while spending LLM tokens; keep the group keyed only by PR/commit or add a real per-commit posting lock.
Useful? React with 👍 / 👎.
1 participant
Summary
.leanchanges as unsupported.Test Plan
python3 -m json.tool .github/ocr/rules.jsonnode --check .github/scripts/post-ocr-review.jsbash -n .github/scripts/ocr-git-wrapper.shnpx -y @alibaba-group/open-code-review@1.7.5 review --previewon PR proof: bridge mappingPackedWord source reads (parallel/experimental) #2127 diff shows.leanfile will be reviewedNote
Low Risk
CI/OCR configuration only; no runtime app, auth, or data-path changes.
Overview
OCR will now review Verity-relevant paths instead of treating
.leanand similar changes as out of scope..github/ocr/rules.jsongains anincludelist for**/*.lean, Solidity/Yul/Cairo, trust docs (AUDIT.md,TRUST_ASSUMPTIONS.md,AXIOMS.md),README.md,docs/**/*.md, and.github/**/*, while existingexcludepatterns (e.g..lake, lockfiles) stay in place.The OCR workflow concurrency key in
ocr-review.ymlnow appendsgithub.event_name, so runs triggered by different events on the same PR (e.g.pull_request_targetvsissue_comment/ocr review) no longer share one group and cancel each other whencancel-in-progressis enabled.Reviewed by Cursor Bugbot for commit 73c70cb. Bugbot is set up for automated code reviews on this repo. Configure here.