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

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.

tests/pkg/def_clash/.gitignore

@@ -0,0 +1 @@
+produced.out

tests/pkg/def_clash/TestFoo.lean

@@ -0,0 +1,3 @@
+module
+import FooA
+import FooB

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

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

tests/pkg/def_clash/deps/fooA/FooA.lean

@@ -0,0 +1,3 @@
+module
+
+public def foo : String := "fooA"

tests/pkg/def_clash/deps/fooA/lakefile.toml

@@ -0,0 +1,5 @@
+name = "fooA"
+
+[[lean_lib]]
+name = "FooA"
+leanOptions.experimental.module = true

tests/pkg/def_clash/deps/fooB/FooB.lean

@@ -0,0 +1,3 @@
+module
+
+public def foo : String := "fooB"

tests/pkg/def_clash/deps/fooB/lakefile.toml

@@ -0,0 +1,5 @@
+name = "fooB"
+
+[[lean_lib]]
+name = "FooB"
+leanOptions.experimental.module = true

tests/pkg/def_clash/deps/useA/UseA.lean

@@ -0,0 +1,4 @@
+module
+import FooA
+
+public def useA : String := foo

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"

tests/pkg/def_clash/deps/useB/UseB.lean

@@ -0,0 +1,4 @@
+module
+import FooB
+
+public def useB : String := foo

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"

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"

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