Zulip Chat Archive

Stream: new members

Topic: Getting Intermediate Output from Lean

RexWang (Apr 04 2023 at 16:54):

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.


Thanks in advance!!!

Alex J. Best (Apr 04 2023 at 16:58):

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

Jason Rute (Apr 04 2023 at 17:41):

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 (Apr 04 2023 at 17:44):

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

RexWang (Apr 05 2023 at 13:08):

Thanks for the suggestion! They are really helpful.

Alex J. Best (Apr 05 2023 at 14:14):

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)

Last updated: Dec 20 2023 at 11:08 UTC