Prototype: Jupyter for Lean4

Stream: lean4

[Siddharth Bhat]

Here's an example of a Hello World Jupyter notebook that was created with the Jupyter Kernel in the same repo. Note that Github renders Jupyter notebooks by default!

Rationale

As I understand it, LeanInk is meant for static visualization of Lean4 code+proofs. I wondered if having a Jupyter kernel would complement this in writing "programming" style Lean4 code. I wonder what others feel about this, and if it makes sense to develop this further. This was a quick weekend hack to see if this is feasible (seems to be so!)

Technical details

This is implemented as a large chunk of C++ in asm-kernel.cpp that interacts with Jupyter via ZeroMQ, and a little bit of Lean4 in REPLLib.lean to run Lean4 commands. Many thanks to arthurpaulino/LeanREPL for the REPL code.

Questions

I'd like to develop this further for fun, so feature requests would be nice :wink:. More to the point, I don't want to duplicate work and split the community's attention between the Jupyter kernel and LeanInk, so having a clearer picture of the relationship between the two would be very useful for me!

[Kevin Buzzard]

Just to remark the obvious -- things like this would be really useful for people like me who are teaching this stuff.

[Johan Commelin]

That's a great proof of concept! Well done!

[Sofia]

Very nice to see. Does it suffer the usual Jupyter notebook issue where dependent cells are not updated?

Julia's Pluto.jl notebook resolves this issue. Might have other things worth looking into. https://github.com/fonsp/Pluto.jl

[Sofia]

Pluto offers an environment where changed code takes effect instantly and where deleted code leaves no trace. Unlike Jupyter or Matlab, there is no mutable workspace, but rather, an important guarantee:

At any instant, the program state is completely described by the code you see.

No hidden state, no hidden bugs.

[Sofia]

If my language/compiler project goes well, I plan to make a Pluto.jl style reactive notebook with a Hazel.org style editor. All edits produce valid syntax. A program containing holes may still be partially reduced. Likewise type and binding errors become holes. All intermediate editor states are thus useful without heuristics or breaking the LSP's ability to infer types and so on.

[Sofia]

I know Lean is somewhat accepting with invalid syntax, but it doesn't go out of its way to inject typed holes in place of binding or type errors. I wonder how difficult this would be to add to Lean...

[Sofia]

Or if it'd even be welcome.

[James Gallicchio]

I'm very supportive of structure editors, personally, but I didn't find the Hazel.org editor to be the smoothest experience..... I would happily use a structure editor for Lean if it was as smooth of an experience as using VSCode :P

[James Gallicchio]

(This might partly be a symptom of the VSCode extension not having substantial autocomplete options -- once we have e.g. exhaustive match template generation, the need might be even less there)

[Sofia]

Hazel certainly could be a lot smoother. I've been thinking more like the traditional auto-complete syntax expansion, maybe even grayed out multiple-choice.

[Arthur Paulino]

Nice work!!
The REPL I wrote (which is not completely authorial either) supports rollbacks exactly for the cases in which an upward cell is executed. In this scenario, my plan would be to reset the cells below it and clean their output.

I'd recommend keeping a clear use case in mind for the development of the kernel so you knowi what you're aiming at. I wrote the REPL after seeing Tomas' SciLean lib and I thought that eventually we'd be able to process data in Lean. Turns out Jupyter notebooks are great for that because once you run the code to read a dataframe, it's cached in memory so you're free to play with it.

