From 0e272ef0201ec3fe89a78d1ef0650d37a8ea1de4 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 6 Sep 2026 14:45:39 +0000 Subject: [PATCH] fix: reference-manual breakage from nightly-2026-09-06 `lean4#15015` added the `precompileImports` field to Lake's `LeanConfig` and `precompileLibrary` to `LeanLibConfig`. The manual embeds elaborated package configurations verbatim in `expected` blocks, so all of them were missing the new fields and `Manual.BuildTools.Lake.Config` failed with `Mismatched elaborated configuration output`. Added `precompileImports := false` after `platformIndependent` in every embedded `LeanConfig`, and `precompileLibrary := false` in the `lean_lib` configurations, in `Manual/BuildTools/Lake/Config.lean` and `Manual/BuildTools/Lake.lean`. CI never saw this: `reference-manual` has been skipped behind the `verso` failure since the shared-`subverso` build-directory problem started. Verified: `lake build` completes (1180/1180). The repo defines no test or lint driver, so `lake check-test`/`lake check-lint` fail and CI skips both phases. --- reference-manual/Manual/BuildTools/Lake.lean | 12 ++++++++++++ reference-manual/Manual/BuildTools/Lake/Config.lean | 12 ++++++++++++ 2 files changed, 24 insertions(+) diff --git a/reference-manual/Manual/BuildTools/Lake.lean b/reference-manual/Manual/BuildTools/Lake.lean index 7fe5ca6d3..8bdafd3c1 100644 --- a/reference-manual/Manual/BuildTools/Lake.lean +++ b/reference-manual/Manual/BuildTools/Lake.lean @@ -728,6 +728,7 @@ root = "Tests" weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, @@ -793,6 +794,7 @@ root = "Tests" weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, @@ -828,6 +830,7 @@ root = "Tests" weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, @@ -893,6 +896,7 @@ lean_exe «my-package-tests» where weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, @@ -958,6 +962,7 @@ lean_exe «my-package-tests» where weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, @@ -993,6 +998,7 @@ lean_exe «my-package-tests» where weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, @@ -1098,6 +1104,7 @@ root = "Lint" weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, @@ -1163,6 +1170,7 @@ root = "Lint" weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, @@ -1198,6 +1206,7 @@ root = "Lint" weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, @@ -1264,6 +1273,7 @@ lean_exe «my-package-lint» where weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, @@ -1329,6 +1339,7 @@ lean_exe «my-package-lint» where weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, @@ -1364,6 +1375,7 @@ lean_exe «my-package-lint» where weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, diff --git a/reference-manual/Manual/BuildTools/Lake/Config.lean b/reference-manual/Manual/BuildTools/Lake/Config.lean index 62b3289c9..376c8a592 100644 --- a/reference-manual/Manual/BuildTools/Lake/Config.lean +++ b/reference-manual/Manual/BuildTools/Lake/Config.lean @@ -158,6 +158,7 @@ name = "example-package" weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, @@ -250,6 +251,7 @@ name = "Sorting" weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, @@ -315,6 +317,7 @@ name = "Sorting" weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, @@ -326,6 +329,7 @@ name = "Sorting" libPrefixOnWindows := false, needs := #[], extraDepTargets := #[], + precompileLibrary := false, precompileModules := false, defaultFacets := #[`lean_lib.leanArts], nativeFacets := #, @@ -354,6 +358,7 @@ name = "Sorting" weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, @@ -365,6 +370,7 @@ name = "Sorting" libPrefixOnWindows := false, needs := #[], extraDepTargets := #[], + precompileLibrary := false, precompileModules := false, defaultFacets := #[`lean_lib.leanArts], nativeFacets := #, @@ -589,6 +595,7 @@ name = "TacticTools" weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, @@ -600,6 +607,7 @@ name = "TacticTools" libPrefixOnWindows := false, needs := #[], extraDepTargets := #[], + precompileLibrary := false, precompileModules := false, defaultFacets := #[`lean_lib.leanArts], nativeFacets := #, @@ -634,6 +642,7 @@ precompileModules = true weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, @@ -645,6 +654,7 @@ precompileModules = true libPrefixOnWindows := false, needs := #[], extraDepTargets := #[], + precompileLibrary := false, precompileModules := true, defaultFacets := #[`lean_lib.leanArts], nativeFacets := #, @@ -687,6 +697,7 @@ name = "trustworthytool" weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false, @@ -737,6 +748,7 @@ exeName = "tt" weakLinkArgs := #[], backend := Lake.Backend.default, platformIndependent := none, + precompileImports := false, dynlibs := #[], plugins := #[], requiresModuleSystem := false,