Running tests with options

Stream: mathlib4

[Scott Morrison]

@Kyle Miller pointed out that we should make tests run with the standard options from the lakefile.lean, to avoid hacks like this and this.

Thus we will need to run the tests from the lakefile. Does anyone know an example of doing this? What is the best practice here?

My simple proposal would be to arrange the tests as another lean_lib, much like Archive and Counterxamples.

[Yury G. Kudryashov]

This will make test.* available for import to any package that depends on mathlib4.

[Yury G. Kudryashov]

It would be nice to have a flag for "unreleased" lean_libs in lakefiles.

[Scott Morrison]

@Mac, do you have advice on how we should set this up?

[Scott Morrison]

(Either the general question of a lakefile.lean driven test suite, or how to mark lean_libs as "unreleased" / "private" / etc.)

[Mac Malone]

Yury G. Kudryashov said:

It would be nice to have a flag for "unreleased" lean_libs in lakefiles.

I was actually working on this, but I realized this is unfortunately infeasible with the current setup. If a module exists in the build directory and that build directory is in the Lean path, than Lean will pick it up. Thus, If two packages have a module test/basic.lean they will clash due to Leans module resolution rules. And there is not a way for Lake to intervene here do to this all being Lean-side (i.e., and import Test.Basic will run into this problem when Lean runs the containing file)

One solution would be to hoist all build files into the workspace root's build directory and selective choose which to hoist, but this could cause problem for things like cache.

[Mac Malone]

As an alternative for tests, one could make a script to run them to and execute lean with the package's moreLeanArgs / moreServerArgs.

[Mac Malone]

Also, if anyone has any ideas how to make this easier (or how else to overcome LEAN_PATH resolution), I would be happy to here them.

[Yury G. Kudryashov]

Can't lake ignore some lean_libs (and don't tell Lean about them) unless it is running with, say, --enable-tests?

[Yury G. Kudryashov]

So that these modules will not be in lake-packages/*/build/lib for a reverse dependency?

[Scott Morrison]

So under this suggestion, the source files for the mathlib tests would appear in a downstream project's lake-packages, but they would not be built or added to the LEAN_PATH.