#!/usr/bin/env bash
source ../../env_test.sh

# The test covers the behavior of transitively importing multiple modules
# that have a definition with the same name.

# The native symbols Lean emits are prefixed with a package identifier
# received from Lake. Thus, symbol clashes should not occur between packages.
# However, they can still occur within them.

# Related Issues:
# https://github.com/leanprover/lean4/issues/222

# In the example in this directory, packages `fooA` and `fooB` both define `foo`.
# `useA` privately imports and uses `fooA`, and `useB` private imports and uses
# `fooB`. The executable `TestUse` then imports and uses `useA` and `useB`.

# Similarly, modules `Test.BarA` and `Test.BarB` both define `bar`.
# Modules `UseBarA` and `UseBarB` use them (privately), and `TestLocalUse`
# imports both.

./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).
capture_fail lake build TestFoo
check_out_contains "environment already contains 'foo'"

# Test the behavior when multiple copies of the same definition (`foo`) exist
# in different packages but are not visible to any one module.
capture lake exe TestUse
check_out_contains "fooA; fooB"

# Test the behavior when multiple copies of the same definition (`foo`) exist
# in the same package but are not visible to any one module.
capture_fail lake build TestLocalUse
check_out_contains "lp_test_bar"