lake: how to build all .lean files without importing them?

Stream: lean4

[Alok Singh]

say I make a new dep-free file A.lean. Unless the main project imports A somehow, lake build will just ignore A.lean. Is there a way to force a build across all lean files, so any errors in A.lean are printed? i can imagine many ways of scripting it but if there's a recommended way i'd prefer that.

[Kevin Buzzard]

The way I've been doing it in FLT is to have FLT.lean in the root directory and to check that it contains a list of all the files in FLT/ by running lake exe mk_all. Mathlib has the same system and checks that lake exe mk_all doesn't change Mathlib.lean in CI. Edit: oh, as of last weekend we have the check in FLT CI as well here.

[Anand Rao Tadipatri]

I wrote a script a while ago that automatically generates top-level files that import all the contents of the folders: #lean4 > Lake script for automatically generating files with imports @ 💬.

This is slightly different from what you want, which is to build all files without any imports, but I thought I'd share this here in case it's useful nevertheless.

[Patrick Massot]

You can use globs. See for instance https://github.com/PatrickMassot/proofs_with_lean/blob/master/lakefile.toml