diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index a2e79f3a45..922b163e72 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/src/lake/Lake/Build/Module.lean @@ -327,13 +327,13 @@ private def ModuleImportInfo.addImport |>.mix expInfo.artsTrace.withoutInputs |>.withoutInputs } + let info := {info with + metaTransTrace := info.metaTransTrace + |>.mix expInfo.metaTransTrace + |>.mix expInfo.metaArtsTrace.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 diff --git a/tests/lake/tests/module/Test/Module/MetaImportImport.lean b/tests/lake/tests/module/Test/Module/MetaImportImport.lean new file mode 100644 index 0000000000..e531f37242 --- /dev/null +++ b/tests/lake/tests/module/Test/Module/MetaImportImport.lean @@ -0,0 +1,3 @@ +module + +meta import Test.Module.Import diff --git a/tests/lake/tests/module/test.sh b/tests/lake/tests/module/test.sh index ce4d8b3d4d..0e4a53d668 100755 --- a/tests/lake/tests/module/test.sh +++ b/tests/lake/tests/module/test.sh @@ -141,8 +141,10 @@ test_run build Test.Module.Import Test.Module.PublicImport --no-build # should trigger a rebuild on a direct `meta import` test_out "Built Test.Module.MetaImport" build Test.Module.MetaImport -v test_out "Built Test.Module.PublicMetaImport" build Test.Module.PublicMetaImport -v -# should trigger a rebuild on a transitive `meta import` +# should trigger a rebuild on a `meta import` of a transitive `public import` test_out "Built Test.Module.MetaImportPublicImport" build Test.Module.MetaImportPublicImport -v +# should trigger a rebuild on a `meta import` of a transitive private `import` +test_out "Built Test.Module.MetaImportImport" build Test.Module.MetaImportImport -v # should trigger a rebuild on module transitive import of a `public meta import` test_out "Built Test.Module.ImportPublicMetaImport" build Test.Module.ImportPublicMetaImport -v # should not trigger a rebuild on module transitive import of a private `meta import`