Test do not use lakefile config

Stream: mathlib4

[Patrick Massot]

Our CI for Mathlib run lake env lean test/whatever.lean to execute each test file. But this isn't picking up the pretty-printing options from the Mathlib lakefile. This failure comes from a guard_msg that works perfectly inside VSCode but fails in CI because of the ugly fun ... => ... that is the default printting.

[Kyle Miller]

We've been adding set_option pp.unicode.fun true to tests as a workaround

[Patrick Massot]

Thanks for fixing this, but I think we need a better solution in the long run.

[Patrick Massot]

Is this something we should consider to be a lake issue or an issue with our CI setup?

[Scott Morrison]

Pinging @Mac Malone for an opinion on this.

Obviously we are just missing a good testing framework for Lean, but in the meantime solving these annoyances will inform what such a testing framework should do.

One option is to make the tests into their own library, i.e. another lean_lib in the lakefile, like we have Archive and Counterexamples in Mathlib. This will then pick up options set at either the package or library level, and you'll be able to run all the tests with lake build Test.

[Scott Morrison]

Currently this is problematic because this will prevent a downstream project having its own lean_lib Test.

I think after our lake meeting yesterday @Mac Malone has an idea about solving this (an option so that for downstream projects Mathlib's lean_lib Test will look like Mathlib.Test), but I'm not sure whose job it is to write this up as an RFC issue. @Mac Malone?

[Mario Carneiro]

I think we could write the test suite as a lake script, although I really don't like adding lines to the lakefile

[Mario Carneiro]

with that approach you would be able to call lean with the right arguments

[Scott Morrison]

Alternatively a lake exe. (I agree that I don't want any lake scripts if possible.)