Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions .github/ocr/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ Before installing or invoking OpenCodeReview, `.github/scripts/ocr-router.js` co
- `no-supported`: OCR does not run because no changed files match the OCR include rules.
- `small-lean`: OCR runs with the current pilot bounds (`--concurrency 3`, `--timeout 20`, PR background capped at 1200 characters). This is used for Lean diffs of at most 1 Lean file and 300 supported changed lines.
- `medium-lean`: OCR runs with stricter bounds (`--concurrency 1`, `--timeout 12`, PR background capped at 800 characters). This is used for medium Lean diffs that are above the small threshold but below the large threshold.
- `large-lean-hotspots`: full-file OCR does not run. The trusted router parses diff hunks, builds a compact risk dossier, optionally asks a cheap/long-context scout model to rank dangerous packets, and posts bounded hotspot coverage. This triggers for at least 3 changed Lean files or more than 800 supported changed lines. If the diff exceeds the bounded packet budget, more than 12 Lean files or more than 2500 supported changed lines, or no safe packets can be produced, the same mode posts a concrete coverage report and checklist instead of a generic skip.
- `large-lean-hotspots`: full-diff OCR does not run. The trusted router ranks diff hunks, optionally using a scout, then runs bounded semantic reviews for selected file groups. This triggers for at least 3 changed Lean files or more than 800 supported changed lines. Overall PR size does not disable this route; at most eight packets and four groups are selected. If no safe packets can be produced, no semantic packet review runs and the report explicitly says so.
- `config-docs`: OCR runs with the current pilot bounds for supported non-Lean changes, including workflows, scripts, docs, trust/security surfaces, Solidity, Yul, Cairo, and config files.

Packetized Lean mode is intentionally partial. It checks deterministic signals first, including introduced `sorry`/`admit`/`axiom`/`unsafe`, changed imports, public declaration or theorem signature changes, trust-boundary documentation drift, and large deleted proof obligations. It then ranks hotspots such as `Compiler/Proofs/YulGeneration/**`, `Compiler/Proofs/**`, `Compiler/**`, `IRGeneration/**`, `Semantics/**`, trust docs, and public theorem statements.
Expand Down Expand Up @@ -56,7 +56,7 @@ All lens calls reuse the same per-call `scoutTimeoutMs` (240s) and run concurren

`.github/ocr/rubric.json` is a permanent, growing checklist of defect **classes** confirmed on past PRs (seeded with the three above). Every scout dossier embeds the rubric (`dossier.rubric`), and each lens also gets a lens-scoped `lens_rubric_focus` pointing it at the past defect classes it owns — so a class caught once is re-checked on every future review instead of being rediscovered serially. When a review confirms a **new** defect class, append it with the `appendRubricItem({ id, lens, title, check, origin })` helper in `ocr-router.js` (it de-dupes by `id`); that helper is also the wiring point for future automation. A missing/invalid rubric file is a soft failure — the scout still runs.

OpenCodeReview 1.7.5 is still invoked only for `small-lean`, `medium-lean`, and `config-docs` full-diff paths. The short-term bridge for `large-lean-hotspots` publishes scout/deterministic packet advisory comments and explicitly marks strong packet review as required but blocked on a safe OCR packet-window input mechanism. The posted comment lists the covered packets, packet budget, scout status, metrics, strong-review blocker, and residual risk. It must not be read as full review coverage or LGTM.
OpenCodeReview 1.7.9 reviews full diffs for `small-lean`, `medium-lean`, and `config-docs`. The `large-lean-hotspots` route reviews selected file groups using the packet runner described below. The posted report distinguishes scout triage from semantic review, lists covered groups and failures, and states residual risk. It must not be read as full review coverage or LGTM.

The hard guarded modes are fallback behavior only. During the pilot, a 3-file Lean PR consumed about 1.25M tokens, made 121 tool calls, and still ended as `completed_with_errors`; packetized review is meant to keep OCR useful without pretending it reviewed whole files.

Expand Down
5 changes: 1 addition & 4 deletions .github/scripts/ocr-router.js
Original file line number Diff line number Diff line change
Expand Up @@ -1440,7 +1440,7 @@ function buildSyntheticResult(decision, metrics) {
message: decision.reason,
comments: [],
warnings: decision.mode === 'large-lean-hotspots'
? [{ type: 'routing', message: 'Large diff receives bounded packet review only; full-diff OCR is not attempted.' }]
? [{ type: 'routing', message: 'No safe review packets could be produced; this diff received no semantic packet review. Use the top-changed-files checklist for manual review.' }]
: [],
summary: {
files_reviewed: 0,
Expand Down Expand Up @@ -1572,9 +1572,6 @@ function packetResidualRisk(decision) {
const basis = decision.scout?.attempted && decision.scout?.status === 'success' ? 'scout-ranked' : 'deterministically ranked';
return `Triaged top ${decision.packets?.length || 0} ${basis} packet(s); remaining changed hunks/files require Codex or human proof review, and selected packets still need strong reviewer analysis.`;
}
if (decision.mode === 'large-lean-hotspots' && ((decision.counts?.lean || 0) > THRESHOLDS.packetMaxFiles || (decision.changedLines || 0) > THRESHOLDS.packetMaxChangedLines)) {
return 'Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.';
}
if (decision.mode === 'large-lean-hotspots') {
return 'Router could not produce safe diff packets; use top changed files as required Codex/human review checklist.';
}
Expand Down
2 changes: 2 additions & 0 deletions .github/scripts/test-ocr-routing.js
Original file line number Diff line number Diff line change
Expand Up @@ -1365,6 +1365,8 @@ async function testLargeLeanScoutNoPacketsStatus() {
await router.applyScoutStage(decision, { files }, { url: 'https://example.invalid/v1', key: 'test-key', model: 'cheap-scout' });
assert.strictEqual(decision.scout.enabled, true);
assert.strictEqual(decision.scout.status, 'skipped_no_packets');
const result = router.buildSyntheticResult(decision, {});
assert.ok(result.warnings.some(w => w.message.includes('no semantic packet review')));
}

function testWorkflowDocsEnabled() {
Expand Down
Loading