Repository navigation
PVL-001 EV-5a: pin Mathlib, scoped Lean warning gate, orphan allowlist #4122
Description
PVL-001 EV-5a (see the PVL-001 spec and the infra PVL ledger). It is the root of the EV-6a → EV-7a → EV-8a/8b → EV-9 chain, so it unblocks #4083.
Scope:
- pin Mathlib;
- add a scoped Lean warning gate;
- add an orphan allowlist.
The Lean build runs on lambda: about 90 min warm, and lambda compute is pre-authorized. No workflow edit.
Done when:
- the pinned build is reproducible from a clean cache;
- the warning gate goes RED on a planted warning inside its scope and ignores one outside it;
- the orphan allowlist goes RED on a new unlisted orphan.
Filed by the cop (aprender-cf); owner aprender-6c [8b6b78].
Activity
fix(lean gate): a lake that prints ././././ProvableContracts/... slip…
fix(lean gate): the build fixtures were never committed -- the root .…
fix(lean gate): a cold cache hid a failed build, and the root module'…
fix(lean build): `cache get` never unpacked on a fresh checkout -- th…
fix(orphans): a `--` line comment containing `/-` opened a block that…
noahgift commentedon Sep 24, 2026
EV-5a is implemented on
feat/4122-pvl-5a-mathlib-pin. It stopped at the receipt: no PR is armed. Code headd18e411aa, receipt on top.lakefile.lean@ "master"→@ "1d042d3e1e93904b24c4fe209c75d2adbb22ee24"; the manifest'sinputRevmatches itsrev.lean/build.sh:lake exe cache get+unpack, thenlake build(rc read directly), then a gate over the log;ProvableContracts.leanorProvableContracts/**→ RED;decline: mathlib cache miss -- not a verdict;lean/check-orphans.sh+orphan-allowlist.yaml: 162 modules, 103 in the root's import cone, 59 orphans, all allowlisted (PVL EV-5a orphan group ProvableContracts.Theorems: 55 module(s) outside the root import cone #4124: 55 Theorems, PVL EV-5a orphan group ProvableContracts.Defs: 4 module(s) outside the root import cone #4125: 4 Defs). An unlisted orphan, a ticketless or reasonless entry, or a stale entry → RED.Alibi.BasicandAlibi.Slopesboth declaredProvableContracts.Alibi.alibi_slope_pos, solake buildfailed with "environment already contains". Slopes' theorem is renamedalibi_slope_real_pos, andcontracts/contracts.ntis regenerated (9 triples;pv extract --checkis a fixed point).lake exe cache getnever unpacks on a fresh checkout when~/.cache/mathlibalready holds the .ltar files. It printed "No files to download", unpacked 0 oleans, and the build then compiled Mathlib from source. The gate declined that correctly (4979 Mathlib modules, rc 2).Acceptance, lambda, fresh checkout (no
.lake):Decompressing 8101 file(s)Build completed successfully (16435 jobs)./build.shrc 0 in 804 sThe machine-level
~/.cache/mathlibwas warm. An empty machine cache was not measured.Self-tests (each mutant is killed by its named row; a crash is refused, never counted as a kill):
build.sh: 10 fixtures, 8 mutants + crash controlcheck-orphans.sh: 10 fixtures, 6 mutants + crash controlQuorum, degraded: same-family (agy out):
d18e411aaThe lanes' fixes: the cache-miss decline masked failed builds, root-module warnings were out of scope, the fixtures were gitignored by
*.log, a crash counted as a kill, and doc-comment imports counted. Receipt:docs/audits/quorum-GH-4122-pvl-5a-degraded.json.receipt-lintrefuses same-family lanes until #363, so that artifact is where this stops.Spec mismatch for infra PVL-001 §EV-5a: the probe greps the lakefile for
inputRev := "<40-hex>", andlakefile.leanhas no such syntax (the pin isrequire … @ "<rev>"). A correctly pinned lakefile fails that probe, so it needs amending rather than gaming.docs(audit): #4122 EV-5a degraded quorum -- Sonnet 5 PASS + Fable 5.1…
chore(roadmap): register PMAT-4122 (EV-5a) for the quorum kind-gate
docs(audit): #4122 EV-5a quorum -- 3/3 gemini PASS on 486bd9f, receip…
noahgift commentedon Sep 24, 2026
The foldable quorum receipt is in: 3/3 gemini PASS (3.1-pro-high, 3.8-flash-high, 3.7-flash-high) on judged head
486bd9ff1, whose code isd18e411aa.receipt-lintis clean (receipt complete: kind=artifact lanes=3). Artifactdocs/audits/quorum-PMAT-4122.jsonis committed on top as0bfa011a9. Nothing is armed; this stops at the receipt.fix(split): move 29 contracts whose tests or bins live in PR-2 out of…
1 remaining item
noahgift commentedon Oct 12, 2026
EV-5a evidence: clean-cache build on
main@03d4af19f0(aprender-78; branch-only lane, no PR)EV-5a reached
mainthrough #4655, so this checks the landed state rather than the old branch: 91 of 93 branch files are identical tomain, andmainhas since refinedbuild.shandorphan-allowlist.yaml.lake-manifest.jsonlocks Mathlibrev=inputRev=1d042d3e1e93904b24c4fe209c75d2adbb22ee24. The toolchain isleanprover/lean4:v4.29.0-rc4..lake. Plain./build.sh(fetch, cache, build, judge) gave rc 0 in 575 s, withlake build rc=0, 0 warning(s) in ProvableContracts/.check-orphans.shreportsmodules=161 in-cone=107 orphans=54 allowlisted=54.build.sh --self-testPASS, andcheck-orphans.sh --self-testPASS.lakeon PATH.build.shfailed closed with rc 2 and named the missing tool. I re-ran it on a fresh.lakewith the toolchain on PATH.Evidence only. I am not closing anything.
noahgift commentedon Oct 14, 2026
Folded into #5310 as a checklist row (TRIAGE-100, 2026-10-14): the open-ticket cap is 100, so this ticket is now tracked on that master and closed as not planned. Nothing is lost: reopen it when its work resumes, and an open PR for it reopens it. Pushed branch:
5d/4122-orphans-wire.Agent: aprender-clerk