printing to stdout

Stream: lean4

[Damiano Testa]

Dear All,

this is a very basic question.

Is it possible to run a command like lean --run <pathToFile> that would print to stdout all the #eval and whatever appears in the infoview? lean --run seems to only work for files that do not import anything else, whereas I would like this to run on files with imports. I use Linux Mint, in case it matters.

Thanks!

[Gabriel Ebner]

You want lake env lean <pathToFile>

[Gabriel Ebner]

--run runs the main function

[Damiano Testa]

Great, thanks! I'll play around with it!

[Damiano Testa]

Gabriel, this seems exactly what I was looking for: thank you very much!