feat: lake: allowImportAll configuration option (#9855)

This PR adds a new `allowImportAll` configuration option for packages
and libraries. When enabled by an upstream package or library,
downstream packages will be able to `import all` modules of that package
or library. This enables package authors to selectively choose which
`private` elements, if any, downstream packages may have access to.

src/lake/Lake/Build/Module.lean

@@ -365,7 +365,7 @@ private def fetchImportInfo
       return .error
     let some mod ← findModule? imp.module
       | return s
-    if imp.importAll && pkgName != mod.pkg.name then
+    if imp.importAll && !mod.allowImportAll && pkgName != mod.pkg.name then
       logError s!"{fileName}: cannot 'import all' across packages"
       return .error
     let importJob ← mod.exportInfo.fetch

src/lake/Lake/Config/LeanLib.lean

@@ -141,6 +141,13 @@ then the default (which is C for now).
 @[inline] public def backend (self : LeanLib) : Backend :=
   Backend.orPreferLeft self.config.backend self.pkg.backend
 
+/--
+Whether downstream packages can `import all` modules of this library.
+Enabled if either the library or the package enables it.
+-/
+@[inline] public def allowImportAll (self : LeanLib) : Bool :=
+  self.config.allowImportAll || self.pkg.allowImportAll
+
 /--
 The dynamic libraries to load for modules of this library.
 The targets of the package plus the targets of the library (in that order).

src/lake/Lake/Config/LeanLibConfig.lean

@@ -99,6 +99,18 @@ public configuration LeanLibConfig (name : Name) extends LeanConfig where
   nativeFacets (shouldExport : Bool) : Array (ModuleFacet FilePath) :=
     #[if shouldExport then Module.oExportFacet else Module.oFacet]
 
+  /--
+  Whether downstream packages can `import all` modules of this library.
+
+  If enabled, downstream users will be able to access the `private` internals of modules,
+  including definition bodies not marked as `@[expose]`.
+  This may also, in the future, prevent compiler optimization which rely on `private`
+  definitions being inaccessible outside their own package.
+
+  Defaults to `false`.
+  -/
+  allowImportAll : Bool := false
+
 deriving Inhabited
 
 namespace LeanLibConfig

src/lake/Lake/Config/Module.lean

@@ -165,6 +165,9 @@ public def dynlibSuffix := "-1"
 @[inline] public def backend (self : Module) : Backend :=
   self.lib.backend
 
+@[inline] public def allowImportAll (self : Module) : Bool :=
+  self.lib.allowImportAll
+
 @[inline] public def dynlibs (self : Module) : TargetArray Dynlib :=
   self.lib.dynlibs
 

src/lake/Lake/Config/Package.lean

@@ -253,6 +253,10 @@ namespace Package
 @[inline] public def backend (self : Package) : Backend :=
   self.config.backend
 
+/-- The package's `allowImportAll` configuration. -/
+@[inline] public def allowImportAll (self : Package) : Bool :=
+  self.config.allowImportAll
+
 /-- The package's `dynlibs` configuration. -/
 @[inline] public def dynlibs (self : Package) : TargetArray Dynlib :=
   self.config.dynlibs

src/lake/Lake/Config/PackageConfig.lean

@@ -294,6 +294,7 @@ public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig
   the `LAKE_ARTIFACT_CACHE` environment variable is set to true.
   -/
   enableArtifactCache?, enableArtifactCache : Option Bool := none
+
   /--
   Whether, when the local artifact cache is enabled, Lake should copy all cached
   artifacts into the build directory. This ensures the build results are available
@@ -302,6 +303,7 @@ public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig
   Defaults to `false`.
   -/
   restoreAllArtifacts : Bool := false
+
   /--
   Whether native libraries (of this package) should be prefixed with `lib` on Windows.
 
@@ -312,6 +314,19 @@ public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig
   Defaults to `false`.
   -/
   libPrefixOnWindows : Bool := false
+
+  /--
+  Whether downstream packages can `import all` modules of this package.
+
+  If enabled, downstream users will be able to access the `private` internals of modules,
+  including definition bodies not marked as `@[expose]`.
+  This may also, in the future, prevent compiler optimization which rely on `private`
+  definitions being inaccessible outside their own package.
+
+  Defaults to `false`.
+  -/
+  allowImportAll : Bool := false
+
 deriving Inhabited
 
 /-- The package's name as specified by the author. -/

src/lake/schemas/lakefile-toml-schema.json

@@ -193,6 +193,11 @@
                             "default": false,
                             "description": "Whether static and shared binaries of this library should be prefixed with `lib` on Windows.\n\nUnlike Unix, Windows does not require native libraries to start with `lib` and, by convention, they usually do not. However, for consistent naming across all platforms, users may wish to enable this.\n\nDefaults to `false`."
                         },
