From 687698e79d9762033031f87b3ea59b2b65d34c85 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Tue, 18 Nov 2025 21:23:34 -0500 Subject: [PATCH] test: module clash across packages (#11246) 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. --- tests/pkg/.gitignore | 1 + tests/pkg/mod_clash/Test/ImportDiff.lean | 3 +++ tests/pkg/mod_clash/Test/ImportSame.lean | 3 +++ tests/pkg/mod_clash/clean.sh | 3 +++ tests/pkg/mod_clash/depA/Diff.lean | 1 + tests/pkg/mod_clash/depA/Same.lean | 1 + tests/pkg/mod_clash/depA/lakefile.toml | 7 +++++++ tests/pkg/mod_clash/depB/Diff.lean | 1 + tests/pkg/mod_clash/depB/Same.lean | 1 + tests/pkg/mod_clash/depB/lakefile.toml | 7 +++++++ tests/pkg/mod_clash/lakefile.toml | 12 ++++++++++++ tests/pkg/mod_clash/test.sh | 13 +++++++++++++ 12 files changed, 53 insertions(+) create mode 100644 tests/pkg/mod_clash/Test/ImportDiff.lean create mode 100644 tests/pkg/mod_clash/Test/ImportSame.lean create mode 100755 tests/pkg/mod_clash/clean.sh create mode 100644 tests/pkg/mod_clash/depA/Diff.lean create mode 100644 tests/pkg/mod_clash/depA/Same.lean create mode 100644 tests/pkg/mod_clash/depA/lakefile.toml create mode 100644 tests/pkg/mod_clash/depB/Diff.lean create mode 100644 tests/pkg/mod_clash/depB/Same.lean create mode 100644 tests/pkg/mod_clash/depB/lakefile.toml create mode 100644 tests/pkg/mod_clash/lakefile.toml create mode 100755 tests/pkg/mod_clash/test.sh diff --git a/tests/pkg/.gitignore b/tests/pkg/.gitignore index 484bdc670f..3c8b7dae07 100644 --- 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 new file mode 100644 index 0000000000..722e3067ba --- /dev/null +++ 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 new file mode 100644 index 0000000000..4235520695 --- /dev/null +++ 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 new file mode 100755 index 0000000000..f07293fd2a --- /dev/null +++ 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 new file mode 100644 index 0000000000..6ade3028f7 --- /dev/null +++ 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 new file mode 100644 index 0000000000..949bb69ad2 --- /dev/null +++ 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 new file mode 100644 index 0000000000..197dc30c8f --- /dev/null +++ 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 new file mode 100644 index 0000000000..4ddddea480 --- /dev/null +++ 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 new file mode 100644 index 0000000000..949bb69ad2 --- /dev/null +++ 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 new file mode 100644 index 0000000000..f73b9a27aa --- /dev/null +++ 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 new file mode 100644 index 0000000000..ba506393d1 --- /dev/null +++ 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 new file mode 100755 index 0000000000..f451c838d0 --- /dev/null +++ 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