From 49d4752bfd50ee8431f95b77d7d30abde1f61ff0 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Tue, 16 Dec 2025 03:28:52 -0500 Subject: [PATCH] fix: lake: `meta import` transitivity (#11683) This PR fixes an inconsistency in the way Lake and Lean view the transitivity of a `meta import`. Lake now works as Lean expects and includes the meta segment of all transitive imports of a `meta import` in its transitive trace. --- src/lake/Lake/Build/Module.lean | 12 ++++++------ .../tests/module/Test/Module/MetaImportImport.lean | 3 +++ tests/lake/tests/module/test.sh | 4 +++- 3 files changed, 12 insertions(+), 7 deletions(-) create mode 100644 tests/lake/tests/module/Test/Module/MetaImportImport.lean 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`