feat: add requiresModuleSystem package option in Lake

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,6 +370,12 @@ def fetchImportInfo
       logError s!"{fileName}: module imports itself"
       return .error
     let mods ← findModules imp.module
+    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 \
+          `{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
@@ -421,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."
@@ -1232,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

src/lake/Lake/Config/Package.lean

@@ -294,6 +294,14 @@ 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 `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

src/lake/Lake/Config/PackageConfig.lean

@@ -321,6 +321,34 @@ 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.
+
+  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.
 

tests/lake/tests/requiresModule/Test/ModuleConsumer.lean

@@ -0,0 +1,3 @@
+module
+
+import Dep

tests/lake/tests/requiresModule/Test/NonModuleConsumer.lean

@@ -0,0 +1 @@
+import Dep

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

tests/lake/tests/requiresModule/dep/Dep.lean

@@ -0,0 +1,3 @@
+module
+
+public def Dep.greet : String := "hi"

tests/lake/tests/requiresModule/dep/lakefile.toml

@@ -0,0 +1,5 @@
+name = "dep"
+requiresModuleSystem = true
+
+[[lean_lib]]
+name = "Dep"

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"

tests/lake/tests/requiresModule/test.sh

@@ -0,0 +1,32 @@
+#!/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
+
+# 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*