mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 10:24:07 +00:00
49715fe63c
The tests need to run with certain environment variables set that only cmake really knows and that differ between stages. Cmake could just set the variables directly when running the tests and benchmarks, but that would leave no good way to manually run a single benchmark. So cmake generates some stage-specific scripts instead that set the required environment variables. Previously, those scripts were sourced directly by the individual `run_*` scripts, so the env scripts of different stages would overwrite each other. This PR changes the setup so they can instead be generated next to each other. This also simplifies the `run_*` scripts themselves a bit, and makes `tests/bench/build` less of a hack.
35 lines
1.4 KiB
Bash
35 lines
1.4 KiB
Bash
# 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"
|