Querying Lean Status Information from Terminal

Stream: lean4

[Jianqiao Lu]

I'm currently exploring the capabilities of Infoview in Lean, where it allows me to directly observe the Lean status of each .lean file, including aspects like grammar errors or the output from #check. I'm interested in finding a way to extract this information through a terminal command. Specifically, I'm looking to retrieve details on grammar errors and the results from #check commands in my .lean files via the terminal.

Could anyone guide me on how to achieve this? Any pointers or commands that could help me access this Lean status information from the terminal would be greatly appreciated.

Thank you! (Moreover, like Albert Jiang provided a PISA (Portal to ISAbelle) to help automatically test in Isabelle, I was wondering if there is any similar tool in lean4?)

[Joachim Breitner]

Maybe https://github.com/leanprover-community/repl is close to what you need?

[Jianqiao Lu]

Joachim Breitner said:

Maybe https://github.com/leanprover-community/repl is close to what you need?

sry for the late reply and this very much, it is exactly what I want

[Jianqiao Lu]

Joachim Breitner said:

Maybe https://github.com/leanprover-community/repl is close to what you need?

sorry for the late reply, this for you kindly reply and it is exactly what i want!!!!!