fix: mathlib4 breakage from the import-graph main merge

[downstream-lean4]

Run 37905266313 on nightly-2026-10-08: mathlib4 went red in its test phase, having been green in the previous run. The only new commit is downstream: update repo import-graph (494de84).

mathlib4 — fixed in import-graph

That merge brought in import-graph#173 (80a81552, merged 08:25Z, eleven minutes before the run), which cuts Lake.Config.Workspace and Lake.Load.Workspace out of the import closure of ImportGraph and ImportGraph.Tools by splitting the workspace-loading and cache-validation halves of WorkspaceModel.Summary.Lake apart. That is exactly what the

assert_not_exists Lake.Workspace -- ensure we do not import deep lake internals

at the bottom of ImportGraph/WorkspaceModel/Summary.lean was guarding against — and having succeeded, the guard became unsatisfiable. assert_not_exists registers a global entry that #check_assertions later expects to be satisfied once the whole library is available, and nothing in the closure provides Lake.Workspace any more. MathlibTest/AssertImported.lean is import Mathlib plus #check_assertions!, so it warns

warning: MathlibTest/AssertImported.lean:9:0: ❌️ 'Lake.Workspace' (declaration) asserted in 'ImportGraph.WorkspaceModel.Summary'.

and lake test --iofail fails on it. There is no ✖ anywhere in the run: the single warning is the whole failure, and build and lint were green.

The same upstream PR added ImportGraphTest/NoLakeAxioms.lean, which checks the property directly and strictly more thoroughly — the workspace and build modules absent from the imports of ImportGraph and ImportGraph.Tools, no Lake.* axioms in the environment, no leaked ImportGraph.Lake.IO.getWorkspace — so this drops the stale assertion and points the module docstring at that test instead.

Fixing it in import-graph rather than in the Mathlib test is deliberate. The alternative — making the assertion satisfiable again — means importing Lake.Config.Workspace into MathlibTest/AssertImported.lean, i.e. putting back into Mathlib's test environment the dependency import-graph#173 just removed. Upstream main still carries the stale line, so this wants to go to import-graph as well; import-graph builds on a release toolchain and never builds Mathlib, so its own CI cannot see this.

Verified on nightly-2026-10-08

repo	phase	result
import-graph	lake build	122 jobs, green
import-graph	lake test	143 jobs, green (incl. ImportGraphTest.NoLakeAxioms)
mathlib4	lake build Mathlib Archive Counterexamples Wanted cache --wfail	18386 jobs, green — 8723 modules compiled from scratch, no warnings
mathlib4	lake test --iofail	18908 jobs, green — #check_assertions! now silent
mathlib4	lake lint	green (Linting passed for Mathlib)

import-graph defines no lint driver; reference-manual and the verso repos are untouched by this PR.

Not in this PR

The rest of the red set is unchanged from the previous rounds and still covered by two open PRs: verso by #145 and reference-manual (skipped behind verso, together with verso-slides and verso-web-components) by #148. 494de84 touches import-graph/ only, which is outside that red set's dependency closure, so their verification on this nightly carries over. master needs all three merged to go green.

Note this edit invalidates the artifact cache for import-graph and everything downstream of it — mathlib4, repl, cslib, doc-gen4 and the rest — so the next CI run rebuilds that subtree once. The change is inert for every consumer other than MathlibTest.AssertImported: an assert_not_exists entry is read by nothing but #check_assertions, and the only other use of that command in the tree, MathlibTest/AssertExists.lean, does not import Mathlib or import-graph.

[downstream-lean4]

Build report for fix: mathlib4 breakage from the import-graph main merge

Turned green:

Repo	Critical	Build	Test	Lint
mathlib4	✅	✅ in 15m 28s	✅ in 39s	✅ in 1m 31s

Stayed red

Repo	Critical	Build	Test	Lint
reference-manual	✅	🛑 by verso	⏭️	⏭️
verso		🟥 in 45s	⏭️	⏭️
verso-slides		🛑 by verso	⏭️	⏭️
verso-web-components		🛑 by verso	⏭️	⏭️

Stayed green

Repo	Critical	Build	Test	Lint
aesop	✅	✅ in 0s	✅ in 4s	⏭️
batteries	✅	✅ in 0s	✅ in 3s	✅ in 2s
import-graph	✅	✅ in 3s	✅ in 4s	⏭️
lean4-cli	✅	✅ in 0s	✅ in 0s	⏭️
plausible	✅	✅ in 0s	✅ in 2s	⏭️
ProofWidgets4	✅	✅ in 1s	✅ in 1s	⏭️
quote4	✅	✅ in 0s	✅ in 1s	⏭️
BibtexQuery		✅ in 1s	⏭️	⏭️
comparator		✅ in 2s	⏭️	⏭️
cslib		✅ in 29s	✅ in 9s	✅ in 3s
doc-gen4		✅ in 1s	⏭️	⏭️
illuminate		✅ in 1s	✅ in 10s	⏭️
lean4-unicode-basic		✅ in 0s	⏭️	⏭️
lean4export		✅ in 0s	✅ in 7s	⏭️
LeanSearchClient		✅ in 0s	✅ in 0s	⏭️
leansqlite		✅ in 3s	✅ in 20s	⏭️
nerodia		✅ in 1s	✅ in 21s	⏭️
repl		✅ in 0s	✅ in 50s	⏭️

View run

[downstream-lean4]

Superseded: mathlib4 fixed this upstream the other way round. MathlibTest/AssertImported.lean now does import Lake.Config.Workspace explicitly ("ImportGraph asserts Lake.Workspace is not imported, but Mathlib doesn't import it either. So import it for the sake of testing."), which arrived in master with downstream: update repo mathlib4 (f12aeda). mathlib4 is green on build/test/lint in run 38263225848 without this PR, so dropping import-graph's assert_not_exists Lake.Workspace guard is no longer needed — and keeping the guard is evidently what upstream wants. Closing; reopen if the assertion turns unsatisfiable again.