feature request: multiple testDrivers in lake

[kim-em]

We've encountered a situation (leanprover-community/aesop#182) where we would really like Aesop's testing framework to both:

• build a library
• run an executable

Could we please have testDrivers (plural) to enable this?

[tydeu]

Why not just create a single test driver (executable) that performs both of these actions?

[kim-em]

Because then I have all the overhead of writing a main function, that calls out to another executable, runs lake on AesopTest, etc. It's also way less obvious to someone reading the lake file what testing actually consists of.

In practice as a workaround in Aesop for now I'm going to handle running the extra executable in CI.

[kim-em]

#10531 is an AI-written implementation, I haven't had the time to seriously look if it is sane or not. For now: if anyone would like to look, it's there.