diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index 409865379d..97d32f32c1 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/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 diff --git a/src/lake/Lake/Config/LeanLib.lean b/src/lake/Lake/Config/LeanLib.lean index 50ce05782a..2c63c34ef0 100644 --- a/src/lake/Lake/Config/LeanLib.lean +++ b/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). diff --git a/src/lake/Lake/Config/LeanLibConfig.lean b/src/lake/Lake/Config/LeanLibConfig.lean index 5e09007439..ea29b63504 100644 --- a/src/lake/Lake/Config/LeanLibConfig.lean +++ b/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 diff --git a/src/lake/Lake/Config/Module.lean b/src/lake/Lake/Config/Module.lean index 0ce94e4940..377b2a02ba 100644 --- a/src/lake/Lake/Config/Module.lean +++ b/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 diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index d8d3083cfe..90df724905 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/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 diff --git a/src/lake/Lake/Config/PackageConfig.lean b/src/lake/Lake/Config/PackageConfig.lean index cbaaa8e627..6cd073d74a 100644 --- a/src/lake/Lake/Config/PackageConfig.lean +++ b/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. -/ diff --git a/src/lake/schemas/lakefile-toml-schema.json b/src/lake/schemas/lakefile-toml-schema.json index 67e697c5aa..09f40a55d5 100644 --- a/src/lake/schemas/lakefile-toml-schema.json +++ b/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." diff --git a/tests/lake/tests/module/ErrorTest/CrossPackageImportAll.lean b/tests/lake/tests/module/ErrorTest/CrossPackageImportAll.lean index d8e81ae1b9..837718d81b 100644 --- a/tests/lake/tests/module/ErrorTest/CrossPackageImportAll.lean +++ b/tests/lake/tests/module/ErrorTest/CrossPackageImportAll.lean @@ -1,2 +1,3 @@ module -import all Dep.Module + +import all Dep.NoImportAll diff --git a/tests/lake/tests/module/Test/CrossPackageImportAll.lean b/tests/lake/tests/module/Test/CrossPackageImportAll.lean new file mode 100644 index 0000000000..7274aa6e49 --- /dev/null +++ b/tests/lake/tests/module/Test/CrossPackageImportAll.lean @@ -0,0 +1,3 @@ +module + +import all Dep.AllowImportAll diff --git a/tests/lake/tests/module/dep/Dep/Module.lean b/tests/lake/tests/module/dep/Dep/AllowImportAll.lean similarity index 100% rename from tests/lake/tests/module/dep/Dep/Module.lean rename to tests/lake/tests/module/dep/Dep/AllowImportAll.lean diff --git a/tests/lake/tests/module/dep/Dep/NoImportAll.lean b/tests/lake/tests/module/dep/Dep/NoImportAll.lean new file mode 100644 index 0000000000..0cca093d7a --- /dev/null +++ b/tests/lake/tests/module/dep/Dep/NoImportAll.lean @@ -0,0 +1 @@ +module diff --git a/tests/lake/tests/module/dep/lakefile.toml b/tests/lake/tests/module/dep/lakefile.toml index 9bc8df4539..455e6d8076 100644 --- a/tests/lake/tests/module/dep/lakefile.toml +++ b/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 diff --git a/tests/lake/tests/module/test.sh b/tests/lake/tests/module/test.sh index 85da9c75de..1b1c0fab14 100755 --- a/tests/lake/tests/module/test.sh +++ b/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