easiest way to get all diagnostics for a new file in cli

Stream: new members

[Xiyu Zhai]

Hi, for my project, I need to have a quick way to get lean4 diagnostics information for a large number of independent files that a small amount of code that depends only on Mathlib4. I would like to know to achieve this.

Background: I'm doing research in autoformalization. I need my pipeline to get lean feedback quickly.

I would like to:

• can be implemented in code like bash or some hack on leanc
• as fast as possible, utilizing mathlib4 cache efficiently
• as simple as possible

Here's what I've tried. It seems that each lean package stores its own copy of mathlib cache. So I set up a central package with mathlib4. And then each file is put under the package, although not imported by the main Basic.lean. lake build simply wouldn't work, because these small files are not imported by the main Basic.lean. Then I tried lake lean, which seems to often output irrelevant information like warnings in Mathlib4 docstrings which I totally don't want to see for my project.

I'm thinking whether I need to go the trouble of using lean server for this purpose.

What would you guys suggest? Thanks a lot in advance.

[Xiyu Zhai]

Maybe if I first lake build with Basic.lean importing Mathlib, then lake lean message would be cleaner?