How to execute .lean file non interactively?

Stream: lean4

[Shange Tang]

Hi, I am new on Lean4. Currently I am trying to write and execute Lean code in VSCode. I need to move my mouse to the end of each line to see the current goal or error message.
However I am wondering how can I execute the entire .lean file and output the goal/error messages for every line? Just like executing a .py file in command line.

[Henrik Böving]

Usually we work with the lake build system and run lake build on the CLI

[Mario Carneiro]

you can run lake lean <name of file> to run just one file

[Mario Carneiro]

but you shouldn't need to move your mouse to see the current goal or error messages

[Shange Tang]

Thank you so much! That helps a lot.

[Kim Morrison]

The "Error Lens" extension in VSCode is also extremely helpful.

[Damiano Testa]

There was also a recent thread with a possibly similar question:

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Discussion.3A.20Making.20Your.20Lean.20Code.20More.20Readable

Maybe the show_goals command from there is useful.