fix: refuse a window whose declarations could not be read, instead of reporting it empty

[roed-math]

facts.collect skips any module page whose read raises DocsError, on the understanding that the page is unpublished. But DocsError is also what Docs.declarations raises when a page comes from a different build than the one the run committed to ("the site is redeploying and this run cannot describe one build"), and what the transport raises for a timeout, a 403, a 429 or a 5xx. test_docs.py describes the redeploy case as a refusal ("Refusing is the honest outcome ... the next run closes the window cleanly"), but in facts it became a silent skip. A run that straddles a deploy drops every page it reads after the deploy, the writing model is handed a window with few or no declarations, and it reports that nothing happened.

Three reports on TauCetiRoadmap have come out of this, each opened within an hour of a docs deploy (the cache TTL, during which a run can straddle two builds):

• ClassFieldTheory, progress: ClassFieldTheory report for 2026-09-26 TauCetiRoadmap#455, window 93386bc..de52a34: "No new ClassFieldTheory declaration is recorded in this window", for 72 merged pull requests. Extracting the same window finds 501 declarations (336 new) in 87 files. The docs deployed at 20:08 UTC on 2026-09-26 and the report was opened at 20:53. It landed and was announced on Zulip.
• PDE, progress: PDE report for 2026-09-26 TauCetiRoadmap#463, and AlgebraicCodingTheory, progress: AlgebraicCodingTheory report for 2026-09-26 TauCetiRoadmap#464, both ending at 759eb3e. PDE says "No new mathematical declarations are recorded in this window" for 56 pull requests. AlgebraicCodingTheory marks every layer unassessed. The docs deployed at 04:13 UTC on 2026-09-27 and they were opened at 04:17 and 04:19. Neither has landed.

Changes

• docs.py: a 404 from the site raises the new DocsNotFound, a subclass of DocsError. Every other transport failure stays a plain DocsError.
• facts.py: only DocsNotFound is skipped. Any other DocsError from a module page, including the redeploy refusal, raises FactsError.
• facts.py, a backstop: if the window has pull requests but no declaration can be attributed to any of them, collect raises FactsError whatever the cause. The message gives the counts: pull requests, merge commits found, Lean files changed, and pages with no published page.
• cli.py: facts prints a FactsError to stderr and exits 1 without writing its output. The worker already treats a non-zero facts as a failed round, so no model is started and no pull request is opened.

Tradeoffs

• Genuinely empty windows wait. A window whose pull requests changed no declaration (comments, imports or non-Lean files only) is now refused, and stays open until a pull request that does change one lands. With MIN_PRS = 10, an empty window is much more likely to be a failed extraction than a real one.
• Refusals after a deploy. For up to the cache TTL after a deploy, a cached probe page can keep source_commit() on the old build. A run in that period now refuses instead of publishing a hollow report. The first run after the probe expires plans against the new build.

Tests

• test_facts.py gains three tests: a redeploy-mid-run regression, the empty-window backstop, and the CLI exit code.
• test_an_undocumented_module_contributes_nothing now checks that an unpublished module is skipped while the rest of the window is still reported.
• test_docs.py checks that only a 404 becomes DocsNotFound; a 403, 429, 503 and an unreachable host do not.

Each new test fails when the corresponding part of the fix is reverted. ./tests/run passes.

Not addressed here: the ClassFieldTheory entry already in TauCetiRoadmap's PROGRESS.md, which needs a reviewed correction in that repository.

🤖 Generated with Claude Code

[roed314]

There is still a mixed-build correctness hole that can publish a partial report.

DocsNotFound is inferred solely from an HTTP 404, but a 404 does not identify which docs build answered. With the per-page disk cache, this sequence is possible:

source_commit() is anchored to build A from a still-fresh cached probe page.
One changed module page is also served from the build-A cache and contributes declarations.
The docs site deploys build B.
Another changed module page is not cached and returns 404 from build B (for example because that module was removed / is no longer imported in B).
facts.collect treats that as a benign unpublished page and skips it.
The empty-window backstop does not fire because the first page already contributed declarations, so the report is nonempty but incomplete.

That is the same redeploy incoherence this PR is fixing, except it loses only some pages rather than all of them. A 404 should only be accepted as “unpublished” if the absence can be validated against the build already chosen by source_commit(); otherwise the window should be refused conservatively.

Please add a regression test with one contributing cached page from the old build plus one uncached page that becomes 404 after the deploy, and assert that collection refuses rather than emitting partial facts.

Generated by GPT-6 Pro.