From 291d238ec4fca5219ff6f742441fa92cbc7a2426 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Wed, 22 Oct 2025 23:42:52 -0400 Subject: [PATCH] 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 | 1 + tests/pkg/def_clash/TestFoo.lean | 3 +++ tests/pkg/def_clash/TestUse.lean | 7 ++++++ tests/pkg/def_clash/clean.sh | 2 ++ tests/pkg/def_clash/deps/fooA/FooA.lean | 3 +++ tests/pkg/def_clash/deps/fooA/lakefile.toml | 5 ++++ tests/pkg/def_clash/deps/fooB/FooB.lean | 3 +++ tests/pkg/def_clash/deps/fooB/lakefile.toml | 5 ++++ tests/pkg/def_clash/deps/useA/UseA.lean | 4 +++ tests/pkg/def_clash/deps/useA/lakefile.toml | 9 +++++++ tests/pkg/def_clash/deps/useB/UseB.lean | 4 +++ tests/pkg/def_clash/deps/useB/lakefile.toml | 9 +++++++ tests/pkg/def_clash/lakefile.toml | 17 +++++++++++++ tests/pkg/def_clash/test.sh | 27 +++++++++++++++++++++ 14 files changed, 99 insertions(+) create mode 100644 tests/pkg/def_clash/.gitignore create mode 100644 tests/pkg/def_clash/TestFoo.lean create mode 100644 tests/pkg/def_clash/TestUse.lean create mode 100755 tests/pkg/def_clash/clean.sh create mode 100644 tests/pkg/def_clash/deps/fooA/FooA.lean create mode 100644 tests/pkg/def_clash/deps/fooA/lakefile.toml create mode 100644 tests/pkg/def_clash/deps/fooB/FooB.lean create mode 100644 tests/pkg/def_clash/deps/fooB/lakefile.toml create mode 100644 tests/pkg/def_clash/deps/useA/UseA.lean create mode 100644 tests/pkg/def_clash/deps/useA/lakefile.toml create mode 100644 tests/pkg/def_clash/deps/useB/UseB.lean create mode 100644 tests/pkg/def_clash/deps/useB/lakefile.toml create mode 100644 tests/pkg/def_clash/lakefile.toml create mode 100755 tests/pkg/def_clash/test.sh diff --git a/tests/pkg/def_clash/.gitignore b/tests/pkg/def_clash/.gitignore new file mode 100644 index 0000000000..10ed5ae23f --- /dev/null +++ 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 new file mode 100644 index 0000000000..730a5c09c4 --- /dev/null +++ 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 new file mode 100644 index 0000000000..c03da91bd2 --- /dev/null +++ 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 new file mode 100755 index 0000000000..d0fc520759 --- /dev/null +++ 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 new file mode 100644 index 0000000000..ef3c1966dc --- /dev/null +++ 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 new file mode 100644 index 0000000000..337fe19f76 --- /dev/null +++ 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 new file mode 100644 index 0000000000..5eeb1fc4d0 --- /dev/null +++ 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 new file mode 100644 index 0000000000..6e6d2d1fe9 --- /dev/null +++ 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 new file mode 100644 index 0000000000..07106dcc63 --- /dev/null +++ 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 new file mode 100644 index 0000000000..95a4a95f2a --- /dev/null +++ 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 new file mode 100644 index 0000000000..02cd1cbb9e --- /dev/null +++ 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 new file mode 100644 index 0000000000..7a978c7ccd --- /dev/null +++ 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 new file mode 100644 index 0000000000..5bc1109c07 --- /dev/null +++ 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 new file mode 100755 index 0000000000..afb51b29ed --- /dev/null +++ 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