Getting Intermediate Output from Lean

Stream: new members

[RexWang]

Is there a way to directly interact with the front end of Lean to get the intermediate output. For example, using Python or other tools? The purpose of doing so is to check for syntax errors and update goals when the proof reaches a certain step. This would be very helpful for research experiment. Considering of the VSCode plugin, this seems possible, but I'm not sure how to do it.

vscode

Thanks in advance!!!

[Alex J. Best]

It sounds a bit like you are looking for https://github.com/leanprover-community/lean-client-python

[Jason Rute]

That Python client is just a light weight wrapper around the lean 3 language server which is how editors like vs code interact with Lean. So anything you see in the editor is available in that client (or the server directly). It unfortunately is sparse on examples or documentation, but it is probably a good way to start interfacing with Lean. It can be a bit slow for some applications and frankly the Lean server has a lot of quirks. Another approach is to more directly interact with Lean via metaprogramming. It is more work at first, but could have good payoff. It really depends on your application.

[Jason Rute]

Also this is actually a very common question. You probably can find a lot of advice here on Zulip.

[RexWang]

Thanks for the suggestion! They are really helpful.

[Alex J. Best]

Since you asked your question @Scott Morrison released a Lean 4 repl tool https://github.com/leanprover-community/repl this might also be a good way to go (Lean 4 is the future after all, though there are still a few issues at this point depending on what you want to do)