From bf89e2615ed91b1149dcf6d8f4084c1f0eafd512 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Fri, 9 Oct 2026 09:10:27 +0000 Subject: [PATCH] fix: mathlib4 breakage from the import-graph main merge MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `downstream: update repo import-graph` (494de840) brought in [import-graph#173](https://github.com/leanprover-community/import-graph/pull/173), 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` in `ImportGraph/WorkspaceModel/Summary.lean` was guarding against — and having succeeded, the guard became unsatisfiable: `assert_not_exists` registers a global entry that `#check_assertions` expects to be *satisfied* once the whole library is available, and nothing in the closure provides `Lake.Workspace` any more. `mathlib4`'s `MathlibTest.AssertImported` (`import Mathlib` plus `#check_assertions!`) therefore warns warning: MathlibTest/AssertImported.lean:9:0: ❌️ 'Lake.Workspace' (declaration) asserted in 'ImportGraph.WorkspaceModel.Summary'. and the `test` phase, which runs with `--iofail`, fails on it. There is no `✖` anywhere: the one warning is the whole failure. The same upstream PR added `ImportGraphTest.NoLakeAxioms`, 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 drop the stale assertion and point 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. Verified on `nightly-2026-10-08`: `import-graph` `lake build` (122 jobs) and `lake test` (143 jobs, `NoLakeAxioms` among them) pass; `mathlib4` `lake build Mathlib Archive Counterexamples Wanted cache --wfail` (18386 jobs, 8723 modules compiled from scratch), `lake test --iofail` (18908 jobs) and `lake lint` all pass. Note the edit invalidates the artifact cache for `import-graph` and everything downstream of it, so the next CI run rebuilds that subtree once. Co-Authored-By: Claude Opus 5 --- import-graph/ImportGraph/WorkspaceModel/Summary.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/import-graph/ImportGraph/WorkspaceModel/Summary.lean b/import-graph/ImportGraph/WorkspaceModel/Summary.lean index b16f9d24f..d201c3dd0 100644 --- a/import-graph/ImportGraph/WorkspaceModel/Summary.lean +++ b/import-graph/ImportGraph/WorkspaceModel/Summary.lean @@ -17,9 +17,7 @@ public import Lake.Util.Version ``` These provide `Glob` and `ToolchainVer` in `WorkspaceSummary` field types. Cache validation also uses `Lake.Build.Trace` for hashing. None of these imports brings in Lake workspace loading or -the build type-family axioms. +the build type-family axioms; `ImportGraphTest.NoLakeAxioms` checks that. For Lake interaction with `WorkspaceSummary`, import `ImportGraph.WorkspaceModel.Summary.Lake`. -/ - -assert_not_exists Lake.Workspace -- ensure we do not import deep lake internals