## Stream: general

### Topic: Lean + Observable notebooks

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

#### Andrew Ashworth (Jul 28 2019 at 21:10):

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

#### Scott Morrison (Jul 28 2019 at 21:19):

This is really cool!

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

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

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

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

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

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

#### Johan Commelin (Jul 31 2019 at 18:17):

Whoah! That's really wicked! Well done.

#### Johan Commelin (Jul 31 2019 at 18:18):

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

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

#### 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:

#### Kevin Kappelmann (Jul 31 2019 at 19:18):

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

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

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

#### Bryan Gin-ge Chen (Jul 31 2019 at 19:29):

Maybe this post will clarify things.

#### Kevin Kappelmann (Jul 31 2019 at 19:32):

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

#### Bryan Gin-ge Chen (Jul 31 2019 at 19:33):

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

#### Kevin Kappelmann (Jul 31 2019 at 21:21):

I most certainly will - thanks! :)

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

Nice!

#### 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)?

#### Kevin Kappelmann (Aug 23 2019 at 15:00):

It is fully interactive

#### Patrick Massot (Aug 23 2019 at 15:00):

How do you interact?

#### Kevin Kappelmann (Aug 23 2019 at 15:01):

You can use the Lean editor below the proof view

#### 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}})


#### Patrick Massot (Aug 23 2019 at 15:03):

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

#### Patrick Massot (Aug 23 2019 at 15:04):

It looks very promising anyway.

#### 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

#### 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

#### 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

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

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

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

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

#### Yufan Lou (Sep 30 2019 at 17:06):

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

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

#### Yufan Lou (Sep 30 2019 at 17:08):

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
starting lean... 9aa8d4b2-493f-404a-802d-bd2bf573409f:8:48228


#### Bryan Gin-ge Chen (Sep 30 2019 at 17:10):

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

#### Bryan Gin-ge Chen (Sep 30 2019 at 17:11):

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

#### Yufan Lou (Sep 30 2019 at 17:11):

lol it took a looooong time

#### Yufan Lou (Sep 30 2019 at 17:12):

I guess it was just slow on cold boot

#### 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!

#### 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
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 (Sep 30 2019 at 17:25):

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

#### 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

#### Yufan Lou (Oct 01 2019 at 19:44):

Ah, the TypeError disappeared.

#### 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!

#### 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