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 +1,2 @@
 lake-manifest.json
+produced.out

tests/pkg/mod_clash/Test/ImportDiff.lean

@@ -0,0 +1,3 @@
+import Diff
+
+def testDiff := foo

tests/pkg/mod_clash/Test/ImportSame.lean

@@ -0,0 +1,3 @@
+import Same
+
+def testSame := same

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

tests/pkg/mod_clash/depA/Diff.lean

@@ -0,0 +1 @@
+def foo := "depA"

tests/pkg/mod_clash/depA/Same.lean

@@ -0,0 +1 @@
+def same := 0

tests/pkg/mod_clash/depA/lakefile.toml

@@ -0,0 +1,7 @@
+name = "depA"
+
+[[lean_lib]]
+name = "Same"
+
+[[lean_lib]]
+name = "Diff"

tests/pkg/mod_clash/depB/Diff.lean

@@ -0,0 +1 @@
+def bar := "depB"

tests/pkg/mod_clash/depB/Same.lean

@@ -0,0 +1 @@
+def same := 0

tests/pkg/mod_clash/depB/lakefile.toml

@@ -0,0 +1,7 @@
+name = "depB"
+
+[[lean_lib]]
+name = "Same"
+
+[[lean_lib]]
+name = "Diff"

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"

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