test: module clash across packages (#11246)

tydeu · web-flow · commit 687698e79d97 · 2025-11-19T02:23:34.000Z
This PR adds a test that covers importing modules defined in multiple
packages.

Currently, will resolve the module to its first occurrence in the its
search order. However, this will soon change, so this test is designed
to analyze that behavior.
diff --git a/tests/pkg/.gitignore b/tests/pkg/.gitignore
@@ -1 +1,2 @@
 lake-manifest.json
+produced.out
diff --git a/tests/pkg/mod_clash/Test/ImportDiff.lean b/tests/pkg/mod_clash/Test/ImportDiff.lean
@@ -0,0 +1,3 @@
+import Diff
+
+def testDiff := foo
diff --git a/tests/pkg/mod_clash/Test/ImportSame.lean b/tests/pkg/mod_clash/Test/ImportSame.lean
@@ -0,0 +1,3 @@
+import Same
+
+def testSame := same
diff --git a/tests/pkg/mod_clash/clean.sh b/tests/pkg/mod_clash/clean.sh
@@ -0,0 +1,3 @@
+rm -rf .lake lake-manifest.json produced.out
+rm -rf depA/.lake depA/lake-manifest.json
+rm -rf depB/.lake depB/lake-manifest.json
diff --git a/tests/pkg/mod_clash/depA/Diff.lean b/tests/pkg/mod_clash/depA/Diff.lean
@@ -0,0 +1 @@
+def foo := "depA"
diff --git a/tests/pkg/mod_clash/depA/Same.lean b/tests/pkg/mod_clash/depA/Same.lean
@@ -0,0 +1 @@
+def same := 0
diff --git a/tests/pkg/mod_clash/depA/lakefile.toml b/tests/pkg/mod_clash/depA/lakefile.toml
@@ -0,0 +1,7 @@
+name = "depA"
+
+[[lean_lib]]
+name = "Same"
+
+[[lean_lib]]
+name = "Diff"
diff --git a/tests/pkg/mod_clash/depB/Diff.lean b/tests/pkg/mod_clash/depB/Diff.lean
@@ -0,0 +1 @@
+def bar := "depB"
diff --git a/tests/pkg/mod_clash/depB/Same.lean b/tests/pkg/mod_clash/depB/Same.lean
@@ -0,0 +1 @@
+def same := 0
diff --git a/tests/pkg/mod_clash/depB/lakefile.toml b/tests/pkg/mod_clash/depB/lakefile.toml
@@ -0,0 +1,7 @@
+name = "depB"
+
+[[lean_lib]]
+name = "Same"
+
+[[lean_lib]]
+name = "Diff"
diff --git a/tests/pkg/mod_clash/lakefile.toml b/tests/pkg/mod_clash/lakefile.toml
@@ -0,0 +1,12 @@
+name = "test"
+
+[[lean_lib]]
+name = "Test"
+
+[[require]]
+name = "depA"
+path = "depA"
+
+[[require]]
+name = "depB"
+path = "depB"
diff --git a/tests/pkg/mod_clash/test.sh b/tests/pkg/mod_clash/test.sh
@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+source ../../lake/tests/common.sh
+
+# This test covers importing modules which are defined in multiple packages.
+
+./clean.sh
+test_run resolve-deps
+
+# Test that importing a module with multiple equivalent candidates works
+test_run build Test.ImportSame
+
+# Test that importing a module with multiple distinct candidates fails
+test_err 'Unknown identifier `foo`' build Test.ImportDiff

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+import Diff`
	`2`	`+`
	`3`	`+def testDiff := foo`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+import Same`
	`2`	`+`
	`3`	`+def testSame := same`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+rm -rf .lake lake-manifest.json produced.out`
	`2`	`+rm -rf depA/.lake depA/lake-manifest.json`
	`3`	`+rm -rf depB/.lake depB/lake-manifest.json`