Lean + Observable notebooks

Stream: general

[Bryan Gin-ge Chen]

I've been playing around with displaying and interacting with Lean files on the web using "Observable notebooks" recently. See this page for a demonstration:

https://observablehq.com/@bryangingechen/fibonacci-formalized-1-some-sums

Basically, the notebook displays some simple Lean code in several embedded Lean editors with lots of markdown / LaTeX explanation around them. You can click to the left of any of the "cells" to see their Javascript source code. You can write and edit notebooks like this directly in your browser if you create a free account on observablehq.com by e.g. signing in with Github.

One feature I rigged into the Lean editor cells is that they pass their messages from the Lean server back to Javascript. Since Observable notebooks work like spreadsheets, I could make "Lean-driven" graphics like the ones in the following notebook:

https://observablehq.com/@bryangingechen/fibonacci-formalized-2-bees-and-cars

Try changing the numbers in the #eval statements in the editors above the family tree graphic and the car configuration graphic and seeing how they change. (Don't make them too large or else browser Lean will run out of memory).

It'd be interesting to see what else this could be used for!

I wrote a little bit more about Observable notebooks and how you can write notebooks like these at the end of the first notebook above, but feel free to ask here if you have any questions.

[Andrew Ashworth]

I haven't seen anyone do anything except D3 visualizations on Observable. This is great!

[Scott Morrison]

This is really cool!

[Andrew Ashworth]

I love reading interactive notebook explanations; I still look at Peter Norvig's Jupyter notebooks from time to time for reference.

[Bryan Gin-ge Chen]

Thanks, glad you guys like it! I'm hoping other folks will try out writing some notebooks with Lean. I'm sure the code I wrote could be improved so I'm looking forward to feedback.

[Andrew Ashworth]

I might give it a shot in the next couple weeks. I'm mostly a Jupyter person since I like to program in languages that don't have a native WASM backend like Lean, so this is incentive to figure out how ObservableHQ works.

[Yao Liu]

Great! I'll see if I can learn some basics of Lean this way. I love Observable for the ability to easily write in LaTeX. For suggestions, as much as I like to write long posts to explain, Observable is at its best for smallish notebook so people could fork out and tinker with (and also making PR). I recall Kevin's suggestion for math people was to start off by reading definitions and statements, not the proofs, of interesting theorems, to get familiar with the syntax. Fibonacci stuff is as good as any.

[Bryan Gin-ge Chen]

Yeah, point taken about the long notebooks. In fact, Fibonacci parts 1 and 2 were actually originally one super-long notebook.

[Bryan Gin-ge Chen]

It's now possible to use Lean running on your computer as a backend to the Lean editors on Observable!

https://observablehq.com/@bryangingechen/lean-websocketd

In short, websocketd makes it really convenient to turn any program that reads from stdin and writes to stdout to a local webserver, so I wrote a little bit of code to replace the connection to Emscripten Lean with a connection to that server.

Using this, you can play around with Lean in notebooks without being constrained by the various shortcomings of Lean in the browser. For instance, you can import from Lean packages on your computer without having to create and upload some library.zip bundle.

[Johan Commelin]

Whoah! That's really wicked! Well done.

[Johan Commelin]

I guess it also gives some speed up. wasm can only do so much.

[Bryan Gin-ge Chen]

Very true, particularly since it is single-threaded. However, Emscripten Lean does seem to be able to avoid some crashes. Something to do with the way it treats null pointer dereferences I guess.

[Kevin Kappelmann]

It's now possible to use Lean running on your computer as a backend to the Lean editors on Observable!

https://observablehq.com/@bryangingechen/lean-websocketd

In short, websocketd makes it really convenient to turn any program that reads from stdin and writes to stdout to a local webserver, so I wrote a little bit of code to replace the connection to Emscripten Lean with a connection to that server.

Using this, you can play around with Lean in notebooks without being constrained by the various shortcomings of Lean in the browser. For instance, you can import from Lean packages on your computer without having to create and upload some library.zip bundle.

what the... this is insane! :flushed:

[Kevin Kappelmann]

why have I never heard of observablehq?! It's so slick!

[Kevin Kappelmann]

@Bryan Gin-ge Chen On the website, it says Unlimited free viewers for the paid version. Does this mean your notebooks can only be viewed a certain number of times if you don't have a subscription?

[Bryan Gin-ge Chen]

I think that's referring to private team notebooks where you can give out some login keys for other people to view (but not edit). I haven't noticed any restrictions with my free account yet.

[Bryan Gin-ge Chen]

Maybe this post will clarify things.

[Kevin Kappelmann]

Nice! I'll start reading observablehq tutorials then! :)

[Bryan Gin-ge Chen]

Great, feel free to reach out if you have any questions!

[Kevin Kappelmann]

I most certainly will - thanks! :)

[Kevin Kappelmann]

I built an interactive Lean proof view on top of @Bryan Gin-ge Chen's neat work - feel free to check it out and tell me what you like and what you miss :) Its purpose is to interactively compare a standard maths proof and Lean proof, side by side. image (note: first page visit downloads ~20MB of Lean files, so it might take a bit).

[Patrick Massot]

Nice!

[Patrick Massot]

This is read-only Lean, right? So what is the difference with format_lean (apart from slow loading time and dependence on observablehq)?

[Kevin Kappelmann]

It is fully interactive

