time a single test file

Stream: mathlib4

[Rob Lewis]

This is probably a silly question, but I haven't had to do it in the Lean4 era yet and can't find the right incantation. I'm trying to profile a single file in the test directory. What's the proper way to measure the build time? (Equivalently, how do I tell lake to build one file in test?)

[Mario Carneiro]

lake env lean Test.lean

[Mario Carneiro]

lake env time lean Test.lean