test: symbol clash on private import of same def (#10915)

tydeu · web-flow · commit 291d238ec4fc · 2025-10-23T03:42:52.000Z
This PR adds a test for depending on two packages which privately import
modules that define the same Lean definition. It verifies the current
behavior of a symbol clash. This behavior will be fixed later this
quarter.
diff --git a/tests/pkg/def_clash/.gitignore b/tests/pkg/def_clash/.gitignore
@@ -0,0 +1 @@
+produced.out
diff --git a/tests/pkg/def_clash/TestFoo.lean b/tests/pkg/def_clash/TestFoo.lean
@@ -0,0 +1,3 @@
+module
+import FooA
+import FooB
diff --git a/tests/pkg/def_clash/TestUse.lean b/tests/pkg/def_clash/TestUse.lean
@@ -0,0 +1,7 @@
+module
+import UseA
+import UseB
+
+def main : IO Unit := do
+  IO.println useA
+  IO.println useB
diff --git a/tests/pkg/def_clash/clean.sh b/tests/pkg/def_clash/clean.sh
@@ -0,0 +1,2 @@
+rm -rf lake-manifest.json .lake/build produced.out
+rm -rf deps/fooA/.lake/build deps/fooB/.lake/build deps/useA/.lake/build deps/useB/.lake/build
diff --git a/tests/pkg/def_clash/deps/fooA/FooA.lean b/tests/pkg/def_clash/deps/fooA/FooA.lean
@@ -0,0 +1,3 @@
+module
+
+public def foo : String := "fooA"
diff --git a/tests/pkg/def_clash/deps/fooA/lakefile.toml b/tests/pkg/def_clash/deps/fooA/lakefile.toml
@@ -0,0 +1,5 @@
+name = "fooA"
+
+[[lean_lib]]
+name = "FooA"
+leanOptions.experimental.module = true
diff --git a/tests/pkg/def_clash/deps/fooB/FooB.lean b/tests/pkg/def_clash/deps/fooB/FooB.lean
@@ -0,0 +1,3 @@
+module
+
+public def foo : String := "fooB"
diff --git a/tests/pkg/def_clash/deps/fooB/lakefile.toml b/tests/pkg/def_clash/deps/fooB/lakefile.toml
@@ -0,0 +1,5 @@
+name = "fooB"
+
+[[lean_lib]]
+name = "FooB"
+leanOptions.experimental.module = true
diff --git a/tests/pkg/def_clash/deps/useA/UseA.lean b/tests/pkg/def_clash/deps/useA/UseA.lean
@@ -0,0 +1,4 @@
+module
+import FooA
+
+public def useA : String := foo
diff --git a/tests/pkg/def_clash/deps/useA/lakefile.toml b/tests/pkg/def_clash/deps/useA/lakefile.toml
@@ -0,0 +1,9 @@
+name = "useA"
+
+[[lean_lib]]
+name = "UseA"
+leanOptions.experimental.module = true
+
+[[require]]
+name = "fooA"
+path = "../fooA"
diff --git a/tests/pkg/def_clash/deps/useB/UseB.lean b/tests/pkg/def_clash/deps/useB/UseB.lean
@@ -0,0 +1,4 @@
+module
+import FooB
+
+public def useB : String := foo
diff --git a/tests/pkg/def_clash/deps/useB/lakefile.toml b/tests/pkg/def_clash/deps/useB/lakefile.toml
@@ -0,0 +1,9 @@
+name = "useB"
+
+[[lean_lib]]
+name = "UseB"
+leanOptions.experimental.module = true
+
+[[require]]
+name = "fooB"
+path = "../fooB"
diff --git a/tests/pkg/def_clash/lakefile.toml b/tests/pkg/def_clash/lakefile.toml
@@ -0,0 +1,17 @@
+name = "test"
+
+[[lean_lib]]
+name = "TestFoo"
+leanOptions.experimental.module = true
+
+[[lean_exe]]
+name = "TestUse"
+leanOptions.experimental.module = true
+
+[[require]]
+name = "useA"
+path = "deps/useA"
+
+[[require]]
+name = "useB"
+path = "deps/useB"
diff --git a/tests/pkg/def_clash/test.sh b/tests/pkg/def_clash/test.sh
@@ -0,0 +1,27 @@
+#!/usr/bin/env bash
+
+# Tests the behavior of transitively importing multiple modules
+# that define the same symbol.
+
+# Currently, if two packages define the same Lean symbol (e.g., `foo`)
+# they cannot be in the same transitive import graph, even if the no module
+# can see both instances of the symbol.
+
+# In the example in this directory, `fooA` and `fooB` both define `foo`.
+# `useA` privately imports and uses `fooA`, and `useB` private imports and uses
+# `fooB`. When `TestUse` imports `useA` and `useB`, the linker will complain
+# even though the Lean file does not see both `foo` definitions.
+
+# See also https://github.com/leanprover/lean4/issues/222
+
+source ../../lake/tests/common.sh
+
+./clean.sh
+
+# Test the behavior when multiple copies of the same definition (`foo`)
+# are seen by Lean (e.g., via importing two modules which define them).
+test_err "environment already contains 'foo'" build TestFoo
+
+# Test the behavior when multiple copies of the same definition (`foo`) exist
+# but are not visible to any one module: a symbol clash between the two `foo`s.
+test_err "l_foo" build TestUse

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+module`
	`2`	`+import FooA`
	`3`	`+import FooB`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,2 @@`
	`1`	`+rm -rf lake-manifest.json .lake/build produced.out`
	`2`	`+rm -rf deps/fooA/.lake/build deps/fooB/.lake/build deps/useA/.lake/build deps/useB/.lake/build`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+module`
	`2`	`+`
	`3`	`+public def foo : String := "fooA"`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+module`
	`2`	`+`
	`3`	`+public def foo : String := "fooB"`
-Original file line number
+Diff line change
@@ @@ -0,0 +1,4 @@ @@
 +module
 +import FooA
++
 +public def useA : String := foo