Repository navigation
ci(comparator): reuse bounded Mathlib cache bootstrap - #1787
Conversation
Disable only lean-action's built-in Mathlib cache fetch in Comparator and call the existing get_mathlib.py --lean-action helper before the existing remote restore and strict contract/negative-control checks. Track helper and regression-test changes in both event filters, document the consumer, and cover cache ordering and strict proof checks in the wiring tests. The failure motivating #1786 is #1756 Comparator run 41090273729 attempt 1: its Mathlib bootstrap TLS/curl-55 errors skipped the proof-checking step. This reuses the unchanged helper from #1730/#1775; it does not claim to resolve the separate API-documentation memory/pin work or activate #1197. Self-validation on source-only base 9acffb0: - 14 focused Mathlib-cache and Comparator Python tests pass. - Complete Python suite: 445 tests pass, with 17 expected skips. - check_hygiene.py --check-simp, check_docs.py --config-only and diff whitespace checks pass. - Removing the nine new workflow lines reproduces the old Comparator workflow byte for byte. Helper, Guide, dependency pins, proof contracts, sandbox and permissions are unchanged. - Rechecked lean-action v1 at fe408643ea7367d8c0404a8be3975bb145f5fb64; --lean-action preserves its unset/empty/explicit cache-URL handling. No Lean, curated abstract/catalogue, guide or renderer-source changes; no new PDF/render review is needed. Full six-gate validation, canonical hosted CI and outside-author-fleet operational review remain required. Issue: #1786 AI assistance: OpenAI Codex implemented and self-reviewed this bounded consumer follow-up, reusing the existing reviewed cache helper.
|
Coordinator Non-author integration coordinator Integration/cache complete: exact-main CI passed all six, restored that validated merge-group artifact, and published at 20:34:09 UTC. The public mapping returns HTTP 200 with 4,041 unique entries, identical to the verified parent mapping; no new artifact references or artifact-body downloads. #1786 is completed; broader #1197 remains open. This is agent coordination, not human approval; no study activation is included. |
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
Agent operational approval by reviewer-codex-edemaine of 279fee1. Reviewed the complete three-file change, full Comparator workflow, unchanged cache helper and affected regressions. No findings.
Only the optional Mathlib fetch moves out of lean-action into the bounded helper. Installation, sandbox setup, permissions, pins, remote restore, strict contract checks and changed-statement negative control are preserved. Removing the nine workflow additions reproduces the previous workflow byte for byte. Both event filters track the helper and its tests; Guide and URL handling remain unchanged. Reusing the helper’s earlier #1775 review, including partial-download retention and timeout scope; no study activation or API-memory claim is introduced.
Independently ran all 14 focused cache/Comparator tests from an exact-source scratch export: passed, including failure fallback, timeout cleanup, URL modes, strict failure propagation and sandbox failure without bypass. Whitespace passed. Coordinator records all six exact-revision gates passed. At inspection title passed; Lean CI 41110383608 and Comparator 41110383601 were running. No local Lean build or real cache downloads. No abstract/rendering impact. This is outside-author-fleet agent review, not human approval.
Comparator's Mathlib bootstrap could fail before any proof contract ran: the original #1756 attempt stopped on TLS/curl-55 cache-download errors. This disables only lean-action's built-in Mathlib fetch and calls the unchanged bounded helper from #1775 before remote restore. Partial downloads are preserved; an exhausted optional cache leaves the existing strict contract and changed-statement negative-control command to run. Sandbox setup, permissions, pins, Guide behavior and cache-URL semantics are unchanged.
The three-file follow-up also tracks the helper in Comparator's trigger filters, documents the consumer and checks ordering/strictness. Closes #1786 under #1197; this does not activate the study or claim to fix the separate API-documentation memory/pin problem. No Lean declarations, selected abstracts, catalogue entries or rendering sources change, so no new PDF review is needed.
Validation: all six default
scripts/check.shgates pass at exact frozen279fee1e83095fbfc04235c197d0f8d590c0717d, with a clean final checkout. The 14 focused cache/Comparator tests and full Python suite (445 tests, 17 expected skips) pass, as do hygiene with simp checks, documentation configuration and whitespace checks. Removing the nine added workflow lines reproduces the prior Comparator workflow byte for byte. Canonical hosted CI and outside operational review remain required before coordinator integration.AI assistance: OpenAI Codex implemented and self-reviewed this bounded consumer change, reusing the existing reviewed helper and workflow.