+                        "allowImportAll": {
+                            "type": "boolean",
+                            "default": false,
+                            "description": "Whether downstream packages can `import all` modules of this library.\n\nIf enabled, downstream users will be able to access the `private` internals of modules, including definition bodies not marked as `@[expose]`. This may also, in the future, prevent compiler optimization which rely on `private` definitions being inaccessible outside their own package."
+                        },
                         "needs": {
                             "type": "array",
                             "items": {
@@ -451,6 +456,11 @@
                     "default": false,
                     "description": "Whether native libraries (of this package) should be prefixed with `lib` on Windows.\n\nUnlike Unix, Windows does not require native libraries to start with `lib` and, by convention, they usually do not. However, for consistent naming across all platforms, users may wish to enable this."
                 },
+                "allowImportAll": {
+                    "type": "boolean",
+                    "default": false,
+                    "description": "Whether downstream packages can `import all` modules of this package.\n\nIf enabled, downstream users will be able to access the `private` internals of modules, including definition bodies not marked as `@[expose]`. This may also, in the future, prevent compiler optimization which rely on `private` definitions being inaccessible outside their own package."
+                },
                 "enableArtifactCache": {
                     "type": "boolean",
                     "description": "Whether to enables Lake's local, offline artifact cache for the package.\n\nArtifacts (i.e., build products) of packages will be shared across local copies by storing them in a cache associated with the Lean toolchain.\nThis can significantly reduce initial build times and disk space usage when working with multiple copies of large projects or large dependencies.\n\nAs a caveat, build targets which support the artifact cache will not be stored in their usual location within the build directory. Thus, projects with custom build scripts that rely on specific location of artifacts may wish to disable this feature.\n\nIf not set, the cache will be disabled by default unless the `LAKE_ARTIFACT_CACHE` environment variable is set to true."

tests/lake/tests/module/ErrorTest/CrossPackageImportAll.lean

@@ -1,2 +1,3 @@
 module
-import all Dep.Module
+
+import all Dep.NoImportAll

tests/lake/tests/module/Test/CrossPackageImportAll.lean

@@ -0,0 +1,3 @@
+module
+
+import all Dep.AllowImportAll

tests/lake/tests/module/dep/Dep/NoImportAll.lean

@@ -0,0 +1 @@
+module

tests/lake/tests/module/dep/lakefile.toml

@@ -1,5 +1,9 @@
 name = "dep"
+leanOptions.experimental.module = true
 
 [[lean_lib]]
-name = "Dep"
-leanOptions.experimental.module = true
+name = "Dep.NoImportAll"
+
+[[lean_lib]]
+name = "Dep.AllowImportAll"
+allowImportAll = true

tests/lake/tests/module/test.sh

@@ -19,8 +19,10 @@ module
 public def foo : String := "bar"
 EOF
 
-# Test cross-package `import all``
+# Test cross-package `import all` is prevented by default
 test_err "cannot 'import all' across packages" build ErrorTest.CrossPackageImportAll
+# Test cross-package `import all` is allowed when `allowImportAll = true` is set
+test_run build Test.CrossPackageImportAll
 
 # Tests importing of a module's private segment
 # should not not be imported by a plain `import` in a module