[Patrick Massot]

How do you interact?

[Kevin Kappelmann]

You can use the Lean editor below the proof view

[Kevin Kappelmann]

or you can change the proof view command to

proofView({proof: sqrtTwoIrrat, invalidation, indexOffset: 1, editorOpts: {readOnly: false}})

[Patrick Massot]

Is it meant to update the top of the page (with step by step proof)?

[Patrick Massot]

It looks very promising anyway.

[Kevin Kappelmann]

Changing the proof in the editor below does not automatically update the step by step proof at the top (there was an attempt to do so, but it's not straightforward). If you want to update the proof at the top, you need to replace the value of sqrtTwoIrrat(just below the step by step proof view) with the new content

[Patrick Massot]

Could you get rid of that awful green, it looks a lot like https://upload.wikimedia.org/wikipedia/commons/7/74/Coq_8.5_stdlib_proof.png which is one of those things from the past that make people not even try Coq and come here instead

[Patrick Massot]

It says "You have 1 unsaved change. Fork this notebook to save." when I try to edit that

[Kevin Kappelmann]

Yep, that means you can now create a fork of my notebook if you want to - just like in git.

[Patrick Massot]

Anyway, I think we need a lighter variation on this in order to display read-only Lean files (something we could host on github.io pages for instances).

[Yufan Lou]

Today I wanted to try to get into this more but found out that all notebooks stopped working on my Firefox. What happened?

[Bryan Gin-ge Chen]

Interesting, they are working for me. Do you mean that every Observable notebook is failing, or just the ones with Lean editors?

[Yufan Lou]

More precisely the notebooks are working, but none of the Lean editors are working.

[Bryan Gin-ge Chen]

In what way precisely do they fail to work? Can you share a screenshot? Do you see any errors in your browser's dev console?

[Yufan Lou]

Screen-Shot-2019-09-30-at-13.07.13.png
log:

Content Security Policy: Couldn’t process unknown directive ‘prefetch-src’
Content Security Policy: The page’s settings blocked the loading of a resource at eval (“script-src”).
Content Security Policy: The page’s settings blocked the loading of a resource at inline (“script-src”). 3 proof-view-designer-template:1:1
resetting open lean files... hello-lean-prover.js:483:11
downloading lean... 9aa8d4b2-493f-404a-802d-bd2bf573409f:8:49093
starting lean... 9aa8d4b2-493f-404a-802d-bd2bf573409f:8:48228

[Bryan Gin-ge Chen]

Ah, OK, the cells aren't loading for me either. @Kevin Kappelmann

Does the editor for this notebook load for you? https://observablehq.com/@kappelmann/lean-proof-view

[Bryan Gin-ge Chen]

Because that one and the notebook that implements the editor both work for me.

[Yufan Lou]

lol it took a looooong time

[Yufan Lou]

but i loaded it

[Yufan Lou]

I guess it was just slow on cold boot

[Bryan Gin-ge Chen]

Hmm. When I refreshed the Proof View Designer Template notebook it loaded quickly, but then I get the message: file '/library/init/default.lean' not found which means that something screwed up the notebook's IndexedDB cache on my end. I'll have to investigate this further.

Glad you got things working though! Feel free to ask here if you run into more trouble!

[Yufan Lou]

https://observablehq.com/@kappelmann/lean-proof-view still doesn't display any of the lean cells.

log:

Content Security Policy: Couldn’t process unknown directive ‘prefetch-src’
Content Security Policy: The page’s settings blocked the loading of a resource at eval (“script-src”).
Content Security Policy: The page’s settings blocked the loading of a resource at inline (“script-src”). 3 lean-proof-view:1:1
resetting open lean files... hello-lean-prover.js:483:11
downloading lean... 2a56e349-1112-a845-b6e5-28d9d8a66f8c:8:49093
TypeError: First argument must be a string, Buffer, ArrayBuffer, Array, or array-like object. 2a56e349-1112-a845-b6e5-28d9d8a66f8c:8:1610
    u blob:https://kappelmann.static.observableusercontent.com/2a56e349-1112-a845-b6e5-28d9d8a66f8c:8
    u blob:https://kappelmann.static.observableusercontent.com/2a56e349-1112-a845-b6e5-28d9d8a66f8c:8
    c blob:https://kappelmann.static.observableusercontent.com/2a56e349-1112-a845-b6e5-28d9d8a66f8c:8
    onsuccess blob:https://kappelmann.static.observableusercontent.com/2a56e349-1112-a845-b6e5-28d9d8a66f8c:8
starting lean... 2a56e349-1112-a845-b6e5-28d9d8a66f8c:8:48228

[Yufan Lou]

https://observablehq.com/@bryangingechen/hello-lean-prover displays everything normally

[Bryan Gin-ge Chen]

Could you try the following:
- navigate to the "Storage" tab in the Firefox dev tools from the lean-proof-view notebook
- click on Indexed DB in the list on the left
- open the https://kappelmann.static.observableusercontent.com entry
- right click and delete the "leanlibrary (default)" entry
- refresh

[Yufan Lou]

Ah, the TypeError disappeared.

[Bryan Gin-ge Chen]

OK, great. I made a small change so that the libraries get loaded more robustly going forward. Do share in this thread if you end up making anything with Observable+Lean!

[Yufan Lou]

I did not have time and I confirmed it loads well now. Thank you! I will!