search

leanprover-community / lean-client-python

Python talking to the Lean theorem prover
Apache License 2.0
39 stars 6 forks source link

Lean IPython kernel #23

Open hodgestar opened 2 years ago

hodgestar commented 2 years ago

Could this lean client be use to write an IPython kernel that supports Lean?

Julian commented 2 years ago

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.

hodgestar commented 2 years ago

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).

Julian commented 2 years ago

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.

hodgestar commented 2 years ago

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.