lean-client-python
lean-client-python copied to clipboard
leanprover-community
Lean IPython kernel
Could this lean client be use to write an IPython kernel that supports Lean?
Hello Simon :), been awhile.
Indeed, I think someone's just done so in a POC.
The Zulip thread is here and starts with Lean 4 (the new version of Lean, where doing so should be much easier). But there's a Lean 3 one at the bottom -- albeit I think it just talks to the server directly without using this client. It seems to me it could though. Perhaps worth having a look and asking further there.
Thanks Julian! That is awesome. And indeed it has been awhile. Glad to see we are both still doing lots of free software things. :D
The use case I have in mind is to be able to use something like Jupyter book or Jupyter notebooks to run Lean examples alongside written proofs (both for teachers and for students).
Glad to see we are both still doing lots of free software things. :D
So am I :D (congrats on the HPy release)
Patrick Massot (who I'm sure is being pinged, he originally wrote a lot of what's here) has some nice tooling for doing things like that as I understand it, albeit not specifically via Jupyter. There's also some work going on to port Alectryon to Lean. Perhaps besides the above Jupyter link, you might come stop by the Lean for Teaching Zulip Stream -- there definitely are others (including Patrick) with useful expertise there using Lean in similar scenarios.
Alectryon looks great! Perhaps it is already enough to make somethings using Jupyter book since that already passes things to Sphinx. I will check out the Lean for Teaching stream.