Repository navigation
PVL-001 EV-9 — PVL-9: provable-ladder required on main #4083
Description
Aprender-side row of PVL-001 that blocks the ontology spec (ONT-001), which the operator requires finished in 0.70 ("the ontology spec MUST be finished in .7", relayed by the cop aprender-cf). IDs are SPEC-QUALIFIED: this is PVL-001 EV-9. APEX-001 reuses the same EV numbers, so a bare "EV-9" is ambiguous.
Row (paiml/infra docs/specifications/PVL-001-pv-lean-gate.md:214), verbatim: EV-9 aprender · "PVL-9: provable-ladder required on main" · depends_on EV-1, EV-4, EV-6a, EV-7a, EV-8b · K̂ 120
- depends_on (PVL-001): EV-1, EV-4, EV-6a, EV-7a, EV-8b
- K̂: 120
- blocks: ONT-5 (per infra's ONT-001 receipts), and through it the rest of ONT-001.
Activity
ci(pvl): provable-ladder -- the quorum's findings (#4083)
fold: #4083 discharge summary fresh (fix/4083-discharge-summary-fresh…
fold: #4083 EV-9 advisory provable-ladder job (feat/4083-pvl-9-provab…
fold: #4083 provable-ladder runs-on widened to clean-room X64 (ci/408…
noahgift commentedon Sep 25, 2026
Parked by APR-EPIC-001: over S2 budget (rank 10/38). Reopen = pull. Applied by aprender-d1: claude+agy both said close, apr shadow row recorded (handoff/close-quorum-2026-09-25.json).
docs(findings): provable-ladder on car #4429 declines on inputs that …
noahgift commentedon Sep 27, 2026
Reopened by the cop per operator directive 2026-09-27: provable-ladder required on main (PVL-001 EV-9) blocks the 0.71 Aeneas spike #4555. Today main requires only gate + workspace-test. Moving this to 0.71.0. Making the check required is a ruleset change, which needs the operator's go when it's ready to land.
4 remaining items
noahgift commentedon Sep 27, 2026
#4083 status — NOT done. The evidence and the remaining gaps are below.
Evidence, measured 2026-09-27:
provable-ladderjob, and no inputs (lean/build.sh,discharge-summary.jsonand the escape allowlist are all absent). None of the three*/4083-*branches is in main, release(0.70.0): sealed car — REPLACES #4372 #4429 or fold(B3): contracts / ONT / PVL / docs onto main — replaces #4317 #4431.axiomdecls) but no job. Its committed summary is stale (tree_sha 8671a7ac vs 04b963773).pv discharge runrc=1: 249/381 closed, with 132FAIL DUPLICATE. Every one was fan-in (one root bound by several contracts, so one row per Challenge file).Fixed on branch
52/4083-ladder-fanin@ f6f7606 (on #4431's head, branch-only):pv discharge runrc=0, 249/249 closed, axioms_ok and escapes_ok true (787 s). Unit tests: contracts 110 pass, cli 25 pass; fmt and clippy are clean.Remaining gaps:
pv lint contracts/is still RED on ontology gates, owned by infra-83:bash scripts/check_package_includes.sh/check_readme_claims.shas unresolved), PV-ONT-013, PV-ONT-011, and PV-ONT-033 (131 unrefined modules vs a baseline of 76).fix(ladder): quorum round 1 — nightly on x86-main's labels, per-host …
findings(EV-9): ladder SKIP reads as success; discharge summary bools…
fix(ci): a skipped provable-ladder is RED, not a pass (EV-9, #4083)
roadmap: rows for the #4083 (EV-9) and #4189 (G5) folds in PR-2 (C78,…
noahgift commentedon Oct 12, 2026
park proposal: parked, the issue already carries the
parkedlabel and its done-when (aprovable-ladderjob required inci / gateon main) is still unmet; the ladder runs only as a nightly. Making it a required check is a new gate and needs its own ruling.noahgift commentedon Oct 14, 2026
Folded into #4347 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:
52/4083-ladder-fanin,a2/4083-ev9-one-owner.Agent: aprender-clerk