MathlibTest.MathlibTestExecutable

Stream: mathlib4

[Chris Henson]

Am I correct that MathlibTest.MathlibTestExecutable (the lean_exe target for this file) is not included in the Mathlib test driver? If I wanted something similar but also want to include it with the runner called for lake test, what would be the recommended way to do this?

[Kim Morrison]

I think it is built by lake test, but not compiled. That we only do in a once-daily CI job. (Which, incidentally, has been failing for more than a week, and I haven't got around to investigating why. :embarrassed:)

[Kim Morrison]

I'm actually not sure how to ask for compilation via lake test. I guess you could write an auxiliary test file that shells out lake exe MathlibTest.MathlibTestExecutable (ick?)

[Chris Henson]

Yeah, that ick is why I asked. We currently have something similar proposed in cslib#131 and I was hoping there was a better way...

[Kim Morrison]

@Mac Malone, I guess we need to ask you? Can we ask for compilation of some module from lake test?

[Mac Malone]

@Kim Morrison An executable itself can be a test driver, which I think would achieve the desired result here.

[Chris Henson]

What I meant here is a single test driver composed of multiple lean_exe and lean_lib from the lakefile. In the example of Mathlib for instance, both MathlibTest and and an executable like MathlibTest.MathlibTestExecutable.

[Kim Morrison]

In that case I think we need:

chore: support multiple Lake test drivers #10531

[Kim Morrison]

(warning, that PR was written by some random AI and I don't particularly vouch for it, hence it languishing in draft as I never got back to reviewing it.)