building many independent files with lake

Stream: lean4

[Jireh Loreaux]

Let's suppose I have a bunch of files Foo/Bar1.lean, Foo/Bar2.lean, etc., and I would like lake to build these with the following caveat: I don't want to simply create a new file of the form:

import Foo.Bar1
import Foo.Bar2
...

and have lake build that (which I understand I would do with @[default target] lean_lib «Foo»). Instead, I would like lake to build all of these files independently, but I would prefer the user to only type lake build. Can I accomplish this?

[Jireh Loreaux]

I would go look in the reference manual, but that section isn't ready just yet.

[Damiano Testa]

According to this message, globbing appears to be the answer, but I have never used it.

[Jireh Loreaux]

Thanks! Undocumented globs to the rescue!