The downside of a Jupyter notebook is that we don't have the fast interactive response from the server while we're trying to prove theorems for example (which is a big part of Lean's use case)

[Sebastian Ullrich]

Turns out Jupyter notebooks are great for that because once you run the code to read a dataframe, it's cached in memory so you're free to play with it.

I mean, that's true of the Lean language server as well, no? Do you have something in mind we could improve there?

[Arthur Paulino]

Reading a dataframe (say a CSV file) sounds like an IO operation to me. The current limitation I see is that IO calls like read/write files can be run after you compile your Lean code to a binary and run it. We can't, for instance, run a piece of code to read a file and play with its content on the same interface, whereas an interface like Jupyter would be fine for such task

[Arthur Paulino]

(the limitation might be on the combination of VS Code + lean4 plugin rather than on the language server)

[Arthur Paulino]

I even came to the point of envisioning a separate plugin to talk to the language server from Jupyter, similar to what we have for VS Code. So we would have a Lean 4 infoview on Jupyter. But the motivation needs to be strong before that path is crossed because I think it's a long road with a lot of work

[Sebastian Ullrich]

There is no such limitation, see https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Util/IncludeStr.lean

[Sebastian Ullrich]

Having said that, while I believe the current compilation strategy should ensure the string is loaded exactly once as long as only text below it is changed, this is not true for further computations done on the string, even if they are stored in parameter-less defs. This is a performance optimization in the interpreter we've considered before, but it has been low priority so far.

[Arthur Paulino]

Interesting! But what about plotting things? Jupyter supports having images as the output of cells

[Henrik Böving]

Technically speaking the infoview could support plotting things as well and e.g. pretty print trees as SVGs instead of the more sexp like representation

[Arthur Paulino]

Makes sense, but it's different from having the plots laid out so people can just scroll down and explore the document.
I am aware that I'm making a stretch because I am talking about using Lean for a task that has the right tooling already set for Python, R etc. I am just daydreaming :D

[Christian Pehle]

I experimented with plotting a bit using a hacked lean-vscode that didn't escape html in strings, I thought it was surprisingly nice to just rendered svg in a separate organised pane next to the eval commands, which automatically update when you change code.

[François G. Dorais]

This is really cool!

Arthur Paulino said:

[...] In this scenario, my plan would be to reset the cells below it and clean their output.

This goes against the traditional notebook format where things are executed in order they are input and not in the order of the file contents. I think the traditional notebook format is a bad fit for Lean so a non-traditional notebook format is probably better. The drawback is that I would expect having to constantly battle with the Jupyter core in the implementation. I hope it works out anyway!

[James Gallicchio]

Christian Pehle said:

I experimented with plotting a bit using a hacked lean-vscode that didn't escape html in strings, I thought it was surprisingly nice to just rendered svg in a separate organised pane next to the eval commands, which automatically update when you change code.

Now I'm wondering how hard it would be to hack lean-vscode to show all #eval output in a continuous panel that automatically scrolls to where you are in the document, like what the markdown extension does for previewing your markdown

[James Gallicchio]

Is your code in a repository somewhere that I can play around with? :joy:

[Henrik Böving]

If i look at my goal view in Emacs the language server is already telling the client/vscode in this case where the messages are coming from line (and even column) wise so If you have some code to sync that scrolling, shouldnt be too hard.

[James Gallicchio]

If we get something like that working, + a library for building data visualizations in HTML, + SciLean, + the optimization Sebastian mentioned, I feel like we'd basically have a Lean replacement for jupyter, no?

[James Gallicchio]

(Oh, one other "small" thing -- making a web extension for VS Code, so that it can be run in the browser...)

[Tomas Skrivan]

In emacs, lsp can highlight subterms and show their types, see attached picture(probably works in VS code too).

Screenshot-from-2022-05-18-10-17-59.png

Would it be possible to get something similar in the goal view? In particular, I would like to generate appropriate conv command enter [...] to zoom in on such a subterm and rewrite it as user desires.

Imagined workflow would be that you right click on a subterm and get a menu of potentially operations: simplify, expand, together etc.

[Johan Commelin]

@Tomas Skrivan That's certainly part of what the widget framework should accomplish. In Lean 3 there was never widget support for conv, but I'm pretty sure it is on @Edward Ayers's radar for Lean 4.

[Sebastian Ullrich]

Tomas Skrivan said:

In particular, I would like to generate appropriate conv command enter [...] to zoom in on such a subterm and rewrite it as user desires.

This is exactly what one of @Jakob von Raumer's students is working on right now, so... stay tuned!

[Sebastian Ullrich]

That is, for VS Code (and possibly lean.nvim). No attempts to port widgets to lean4-mode have been made yet.

[Tomas Skrivan]

That is amazing! Looking forward trying it out.

[Miguel Marco]

I have hacked a proof of concept for lean3:

https://github.com/miguelmarco/leankernel

It works but may be fragile.

My main problem is that the jupyter notebook paradigm requires a "clear state" in the backend when the answer is given, whereas the lean server works ayncronously. So the jupyter kernel might think that the lean server has finished processing the last request, answer to the frontend, and then some more messages from the lean server might arrive. The heuristic I use for this is to wait for a is_running:Falsemessage, and then wait 0.5 seconds without new messages. This introduces a slowdown in the user experience.

Is there a way to ask the lean server if it is really done processing all the previous requests?

[Ziyu Zhou]

Miguel Marco said:

I have hacked a proof of concept for lean3:

https://github.com/miguelmarco/leankernel

It works but may be fragile.

My main problem is that the jupyter notebook paradigm requires a "clear state" in the backend when the answer is given, whereas the lean server works ayncronously. So the jupyter kernel might think that the lean server has finished processing the last request, answer to the frontend, and then some more messages from the lean server might arrive. The heuristic I use for this is to wait for a is_running:Falsemessage, and then wait 0.5 seconds without new messages. This introduces a slowdown in the user experience.

Is there a way to ask the lean server if it is really done processing all the previous requests?

I tried to install your leankernel on windows10 and ubuntu22.04, but both of them didn't work. I think I followed the Readme.md every step of the way. May I ask for a detailed installation tutorial?

[Mauricio Collares]

Did you get an error message?

[Ziyu Zhou]

Mauricio Collares said:

Did you get an error message?

It prompts: Failed to start the Kernel. Jupyter log:
image.png

[Ziyu Zhou]

There must be something wrong with my installation process, but I cannot check it out. If you could give me an example of a proper installation, especially the environment variable configuration information, I'd appreciate it.

[Miguel Marco]

Sorry for not answering before. I didn't see the message.

From what I see, you use conda installation, right?

I am not familiar with that kind of environments. Maybe there is a specific way to install python packages there?

[Ziyu Zhou]

Actually I used ''pip install .''

I'm not very familiar with how jupyter kernel works, and it's hard for me to make a reasonable guess as to what went wrong with my installation process. A more detailed installation tutorial may be helpful. Thank you!

[Miguel Marco]

Sorry again for the delay. Since I finally got some free time, i have taken a look again at this project, and found that it was indeed a problem in the code as it has been published.

I will try to improve it. Will let you know when it is done.

[Miguel Marco]

In the meantime, you can try to edit the kernel.json file to make it look like this:

{"argv":["python3" ,"-m" , "leankernel.leankernel", "-f", "{connection_file}"],
 "display_name":"Lean",
 "language": "lean",
"env" : {
    "LEAN_MEMORY" : "4096",
    "LEAN_TIME"  : "100000",
    "LEAN_BINARY"  : "YOUR_LEAN_BINARY,
    "LEAN_PATHFILES" : "YOUR_PATH_TO_LEAN_FILES"
 }
}

[Miguel Marco]

I made some updates, the installation process should be a bit more solid now, and hopefully the documentation will be a bit more clear.

I am still not sure about a good workflow, but may consider using it for teaching, since we already use a jupyter server for other courses. In that setting, the possibility of having richer text explanations, with proper latex typesetting might help the students.

[Miguel Marco]

example.gif
This is the kind of workflow i had in mind.

[Newell Jensen]

This has probably already been asked but does this work in vs code?

[Newell Jensen]

Looks very promising.

[Max Nowak 🐉]

Doesn't VSCode also have its own "notebook" support, without the need to touch Jupyter at all?

[Max Nowak 🐉]

This looks super cool either way tho :o

[Miguel Marco]

Newell Jensen said:

This has probably already been asked but does this work in vs code?

It can be used by any system that supports the jupyter kernel protocol. I think there is a VS code plugin for that, so technically it could be used. But I think in VScode it makes more sense to stick with the usual asyncronous workflow.