retrieve intermediate states of proofs and error messages

Stream: new members

[Kei TSUKAMOTO]

I would like to know how to retrieve intermediate states of proofs and error messages from the Lean server. I'm using Lean 3. Could you please advise?

[Alex J. Best]

The lean server communicates via json, probably the easiest way is to use https://github.com/leanprover-community/lean-client-python

[Kei TSUKAMOTO]

Thank you for telling me! I'm trying trio_example.py, and I could get states but could not get error messages. How to rewrite trio_example.py and retrieve error messages?
https://github.com/leanprover-community/lean-client-python/blob/master/examples/trio_example.py

[Scott Morrison]

I would suggest it's not worth investing new effort into tooling built around Lean 3. I would suggest https://github.com/leanprover-community/repl/pull/5 is the way forward.

[Kei TSUKAMOTO]

Appreciate for your advice! I've decided to change to lean4. Is it possible to retrieve intermediate state of proof by using repl at the moment?

https://github.com/leanprover-community/repl