fix: lake: import all transitivity & related bugs (#9525)
This PR fixes Lake's handling of a module system `import all`. Previously, Lake treated `import all` the same a non-module `import`, importing all private data in the transitive import tree. Lake now distinguishes the two, with `import all M` just importing the private data of `M`. The direct private imports of `M` are followed, but they are not promoted. This also fixes some other Lake bugs with module system imports that were discovered in the process.
This commit is contained in:
Mac Malone
GitHub
parent
820c1e6f15
commit
4875c6447f
10 changed files with 173 additions and 90 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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`. -/
|
||||
|
|
|
|||
3
src/lake/tests/module/Test/ModuleAllTransImportAll.lean
Normal file
3
src/lake/tests/module/Test/ModuleAllTransImportAll.lean
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
module
|
||||
|
||||
import all Test.ModuleImportAll
|
||||
3
src/lake/tests/module/Test/ModuleAllTransMetaImport.lean
Normal file
3
src/lake/tests/module/Test/ModuleAllTransMetaImport.lean
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
module
|
||||
|
||||
import all Test.ModulePrivateMetaImport
|
||||
|
|
@ -0,0 +1,3 @@
|
|||
module
|
||||
|
||||
import all Test.ModulePrivateImport
|
||||
|
|
@ -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
|
||||
|
|
|
|||
4
src/lake/tests/module/Test/ModulePromoteTransImport.lean
Normal file
4
src/lake/tests/module/Test/ModulePromoteTransImport.lean
Normal file
|
|
@ -0,0 +1,4 @@
|
|||
module
|
||||
|
||||
import all Test.ModuleImport
|
||||
import all Test.ModuleImportAll
|
||||
3
src/lake/tests/module/Test/ModuleTransImportAll.lean
Normal file
3
src/lake/tests/module/Test/ModuleTransImportAll.lean
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
module
|
||||
|
||||
import Test.ModuleImportAll
|
||||
|
|
@ -1,3 +0,0 @@
|
|||
module
|
||||
|
||||
import Test.ModulePromoteImport
|
||||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue