From bec0918b3618ad8379bc02bed049f27273b7c8d4 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 5 May 2026 12:05:21 +0000 Subject: [PATCH 1/2] feat: add `requiresModuleSystem` package option in Lake This PR adds a new package configuration option `requiresModuleSystem`. When a package sets it to `true`, Lake emits a warning whenever a module from another package imports any of its modules without itself using the module system (i.e., without a `module` header). This lets package authors signal that their API is designed for the visibility and elaboration semantics of the module system. The check lives in `fetchImportInfo` and runs once per import after resolving the providing module(s); the disambiguation case (multiple packages providing the same module name) warns if any provider has the flag set. --- src/lake/Lake/Build/Module.lean | 6 +++++ src/lake/Lake/Config/Package.lean | 4 +++ src/lake/Lake/Config/PackageConfig.lean | 13 ++++++++++ .../requiresModule/Test/ModuleConsumer.lean | 3 +++ .../Test/NonModuleConsumer.lean | 1 + tests/lake/tests/requiresModule/clean.sh | 3 +++ tests/lake/tests/requiresModule/dep/Dep.lean | 3 +++ .../tests/requiresModule/dep/lakefile.toml | 5 ++++ tests/lake/tests/requiresModule/lakefile.toml | 10 ++++++++ tests/lake/tests/requiresModule/test.sh | 25 +++++++++++++++++++ 10 files changed, 73 insertions(+) create mode 100644 tests/lake/tests/requiresModule/Test/ModuleConsumer.lean create mode 100644 tests/lake/tests/requiresModule/Test/NonModuleConsumer.lean create mode 100755 tests/lake/tests/requiresModule/clean.sh create mode 100644 tests/lake/tests/requiresModule/dep/Dep.lean create mode 100644 tests/lake/tests/requiresModule/dep/lakefile.toml create mode 100644 tests/lake/tests/requiresModule/lakefile.toml create mode 100755 tests/lake/tests/requiresModule/test.sh diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index 83ac5af6da22..7cff46a4fd6d 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/src/lake/Lake/Build/Module.lean @@ -369,6 +369,12 @@ def fetchImportInfo logError s!"{fileName}: module imports itself" return .error let mods ← findModules imp.module + if nonModule then + if let some mod := mods.find? fun mod => + mod.pkg.requiresModuleSystem && pkgName != mod.pkg.keyName then + logWarning s!"{fileName}: imports `{imp.module}` from package \ + `{mod.pkg.prettyName}`, which is designed for use with the module \ + system; consider adding `module` to the start of this file" let n := mods.size if h : n = 0 then return s diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index 03f66b9b72d4..4f6ab2ab5cfc 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/src/lake/Lake/Config/Package.lean @@ -294,6 +294,10 @@ public def id? (self : Package) : Option PkgId := @[inline] public def allowImportAll (self : Package) : Bool := self.config.allowImportAll +/-- The package's `requiresModuleSystem` configuration. -/ +@[inline] public def requiresModuleSystem (self : Package) : Bool := + self.config.requiresModuleSystem + /-- The package's `dynlibs` configuration. -/ @[inline] public def dynlibs (self : Package) : TargetArray Dynlib := self.config.dynlibs diff --git a/src/lake/Lake/Config/PackageConfig.lean b/src/lake/Lake/Config/PackageConfig.lean index 22b08dea9b0a..0ed2187d9bb1 100644 --- a/src/lake/Lake/Config/PackageConfig.lean +++ b/src/lake/Lake/Config/PackageConfig.lean @@ -321,6 +321,19 @@ public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig -/ allowImportAll : Bool := false + /-- + Whether this package is designed for use with the module system. + + If enabled, Lake emits a warning whenever a module from another package + imports a module of this package without itself using the module system + (i.e., without a `module` header). This signals to downstream users that + the package's API expects the visibility and elaboration semantics of the + module system. + + Defaults to `false`. + -/ + requiresModuleSystem : Bool := false + /-- Whether to run Lake's built-in linter on the package. diff --git a/tests/lake/tests/requiresModule/Test/ModuleConsumer.lean b/tests/lake/tests/requiresModule/Test/ModuleConsumer.lean new file mode 100644 index 000000000000..ac338f16ca73 --- /dev/null +++ b/tests/lake/tests/requiresModule/Test/ModuleConsumer.lean @@ -0,0 +1,3 @@ +module + +import Dep diff --git a/tests/lake/tests/requiresModule/Test/NonModuleConsumer.lean b/tests/lake/tests/requiresModule/Test/NonModuleConsumer.lean new file mode 100644 index 000000000000..f341d235af05 --- /dev/null +++ b/tests/lake/tests/requiresModule/Test/NonModuleConsumer.lean @@ -0,0 +1 @@ +import Dep diff --git a/tests/lake/tests/requiresModule/clean.sh b/tests/lake/tests/requiresModule/clean.sh new file mode 100755 index 000000000000..b81d677c37ca --- /dev/null +++ b/tests/lake/tests/requiresModule/clean.sh @@ -0,0 +1,3 @@ +rm -f produced* +rm -rf dep/.lake dep/lake-manifest.json +rm -rf .lake lake-manifest.json diff --git a/tests/lake/tests/requiresModule/dep/Dep.lean b/tests/lake/tests/requiresModule/dep/Dep.lean new file mode 100644 index 000000000000..bb95e594e436 --- /dev/null +++ b/tests/lake/tests/requiresModule/dep/Dep.lean @@ -0,0 +1,3 @@ +module + +public def Dep.greet : String := "hi" diff --git a/tests/lake/tests/requiresModule/dep/lakefile.toml b/tests/lake/tests/requiresModule/dep/lakefile.toml new file mode 100644 index 000000000000..579044da8e13 --- /dev/null +++ b/tests/lake/tests/requiresModule/dep/lakefile.toml @@ -0,0 +1,5 @@ +name = "dep" +requiresModuleSystem = true + +[[lean_lib]] +name = "Dep" diff --git a/tests/lake/tests/requiresModule/lakefile.toml b/tests/lake/tests/requiresModule/lakefile.toml new file mode 100644 index 000000000000..18ad5103cf9a --- /dev/null +++ b/tests/lake/tests/requiresModule/lakefile.toml @@ -0,0 +1,10 @@ +name = "test" +defaultTargets = ["Test"] + +[[lean_lib]] +name = "Test" +globs = "Test.+" + +[[require]] +name = "dep" +path = "dep" diff --git a/tests/lake/tests/requiresModule/test.sh b/tests/lake/tests/requiresModule/test.sh new file mode 100755 index 000000000000..52f20933c921 --- /dev/null +++ b/tests/lake/tests/requiresModule/test.sh @@ -0,0 +1,25 @@ +#!/usr/bin/env bash +source ../common.sh + +./clean.sh + +# --- +# Tests the package-level `requiresModuleSystem` flag. +# A package that sets `requiresModuleSystem = true` should cause Lake +# to warn whenever a downstream module imports it without a `module` header. +# --- + +# Warm up: create the manifest and resolve dependencies so subsequent +# invocations don't emit setup messages that would confuse the warning checks. +test_run resolve-deps + +# A consumer that uses the module system: should build without emitting our warning. +test_not_out "designed for use with the module system" build Test.ModuleConsumer + +# A non-module consumer: should build successfully but emit the warning, +# naming both the importing file and the imported package. +test_out "Test/NonModuleConsumer.lean: imports \`Dep\` from package \`dep\`, which is designed for use with the module system" \ + build Test.NonModuleConsumer + +# Cleanup +rm -f produced* From c374b3fbe80ee30f6f36593b665adf3641a1bc86 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 6 May 2026 09:53:57 +0000 Subject: [PATCH 2/2] feat: add `silenceRequiresModuleSystemWarning` package option in Lake This PR adds a companion configuration option `silenceRequiresModuleSystemWarning` that lets a package opt out of the warning emitted by Lake when it imports modules from a `requiresModuleSystem` dependency without using the module system. This is intended for packages that have knowingly decided not to migrate to the module system yet. The flag is honored by `fetchImportInfo` via a new `silenceWarning` parameter threaded from the importing module's package configuration. --- src/lake/Lake/Build/Module.lean | 5 ++++- src/lake/Lake/Config/Package.lean | 4 ++++ src/lake/Lake/Config/PackageConfig.lean | 15 +++++++++++++++ tests/lake/tests/requiresModule/test.sh | 9 ++++++++- 4 files changed, 31 insertions(+), 2 deletions(-) diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index 7cff46a4fd6d..0e97abb42da1 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/src/lake/Lake/Build/Module.lean @@ -360,6 +360,7 @@ def Package.discriminant (self : Package) := set_option linter.unusedVariables.funArgs false in def fetchImportInfo (fileName : String) (pkgName modName : Name) (header : ModuleHeader) + (silenceWarning : Bool := false) : FetchM (Job ModuleImportInfo) := do let nonModule := !header.isModule let info := ModuleImportInfo.nil modName @@ -369,7 +370,7 @@ def fetchImportInfo logError s!"{fileName}: module imports itself" return .error let mods ← findModules imp.module - if nonModule then + if nonModule && !silenceWarning then if let some mod := mods.find? fun mod => mod.pkg.requiresModuleSystem && pkgName != mod.pkg.keyName then logWarning s!"{fileName}: imports `{imp.module}` from package \ @@ -427,6 +428,7 @@ public def Module.importInfoFacetConfig : ModuleFacetConfig importInfoFacet := mkFacetJobConfig fun mod => do let header ← (← mod.header.fetch).await fetchImportInfo mod.relLeanFile.toString mod.pkg.keyName mod.name header + (silenceWarning := mod.pkg.silenceRequiresModuleSystemWarning) def noServerOLeanError := "No server olean generated. Ensure the module system is enabled." @@ -1238,6 +1240,7 @@ def setupEditedModule let fileName := mod.relLeanFile.toString let localImports := directImports.filterMap (·.module?) let impInfoJob ← fetchImportInfo fileName mod.pkg.keyName mod.name header + (silenceWarning := mod.pkg.silenceRequiresModuleSystemWarning) let precompileImports ← if mod.shouldPrecompile then (← computeTransImportsAux fileName localImports).await diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index 4f6ab2ab5cfc..6d515fd3bd5c 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/src/lake/Lake/Config/Package.lean @@ -298,6 +298,10 @@ public def id? (self : Package) : Option PkgId := @[inline] public def requiresModuleSystem (self : Package) : Bool := self.config.requiresModuleSystem +/-- The package's `silenceRequiresModuleSystemWarning` configuration. -/ +@[inline] public def silenceRequiresModuleSystemWarning (self : Package) : Bool := + self.config.silenceRequiresModuleSystemWarning + /-- The package's `dynlibs` configuration. -/ @[inline] public def dynlibs (self : Package) : TargetArray Dynlib := self.config.dynlibs diff --git a/src/lake/Lake/Config/PackageConfig.lean b/src/lake/Lake/Config/PackageConfig.lean index 0ed2187d9bb1..8f648d73ef59 100644 --- a/src/lake/Lake/Config/PackageConfig.lean +++ b/src/lake/Lake/Config/PackageConfig.lean @@ -330,10 +330,25 @@ public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig the package's API expects the visibility and elaboration semantics of the module system. + Downstream packages can opt out of the warning by setting + `silenceRequiresModuleSystemWarning := true` on their own package. + Defaults to `false`. -/ requiresModuleSystem : Bool := false + /-- + Whether to silence the warnings produced when this package imports modules + from a dependency that has set `requiresModuleSystem` while not using the + module system itself. + + Use this to opt out of the migration nudge after deciding the package is + knowingly going to keep importing such dependencies without `module`. + + Defaults to `false`. + -/ + silenceRequiresModuleSystemWarning : Bool := false + /-- Whether to run Lake's built-in linter on the package. diff --git a/tests/lake/tests/requiresModule/test.sh b/tests/lake/tests/requiresModule/test.sh index 52f20933c921..259ff65b0b81 100755 --- a/tests/lake/tests/requiresModule/test.sh +++ b/tests/lake/tests/requiresModule/test.sh @@ -21,5 +21,12 @@ test_not_out "designed for use with the module system" build Test.ModuleConsumer test_out "Test/NonModuleConsumer.lean: imports \`Dep\` from package \`dep\`, which is designed for use with the module system" \ build Test.NonModuleConsumer -# Cleanup +# Opt out of the warning by setting `silenceRequiresModuleSystemWarning` on the +# importing package. After a clean rebuild, the warning must not appear. +sed_i '1a silenceRequiresModuleSystemWarning = true' lakefile.toml +test_run clean +test_not_out "designed for use with the module system" build Test.NonModuleConsumer + +# Restore the lakefile and clean up. +sed_i '/^silenceRequiresModuleSystemWarning = true$/d' lakefile.toml rm -f produced*