ci: preserve Lean comment context in OCR routing - #2142
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_ae4f1743-005c-445d-8633-047ca71ee425) |
|
@codex review |
OpenCodeReview first-pass reviewStatus: success · Mode: config-docs · 1 finding(s) · 2 files · 190805 tokens · 25 tool calls ✅ Posted 1 inline comment(s). OCR pilot metrics
Pilot mode: advisory only. Codex Review remains the merge gate. Inline findings that could not be posted
|
![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: fb62dc9dc4
ℹ️ 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".
| const stripped = stripLeanCommentsFromLine(line.text, { inBlockComment }); | ||
| inBlockComment = stripped.inBlockComment; |
There was a problem hiding this comment.
When an unchanged Lean context line contains the literal /- outside a comment, such as def marker := "/-", this new full-hunk pass still feeds it to stripLeanCommentsFromLine, sets inBlockComment, and then drops following added code until a -/ appears. That is a regression from scoring only changed lines: an added unsafe def, sorry, or axiom after that context line loses its risk signal and can be ranked below the packet cutoff in large Lean diffs.
Useful? React with 👍 / 👎.
fb62dc9 to
4f42920
Compare
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_5c503e83-d956-4546-ac2f-09854fbaf840) |
|
@codex review |
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: success · Mode: config-docs · 0 finding(s) · 2 files · 79499 tokens · 12 tool calls
No comments generated. Looks good to me.
OCR pilot metrics
- Routing: config-docs (router-v8)
- Changed files: 2 supported / 2 total; Lean 0, trust docs 0, workflow/scripts 2, contracts 0, docs 0
- Changed lines: 52 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 0; files 2; tokens 79499; tool calls 12; warnings 0; duration 179s
- Largest changed files: .github/scripts/test-ocr-routing.js (+35/-0), .github/scripts/ocr-router.js (+9/-8)
Pilot mode: advisory only. Codex Review remains the merge gate.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 4f4292008d
ℹ️ 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".
| const stripped = stripLeanCommentsFromLine(line, { inBlockComment }); | ||
| for (const line of hunk.lines || []) { | ||
| if (line.type === skipType) continue; | ||
| const stripped = stripLeanCommentsFromLine(line.text, { inBlockComment }); |
There was a problem hiding this comment.
Because unchanged context lines now drive inBlockComment through the Lean comment stripper, a normal Lean line such as def marker := "/-" in hunk context makes the router believe every following added line is inside a block comment until a later -/. In that scenario an added unsafe def/sorry loses its risk signal and large-Lean packet ranking under-scores the dangerous change, whereas the previous add-only scan still flagged it. The context scan needs to distinguish real block-comment delimiters from delimiters inside Lean strings before suppressing added code.
Useful? React with 👍 / 👎.
4f42920 to
5cb75e9
Compare
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_4901b198-1451-4b53-a874-76929a9926d6) |
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 5cb75e993d
ℹ️ 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".
| if (ch === '"') { | ||
| code += '""'; |
There was a problem hiding this comment.
When this branch sees the quote in a Lean interpolated string (s!"..."), it skips the whole literal, but the {...} sections are Lean expressions; repo code already uses s!"{...}" interpolation. An added proof line such as have _ := s!"{(by sorry : Nat)}" now produces no introduced sorry/admit signal, so large Lean diffs can under-rank or omit a hunk that introduced a real elaborated sorry.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: success · Mode: config-docs · 1 finding(s) · 2 files · 110312 tokens · 10 tool calls
✅ Posted 1 inline comment(s).
OCR pilot metrics
- Routing: config-docs (router-v8)
- Changed files: 2 supported / 2 total; Lean 0, trust docs 0, workflow/scripts 2, contracts 0, docs 0
- Changed lines: 132 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 1; files 2; tokens 110312; tool calls 10; warnings 0; duration 440s
- Largest changed files: .github/scripts/ocr-router.js (+43/-24), .github/scripts/test-ocr-routing.js (+65/-0)
Pilot mode: advisory only. Codex Review remains the merge gate.
| i = blockEnd + 2; | ||
| inBlockComment = false; | ||
| continue; | ||
| } |
There was a problem hiding this comment.
OpenCodeReview [bug · medium]
Lean 4 block comments are nestable: /- outer /- inner -/ still outer -/ is a single comment block. The rewritten parser does not track nesting depth when inBlockComment is true — it unconditionally exits block-comment mode at the first -/. For a hunk containing /- outer /- inner -/ sorry -/, the parser would exit the comment at the inner -/ and then treat sorry as real code, producing a false-positive OCR risk signal. This issue existed in the previous implementation as well, but since the parser was fully rewritten in this PR, it is worth addressing now by tracking a depth counter.
Suggested change:
if (inBlockComment) {
const blockEnd = text.indexOf('-/', i);
const blockStart = text.indexOf('/-', i);
if (blockEnd === -1) return { code, inBlockComment: true, depth };
if (blockStart !== -1 && blockStart < blockEnd) {
depth += 1;
i = blockStart + 2;
continue;
}
depth -= 1;
i = blockEnd + 2;
if (depth > 0) continue;
inBlockComment = false;
continue;
}
5cb75e9 to
8155073
Compare
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_1d3784f3-f638-42c7-a955-91d168b6f169) |
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 8155073e3d
ℹ️ 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".
| if (ch === '{') { | ||
| interpolationDepth += 1; | ||
| interpolation += ch; | ||
| } else if (ch === '}') { | ||
| interpolationDepth -= 1; |
There was a problem hiding this comment.
When a Lean string interpolation expression contains a brace inside a char/string literal before risky code, this loop still treats that brace as structural and stops scanning the interpolation too early. For example, an added line like def x := s!"{ let c := '}'; (by sorry : Nat) }" no longer gets the introduced sorry/admit signal, whereas the previous scanner did; in large Lean diffs that can drop the packet score enough to omit the actual sorry from bounded review. The interpolation scanner needs to ignore braces while it is inside nested Lean string/char literals.
Useful? React with 👍 / 👎.
OpenCodeReview first-pass reviewStatus: completed_with_errors · Mode: config-docs · 0 finding(s) · 2 files · 23893 tokens · 1 tool calls Some files could not be reviewed due to errors. Warnings
OCR pilot metrics
Pilot mode: advisory only. Codex Review remains the merge gate. |
8155073 to
aabb470
Compare
|
@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_a341561c-3298-4903-98fe-92b2e739f90c) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: aabb4709ef
ℹ️ 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".
| if (ch === "'") { | ||
| interpolationChar = true; | ||
| continue; |
There was a problem hiding this comment.
When a Lean interpolation contains a primed local like let x' := ..., this branch enters interpolationChar mode even though the apostrophe is part of an identifier. If there is no matching apostrophe before the closing brace, the scanner ignores the } and never calls stripLeanCommentsFromLine on the interpolation, so code such as s!"{ let x' := (by sorry : Nat); 0 }" loses the introduced sorry signal and can under-rank the hunk in large Lean diffs.
Useful? React with 👍 / 👎.
aabb470 to
e94d2d8
Compare
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_38e7a707-7c01-4614-9945-d119d0bc643f) |
|
@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_952b612d-bffc-4650-ac25-d326eda8299d) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 8eb4bb9fe8
ℹ️ 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".
| if (line.type === includeType && isOpenInterpolationState(stripped)) { | ||
| pendingChangedInterpolation = true; |
There was a problem hiding this comment.
When an added line opens a multiline s!"...{ interpolation and already contains risky code before the line break, this branch only marks the interpolation as pending and does not buffer the fragment now stored in stripped.stringInterpolationState.interpolation. For example, def note := s!"value { let x := (by sorry : Nat); followed by x }" is valid changed Lean code, but when the later line closes the interpolation the router rescans only the later pendingChangedInterpolationText, so the introduced sorry/admit signal is lost and large-Lean packet routing can under-rank the proof hole.
Useful? React with 👍 / 👎.
OpenCodeReview first-pass reviewStatus: error · Mode: config-docs · 0 finding(s) · files unknown OCR produced no JSON output OCR stderr highlightsOCR pilot metrics
Pilot mode: advisory only. Codex Review remains the merge gate. |
|
@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_d669611b-e512-46a3-b263-cefd71aef7d4) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 81ceffab28
ℹ️ 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".
| openInterpolation(); | ||
| return 1; | ||
| } | ||
| if (ch === '"') { |
There was a problem hiding this comment.
When a Lean raw string such as r#"said "hi""#; unsafe def risky : Nat := 0 contains an unescaped " before the terminating "#, this branch closes the scanner's string state at the inner quote instead of waiting for the matching hash delimiter. The scanner then treats the real terminator as the start of a new ordinary string and hides the following code, so hunks that add unsafe, sorry, or admit after such a raw string lose their high-risk routing signals; the previous comment-only stripper would still have seen that code.
Useful? React with 👍 / 👎.
OpenCodeReview first-pass reviewStatus: error · Mode: config-docs · 0 finding(s) · files unknown OCR produced no JSON output OCR stderr highlightsOCR pilot metrics
Pilot mode: advisory only. Codex Review remains the merge gate. |
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_600a01e6-8a30-4ffd-aeef-9bb0bb00c7c6) |
|
@codex review |
|
Codex Review: Didn't find any major issues. Chef's kiss. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
OpenCodeReview first-pass reviewStatus: error · Mode: config-docs · 0 finding(s) · files unknown OCR produced no JSON output OCR stderr highlightsOCR pilot metrics
Pilot mode: advisory only. Codex Review remains the merge gate. |
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_a8c14e0d-8d9b-46dd-8085-5b017bec8e25) |
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e90ed123b5
ℹ️ 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".
OpenCodeReview first-pass reviewStatus: error · Mode: config-docs · 0 finding(s) · files unknown OCR produced no JSON output OCR stderr highlightsOCR pilot metrics
Pilot mode: advisory only. Codex Review remains the merge gate. |
|
@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_b71471e1-9155-413e-8fae-6cd2f2b5e6a1) |
|
Codex Review: Didn't find any major issues. More of your lovely PRs please. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
OpenCodeReview first-pass reviewStatus: error · Mode: config-docs · 0 finding(s) · files unknown OCR produced no JSON output OCR stderr highlightsOCR pilot metrics
Pilot mode: advisory only. Codex Review remains the merge gate. |
1 participant
Summary
sorry/axiom/unsafeis not treated as codeValidation
node --check .github/scripts/ocr-router.jsnode --check .github/scripts/test-ocr-routing.jsnode --check .github/scripts/post-ocr-review.jsnode .github/scripts/test-ocr-routing.jsbash -n .github/scripts/ocr-git-wrapper.shpython3 -m json.tool .github/ocr/rules.json.github/workflows/ocr-review.yml/tmp/actionlint-bin/actionlint .github/workflows/ocr-review.ymlFixes the latest-head blocker reported on #2137: #2137 (comment)
Note
Medium Risk
Changes only CI OCR routing heuristics, but mis-parsing Lean could miss real proof risks or inflate packet scores; coverage is heavily regression-tested.
Overview
OCR Lean risk detection now walks each diff hunk with a stateful scanner instead of stripping comments line-by-line. Unchanged
ctxlines establish block comments, strings, and opens!"…{interpolations before added/deleted lines are classified, which fixes false positives when prose inside context-delimited/- … -/mentionssorry,axiom, orunsafe.The scanner understands nested block comments, line comments, raw strings (
r#"…"#), interpolated strings (including nested braces, quoted'}', and Unicode primed identifiers),«…»escaped ids, and char literals. Risk signals (sorry/admit,axiom,unsafe, imports) run on code extracted from changed sides only; theorem weakening uses a separate pass withpreserveStringsso literal and raw-string changes in theorem statements still compare correctly.test-ocr-routing.jsadds a large regression suite (context block comments, string delimiters, interpolation edge cases, and a parameterized blocker table).Reviewed by Cursor Bugbot for commit 35ed2a3. Bugbot is set up for automated code reviews on this repo. Configure here.