diff --git a/src/lake/Lake/Build/Facets.lean b/src/lake/Lake/Build/Facets.lean index 08a57986d2..68533d93f1 100644 --- a/src/lake/Lake/Build/Facets.lean +++ b/src/lake/Lake/Build/Facets.lean @@ -67,13 +67,12 @@ structure ModuleImportInfo where trace : BuildTrace /-- Transitive import trace for an `import` of the module with the module system enabled. -/ transTrace : BuildTrace - /-- Transitive import trace for a `meta import` of the module with the module system enabled. -/ + /-- Transitive import trace for a `meta import` of the module. -/ metaTransTrace : BuildTrace - /-- - Transitive import trace for an `import all` of the module from a module with the module system - enabled or an `import` of the module from a module without it. - -/ + /-- Transitive import trace for an `import all` of the module. -/ allTransTrace : BuildTrace + /-- Transitive import trace for an `import` of the module without the module system enabled. -/ + legacyTransTrace : BuildTrace /-- **For internal use only.** Information about the imports of this module. -/ builtin_facet importInfo : Module => ModuleImportInfo @@ -95,13 +94,12 @@ structure ModuleExportInfo where allArtsTrace : BuildTrace /-- Transitive import trace for an `import` of the module with the module system enabled. -/ transTrace : BuildTrace - /-- Transitive import trace for a `meta import` of the module with the module system enabled. -/ + /-- Transitive import trace for a `meta import` of the module. -/ metaTransTrace : BuildTrace - /-- - Transitive import trace for an `import all` of the module from a module with the module system - enabled or an `import` of the module from a module without it. - -/ + /-- Transitive import trace for an `import all` of the module. -/ allTransTrace : BuildTrace + /-- Transitive import trace for an `import` of the module without the module system enabled. -/ + legacyTransTrace : BuildTrace /-- **For internal use only.** Information useful to importers of this module. -/ builtin_facet exportInfo : Module => ModuleExportInfo diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index 8d1de230be..b9741616c7 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/src/lake/Lake/Build/Module.lean @@ -217,15 +217,13 @@ private def computeModuleDeps return {dynlibs, plugins} private partial def fetchTransImportArts - (directImports : Array ModuleImport) (directArts : NameMap ImportArtifacts) (importAll : Bool) + (directImports : Array ModuleImport) (directArts : NameMap ImportArtifacts) (nonModule : Bool) : FetchM (NameMap ImportArtifacts) := do let q ← directImports.foldlM (init := #[]) fun q imp => do let some mod := imp.module? | return q let input ← (← mod.input.fetch).await - return input.imports.foldr (init := q) fun imp q => - if let some mod := imp.module? then - q.push (mod, imp.importAll || importAll) - else q + let importAll := strictOr nonModule imp.importAll + return enqueue importAll input q walk directArts q where walk s q := do @@ -241,25 +239,108 @@ where let arts := if importAll then info.allArts else info.arts let s := s.insert mod.name arts let input ← (← mod.input.fetch).await - let q := input.imports.foldr (init := q) fun imp q => - if let some mod := imp.module? then - q.push (mod, importAll) - else q + let q := enqueue importAll input q walk s q else return s + enqueue importAll input q := + input.imports.foldr (init := q) fun imp q => + if let some mod := imp.module? then + if importAll || imp.isExported then + q.push (mod, nonModule || (importAll && imp.importAll)) + else q + else q + +private def ModuleImportInfo.nil (modName : Name) : ModuleImportInfo where + directArts := {} + trace := .nil s!"imports" + transTrace := .nil s!"{modName} transitive imports (public)" + metaTransTrace := .nil s!"{modName} transitive imports (meta)" + allTransTrace := .nil s!"{modName} transitive imports (all)" + legacyTransTrace := .nil s!"{modName} transitive imports (legacy)" + +private def ModuleImportInfo.addImport + (info : ModuleImportInfo) (nonModule : Bool) + (mod : Module) (imp : Import) (expInfo : ModuleExportInfo) +: ModuleImportInfo := + let info := + if nonModule then + {info with + directArts := info.directArts.insert mod.name expInfo.allArts + trace := info.trace.mix expInfo.legacyTransTrace |>.mix expInfo.allArtsTrace.withoutInputs + } + else if imp.importAll then + {info with + directArts := info.directArts.insert mod.name expInfo.allArts + trace := info.trace.mix expInfo.allTransTrace |>.mix expInfo.allArtsTrace.withoutInputs + } + else + let info := + if !info.directArts.contains mod.name then -- do not demote `import all` + {info with directArts := info.directArts.insert mod.name expInfo.arts} + else + info + if imp.isMeta then + {info with trace := info.trace.mix expInfo.metaTransTrace |>.mix expInfo.metaArtsTrace.withoutInputs} + else + {info with trace := info.trace.mix expInfo.transTrace |>.mix expInfo.artsTrace.withoutInputs} + let info := {info with + legacyTransTrace := info.legacyTransTrace + |>.mix expInfo.legacyTransTrace + |>.mix expInfo.allArtsTrace.withoutInputs + |>.withoutInputs + } + let info := + if imp.importAll then + {info with + allTransTrace := info.allTransTrace + |>.mix expInfo.allTransTrace + |>.mix expInfo.allArtsTrace.withoutInputs + |>.withoutInputs + } + else if imp.isMeta then + {info with + allTransTrace := info.allTransTrace + |>.mix expInfo.metaTransTrace + |>.mix expInfo.metaArtsTrace.withoutInputs + |>.withoutInputs + } + else + {info with + allTransTrace := info.allTransTrace + |>.mix expInfo.transTrace + |>.mix expInfo.artsTrace.withoutInputs + |>.withoutInputs + } + if imp.isExported then + let info := {info with + metaTransTrace := info.metaTransTrace + |>.mix expInfo.metaTransTrace + |>.mix expInfo.metaArtsTrace.withoutInputs + |>.withoutInputs + } + if imp.isMeta then + {info with + transTrace := info.transTrace + |>.mix expInfo.metaTransTrace + |>.mix expInfo.metaArtsTrace.withoutInputs + |>.withoutInputs + } + else + {info with + transTrace := info.transTrace + |>.mix expInfo.transTrace + |>.mix expInfo.artsTrace.withoutInputs + |>.withoutInputs + } + else + info private def fetchImportInfo (fileName : String) (modName : Name) (header : ModuleHeader) : FetchM (Job ModuleImportInfo) := do - let notModule := !header.isModule - let info : ModuleImportInfo := { - directArts := {} - trace := .nil s!"imports" - transTrace := .nil s!"{modName} transitive imports", - metaTransTrace := .nil s!"{modName} transitive imports (meta)", - allTransTrace := .nil s!"{modName} transitive imports (all)" - } + let nonModule := !header.isModule + let info := ModuleImportInfo.nil modName let impArtsJob : Job ModuleImportInfo := .pure info header.imports.foldlM (init := impArtsJob) fun s imp => do if modName = imp.module then @@ -268,50 +349,7 @@ private def fetchImportInfo let some mod ← findModule? imp.module | return s let importJob ← mod.exportInfo.fetch - let importAll := strictOr imp.importAll notModule - return s.zipWith (other := importJob) fun info impInfo => - let info := - if importAll then - {info with - directArts := info.directArts.insert mod.name impInfo.allArts - trace := info.trace.mix impInfo.allTransTrace |>.mix impInfo.allArtsTrace.withoutInputs - } - else if !info.directArts.contains mod.name then -- do not demote `import all` - {info with - directArts := info.directArts.insert mod.name impInfo.arts - trace := info.trace.mix impInfo.transTrace |>.mix impInfo.artsTrace.withoutInputs - } - else - info - let info := {info with - allTransTrace := info.allTransTrace - |>.mix impInfo.allTransTrace - |>.mix impInfo.allArtsTrace.withoutInputs - |>.withoutInputs - } - if imp.isExported then - let info := {info with - metaTransTrace := info.transTrace - |>.mix impInfo.metaTransTrace - |>.mix impInfo.metaArtsTrace.withoutInputs - |>.withoutInputs - } - if imp.isMeta then - {info with - transTrace := info.transTrace - |>.mix impInfo.metaTransTrace - |>.mix impInfo.metaArtsTrace.withoutInputs - |>.withoutInputs - } - else - {info with - transTrace := info.transTrace - |>.mix impInfo.transTrace - |>.mix impInfo.artsTrace.withoutInputs - |>.withoutInputs - } - else - info + return s.zipWith (·.addImport nonModule mod imp ·) importJob /-- The `ModuleFacetConfig` for the builtin `importInfoFacet`. -/ def Module.importInfoFacetConfig : ModuleFacetConfig importInfoFacet := @@ -354,6 +392,7 @@ def Module.computeExportInfo (mod : Module) : FetchM (Job ModuleExportInfo) := d transTrace := importInfo.transTrace metaTransTrace := importInfo.metaTransTrace allTransTrace := importInfo.allTransTrace + legacyTransTrace := importInfo.legacyTransTrace } else return { @@ -365,6 +404,7 @@ def Module.computeExportInfo (mod : Module) : FetchM (Job ModuleExportInfo) := d transTrace := importInfo.transTrace metaTransTrace := importInfo.metaTransTrace allTransTrace := importInfo.allTransTrace + legacyTransTrace := importInfo.legacyTransTrace } /-- The `ModuleFacetConfig` for the builtin `exportInfoFacet`. -/ diff --git a/src/lake/tests/module/Test/ModuleAllTransImportAll.lean b/src/lake/tests/module/Test/ModuleAllTransImportAll.lean new file mode 100644 index 0000000000..2a17166128 --- /dev/null +++ b/src/lake/tests/module/Test/ModuleAllTransImportAll.lean @@ -0,0 +1,3 @@ +module + +import all Test.ModuleImportAll diff --git a/src/lake/tests/module/Test/ModuleAllTransMetaImport.lean b/src/lake/tests/module/Test/ModuleAllTransMetaImport.lean new file mode 100644 index 0000000000..df47c90762 --- /dev/null +++ b/src/lake/tests/module/Test/ModuleAllTransMetaImport.lean @@ -0,0 +1,3 @@ +module + +import all Test.ModulePrivateMetaImport diff --git a/src/lake/tests/module/Test/ModuleAllTransPrivateImport.lean b/src/lake/tests/module/Test/ModuleAllTransPrivateImport.lean new file mode 100644 index 0000000000..4531a1ab4c --- /dev/null +++ b/src/lake/tests/module/Test/ModuleAllTransPrivateImport.lean @@ -0,0 +1,3 @@ +module + +import all Test.ModulePrivateImport diff --git a/src/lake/tests/module/Test/ModulePromoteImport.lean b/src/lake/tests/module/Test/ModulePromoteImport.lean index a6b827909b..3a7ff97928 100644 --- a/src/lake/tests/module/Test/ModulePromoteImport.lean +++ b/src/lake/tests/module/Test/ModulePromoteImport.lean @@ -1,5 +1,5 @@ module -import Test.ModuleImport +public import Test.Generated.Module import all Test.Generated.Module -public import Test.Generated.Module -- no demotion +public import Test.Generated.Module diff --git a/src/lake/tests/module/Test/ModulePromoteTransImport.lean b/src/lake/tests/module/Test/ModulePromoteTransImport.lean new file mode 100644 index 0000000000..9690dd4f9e --- /dev/null +++ b/src/lake/tests/module/Test/ModulePromoteTransImport.lean @@ -0,0 +1,4 @@ +module + +import all Test.ModuleImport +import all Test.ModuleImportAll diff --git a/src/lake/tests/module/Test/ModuleTransImportAll.lean b/src/lake/tests/module/Test/ModuleTransImportAll.lean new file mode 100644 index 0000000000..e87e504f22 --- /dev/null +++ b/src/lake/tests/module/Test/ModuleTransImportAll.lean @@ -0,0 +1,3 @@ +module + +import Test.ModuleImportAll diff --git a/src/lake/tests/module/Test/ModuleTransPromoteImport.lean b/src/lake/tests/module/Test/ModuleTransPromoteImport.lean deleted file mode 100644 index 3387d27485..0000000000 --- a/src/lake/tests/module/Test/ModuleTransPromoteImport.lean +++ /dev/null @@ -1,3 +0,0 @@ -module - -import Test.ModulePromoteImport diff --git a/src/lake/tests/module/test.sh b/src/lake/tests/module/test.sh index a6bfac4eca..a906e7a4de 100755 --- a/src/lake/tests/module/test.sh +++ b/src/lake/tests/module/test.sh @@ -21,19 +21,30 @@ EOF # should not not be imported by a plain `import` in a module test_run build Test.ModuleImport test_cmd_fails grep -F "Test/Generated/Module.olean.private" .lake/build/ir/Test/ModuleImport.setup.json +test_run build Test.ModulePrivateImport +test_cmd_fails grep -F "Test/Generated/Module.olean.private" .lake/build/ir/Test/ModulePrivateImport.setup.json # should be imported by an `import all` in a module test_run build Test.ModuleImportAll test_cmd grep -F "Test/Generated/Module.olean.private" .lake/build/ir/Test/ModuleImportAll.setup.json # including promoted imports test_run build Test.ModulePromoteImport test_cmd grep -F "Test/Generated/Module.olean.private" .lake/build/ir/Test/ModulePromoteImport.setup.json -test_run build Test.ModuleTransPromoteImport -test_cmd grep -F "Test/Generated/Module.olean.private" .lake/build/ir/Test/ModuleTransPromoteImport.setup.json +test_run build Test.ModulePromoteTransImport +test_cmd grep -F "Test/Generated/Module.olean.private" .lake/build/ir/Test/ModulePromoteTransImport.setup.json # should be imported by a non-module test_run build Test.NonModuleImport test_cmd grep -F "Test/Generated/Module.olean.private" .lake/build/ir/Test/NonModuleImport.setup.json +# should not be imported by a module transitive import of a private `import all` +test_run build Test.ModuleTransImportAll +test_cmd_fails grep -F "Test/Generated/Module.olean.private" .lake/build/ir/Test/ModuleTransImportAll.setup.json +test_run build Test.ModuleAllTransPrivateImport +test_cmd_fails grep -F "Test/Generated/Module.olean.private" .lake/build/ir/Test/ModuleAllTransPrivateImport.setup.json -# Build all tests before making edits +# Tests that the transitive module import of a private import does not include its artifacts +test_run build Test.ModuleTransPrivateImport +test_cmd_fails grep -F "Test/Generated/Module.olean" .lake/build/ir/Test/ModuleTransPrivateImport.setup.json + +# Build all tests before making an edit test_run build # Tests a public edit of an import @@ -43,18 +54,23 @@ old_hash=$(cat .lake/build/lib/lean/Test/Generated/Module.olean.hash) test_out "Built Test.Generated.Module" build Test.Generated.Module -v new_hash=$(cat .lake/build/lib/lean/Test/Generated/Module.olean.hash) test_exp $old_hash != $new_hash -# should trigger a rebuild on a plain `import` in a module +# should trigger a rebuild on a module direct `import` test_out "Built Test.ModuleImport" build Test.ModuleImport -v test_out "Built Test.ModulePrivateImport" build Test.ModulePrivateImport -v -# should not trigger a rebuild on a transitive private `import` in a module -test_run build Test.ModuleTransPrivateImport --no-build -# should trigger a rebuild on an `import all` in a module +# should trigger a rebuild on a direct `import all` test_out "Built Test.ModuleImportAll" build Test.ModuleImportAll -v # should trigger a rebuild for a non-module direct import test_out "Built Test.NonModuleImport" build Test.NonModuleImport -v +# should not trigger a rebuild on a module transitive private `import` +test_run build Test.ModuleTransPrivateImport --no-build +# should trigger a rebuild on an `import all` of a transitive private `import` +test_out "Built Test.ModuleAllTransPrivateImport" build Test.ModuleAllTransPrivateImport -v # should trigger a rebuild for a non-module transitive import test_out "Built Test.NonModuleTransImport" build Test.NonModuleTransImport -v +# Build all tests before making an edit +test_run build + # Tests a private edit of an import echo "# TEST: private edit" test_cmd sed_i 's/bar/baz/' Test/Generated/Module.lean @@ -65,16 +81,25 @@ new_pub_hash=$(cat .lake/build/lib/lean/Test/Generated/Module.olean.hash) new_hash=$(cat .lake/build/lib/lean/Test/Generated/Module.olean.private.hash) test_exp $old_pub_hash == $new_pub_hash test_exp $old_hash != $new_hash -# should not trigger a rebuild on a plain `import` in a module +# should not trigger a rebuild on a module direct `import` test_run build Test.ModuleImport --no-build -# should trigger a rebuild on an `import all` in a module +test_run build Test.ModulePrivateImport --no-build +# should trigger a rebuild on a direct `import all` test_out "Built Test.ModuleImportAll" build Test.ModuleImportAll -v test_out "Built Test.ModulePromoteImport" build Test.ModulePromoteImport -v # should trigger a rebuild for a non-module direct import test_out "Built Test.NonModuleImport" build Test.NonModuleImport -v +# should not trigger a rebuild on an `import all` of a transitive private `import` +test_run build Test.ModuleAllTransPrivateImport --no-build +# should trigger a rebuild on an `import all` of a transitive private `import all` +test_out "Built Test.ModuleAllTransImportAll" build Test.ModuleAllTransImportAll -v +test_out "Built Test.ModulePromoteTransImport" build Test.ModulePromoteTransImport -v # should trigger a rebuild for a non-module transitive import test_out "Built Test.NonModuleTransImport" build Test.NonModuleTransImport -v +# Build all tests before making an edit +test_run build + # Tests a server edit of an import echo "# TEST: server edit" test_cmd sed_i '/-- insert here/{G;}' Test/Generated/Module.lean @@ -82,15 +107,18 @@ old_hash=$(cat .lake/build/lib/lean/Test/Generated/Module.olean.server.hash) test_out "Built Test.Generated.Module" build Test.Generated.Module -v new_hash=$(cat .lake/build/lib/lean/Test/Generated/Module.olean.server.hash) test_exp $old_hash != $new_hash -# should not trigger a rebuild on a plain `import` in a module +# should not trigger a rebuild on a direct module `import` test_run build Test.ModuleImport --no-build -# should trigger a rebuild on an `import all` in a module +# should trigger a rebuild on a direct `import all` test_out "Built Test.ModuleImportAll" build Test.ModuleImportAll -v # should trigger a rebuild for a non-module direct import test_out "Built Test.NonModuleImport" build Test.NonModuleImport -v # should trigger a rebuild for a non-module transitive import test_out "Built Test.NonModuleTransImport" build Test.NonModuleTransImport -v +# Build all tests before making an edit +test_run build + # Tests a meta edit of an import echo "# TEST: meta edit" test_cmd sed_i 's/baz/ipsum/' Test/Generated/Module.lean @@ -101,9 +129,9 @@ new_pub_hash=$(cat .lake/build/lib/lean/Test/Generated/Module.olean.hash) new_hash=$(cat .lake/build/lib/lean/Test/Generated/Module.ir.hash) test_exp $old_pub_hash == $new_pub_hash test_exp $old_hash != $new_hash -# should not trigger a rebuild on a plain `import` in a module +# should not trigger a rebuild on a direct module `import` test_run build Test.ModuleImport --no-build -# should trigger a rebuild on a `meta import` +# should trigger a rebuild on a direct `meta import` test_out "Built Test.ModuleMetaImport" build Test.ModuleMetaImport -v test_out "Built Test.ModulePrivateMetaImport" build Test.ModulePrivateMetaImport -v # should trigger a rebuild on a transitive `meta import` @@ -112,8 +140,12 @@ test_out "Built Test.ModuleMetaTransImport" build Test.ModuleMetaTransImport -v test_out "Built Test.ModuleTransMetaImport" build Test.ModuleTransMetaImport -v # should not trigger a rebuild on module transitive import of a private `meta import` test_run build Test.ModuleTransPrivateMetaImport --no-build -# should trigger a rebuild on an `import all` +# should trigger a rebuild on a direct `import all` test_out "Built Test.ModuleImportAll" build Test.ModuleImportAll -v +# should not trigger a rebuild on an `import all` of a transitive private `import` +test_run build Test.ModuleAllTransPrivateImport --no-build +# should trigger a rebuild on a `import all` of a `meta import` +test_out "Built Test.ModuleAllTransMetaImport" build Test.ModuleAllTransMetaImport -v # should trigger a rebuild for a non-module direct import test_out "Built Test.NonModuleImport" build Test.NonModuleImport -v # should trigger a rebuild for a non-module transitive import