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