Zulip Chat Archive

Stream: general

Topic: Lean + Observable notebooks


view this post on Zulip Bryan Gin-ge Chen (Jul 28 2019 at 20:48):

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.

view this post on Zulip Andrew Ashworth (Jul 28 2019 at 21:10):

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

view this post on Zulip Scott Morrison (Jul 28 2019 at 21:19):

This is really cool!

view this post on Zulip Andrew Ashworth (Jul 28 2019 at 21:21):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 28 2019 at 21:25):

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.

view this post on Zulip Andrew Ashworth (Jul 28 2019 at 21:32):

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.

view this post on Zulip Yao Liu (Jul 29 2019 at 15:06):

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.

view this post on Zulip Bryan Gin-ge Chen (Jul 29 2019 at 15:28):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 31 2019 at 18:14):

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.

view this post on Zulip Johan Commelin (Jul 31 2019 at 18:17):

Whoah! That's really wicked! Well done.

view this post on Zulip Johan Commelin (Jul 31 2019 at 18:18):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 31 2019 at 18:28):

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.

view this post on Zulip Kevin Kappelmann (Jul 31 2019 at 19:11):

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:

view this post on Zulip Kevin Kappelmann (Jul 31 2019 at 19:18):

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

view this post on Zulip Kevin Kappelmann (Jul 31 2019 at 19:22):

@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?

view this post on Zulip Bryan Gin-ge Chen (Jul 31 2019 at 19:28):

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.

view this post on Zulip Bryan Gin-ge Chen (Jul 31 2019 at 19:29):

Maybe this post will clarify things.

view this post on Zulip Kevin Kappelmann (Jul 31 2019 at 19:32):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 31 2019 at 19:33):

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

view this post on Zulip Kevin Kappelmann (Jul 31 2019 at 21:21):

I most certainly will - thanks! :)

view this post on Zulip Kevin Kappelmann (Aug 23 2019 at 14:55):

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

view this post on Zulip Patrick Massot (Aug 23 2019 at 14:58):

Nice!

view this post on Zulip Patrick Massot (Aug 23 2019 at 14:59):

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

view this post on Zulip Kevin Kappelmann (Aug 23 2019 at 15:00):

It is fully interactive

view this post on Zulip Patrick Massot (Aug 23 2019 at 15:00):

How do you interact?

view this post on Zulip Kevin Kappelmann (Aug 23 2019 at 15:01):

You can use the Lean editor below the proof view

view this post on Zulip Kevin Kappelmann (Aug 23 2019 at 15:01):

or you can change the proof view command to

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

view this post on Zulip Patrick Massot (Aug 23 2019 at 15:03):

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

view this post on Zulip Patrick Massot (Aug 23 2019 at 15:04):

It looks very promising anyway.

view this post on Zulip Kevin Kappelmann (Aug 23 2019 at 15:05):

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

view this post on Zulip Patrick Massot (Aug 23 2019 at 15:05):

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

view this post on Zulip Patrick Massot (Aug 23 2019 at 15:07):

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

view this post on Zulip Kevin Kappelmann (Aug 23 2019 at 15:08):

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

view this post on Zulip Patrick Massot (Aug 23 2019 at 15:08):

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

view this post on Zulip Yufan Lou (Sep 30 2019 at 17:03):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 30 2019 at 17:04):

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

view this post on Zulip Yufan Lou (Sep 30 2019 at 17:06):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 30 2019 at 17:07):

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?

view this post on Zulip Yufan Lou (Sep 30 2019 at 17:08):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 30 2019 at 17:10):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 30 2019 at 17:11):

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

view this post on Zulip Yufan Lou (Sep 30 2019 at 17:11):

lol it took a looooong time

view this post on Zulip Yufan Lou (Sep 30 2019 at 17:11):

but i loaded it

view this post on Zulip Yufan Lou (Sep 30 2019 at 17:12):

I guess it was just slow on cold boot

view this post on Zulip Bryan Gin-ge Chen (Sep 30 2019 at 17:16):

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!

view this post on Zulip Yufan Lou (Sep 30 2019 at 17:22):

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

view this post on Zulip Yufan Lou (Sep 30 2019 at 17:25):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 30 2019 at 17:28):

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

view this post on Zulip Yufan Lou (Oct 01 2019 at 19:44):

Ah, the TypeError disappeared.

view this post on Zulip Bryan Gin-ge Chen (Oct 01 2019 at 19:47):

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!

view this post on Zulip Yufan Lou (Oct 02 2019 at 00:07):

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


Last updated: May 14 2021 at 00:42 UTC