lean web editor slow

Stream: general

[Huỳnh Trần Khanh]

why is the lean web editor slow? as a programmer i want to make a faster version of the lean web editor... but i want to know the reason why it's slow first. could anyone give me pointers, thanks in advance

[Johan Commelin]

How much does one generally expect performance to decrease when running something in the browser via WASM?

[Huỳnh Trần Khanh]

my guess is not significant unless the application is multithreaded or relies heavily on SIMD, as these are the features that WASM doesn't support. otherwise, WASM is pretty close to the hardware and I don't think it imposes much overhead

[Johan Commelin]

Aah, is multithreading an issue?

[Johan Commelin]

Because Lean is using that a lot.

[Eric Wieser]

I would imagine it is also slow (at startup) because it presumably has to download mathlib oleans?

[Mario Carneiro]

An easy way to address that is to provide some user feedback about the download, so that it doesn't just look like lean startup time

[Gabriel Ebner]

The startup time is an issue no matter whether it's downloading, wasm compilation, or lean runtime. Adding a more informative progress message is a good thing, but doesn't fix the issue.

[Johan Commelin]

If we have a per-file olean cache, then the downloading could be done on-demand

[Johan Commelin]

which helps if you only want to do some demlo with ℕ

[Johan Commelin]

but if you start with import kitchen.sink you're still stuck of course

[Eric Wieser]

Storing the olean cache in the browser somewhere might help, but only if we make the online editor slower at updating mathlib

[Eric Wieser]

I find gitpod to feel much faster than our own in-browser version, likely as that's not really running in a browser in the first place, but instead being streamed to one.

[Kevin Buzzard]

I am using links to the community web editor in teaching resources such as this one (see "links for the impatient"). Is there a way to instead link to some gitpoddery?

[Bryan Gin-ge Chen]

In fact the community lean web editor does store the olean cache in the browser's IndexedDB, but since we update the oleans once a day, it doesn't help people who only use the web editor occasionally...

[Gabriel Ebner]

I believe @Chris Lovett is thinking about working on a live editor version that works more like gitpod, where Lean is run a VM in the cloud.

[Kevin Buzzard]

I ask because I just import tactic at the top of every file, which is the proverbial kitchen sink import (I don't need to for the first couple of problem sheets, but we get onto rintro pretty quickly and I like the idea of a one size fits all import for tactics rather than importing some of them and then later having to import more as we get to ring etc)

[Bryan Gin-ge Chen]

I suspect that an olean cache that supports just import tactic would be fairly small, but the web editor doesn't have great support at the moment for switching between different types of caches.

[Eric Wieser]

Kevin Buzzard said:

I am using links to the community web editor in teaching resources such as this one (see "links for the impatient"). Is there a way to instead link to some gitpoddery?

Sure, https://gitpod.io/#https://github.com/ImperialCollegeLondon/M40001_lean

[Kevin Buzzard]

then they have to log into something?

[Eric Wieser]

Yes, just github I think

[Eric Wieser]

But bear in mind that gitpod has a usage quota (50 hours/month) unless:

• you pay money
• you convince them you are a professional open source developer

The mathlib maintainers and probably most of the active contributors could quite easily argue this second point (I did), but I doubt your students can.

[Kevin Buzzard]

and I have no infoview :-/

[Eric Wieser]

Oh, I think there's some setup too

[Eric Wieser]

Add this file to your repo:

https://github.com/leanprover-community/mathlib/blob/master/.gitpod.yml

[Bryan Gin-ge Chen]

Looks like that refers to stuff in mathlib's .docker/ too.

[Eric Wieser]

Good point

[Eric Wieser]

Then you want

image: leanprovercommunity/mathlib:gitpod

vscode:
  extensions:
    - jroesch.lean

tasks:
  - command: . /home/gitpod/.profile && leanpkg configure && leanproject get-cache --fallback=download-all

[Kevin Buzzard]

or maybe get-mathlib-cache

[Eric Wieser]

https://github.com/ImperialCollegeLondon/M40001_lean/pull/3

[Eric Wieser]

Oh, good point

[Eric Wieser]

Since this isn't mathlib

[Kevin Buzzard]

and this will be as slow as the web editor presumably, if it's getting all the oleans

[Bryan Gin-ge Chen]

It'd be good if this info was somewhere on the community website. Maybe here though it's not about CI.

[Eric Wieser]

It downloads them in a VM somewhere that's quite speedy and probably has a faster connection to azure

[Eric Wieser]

(I think it can be quite slow when used for the very first time by anyone)

[Kevin Buzzard]

and what happens when I do that trick where I can wipe a hard drive using a malicious Lean file? The idea is that it's just some VM presumably?

[Kevin Buzzard]

I have an infoview! Thanks Eric and everyone! It was much slower than the web editor but I guess I don't have to now wait again when I switch sheets :D

[Eric Wieser]

Weird, the mathlib one seemed to start faster than yours does

[Yaël Dillies]

Eric Wieser said:

The mathlib maintainers and probably most of the active contributors could quite easily argue this second point

Oh, you think I can?

[Eric Wieser]

Worth a try for sure

[Eric Wieser]

https://www.gitpod.io/docs/professional-open-source

[Yaël Dillies]

WIll give it a try then!

[Eric Wieser]

In the last 6 months you're the 3rd most active contributor so I think it's fair to claim you're a "core contributor"

[Yaël Dillies]

Oh what. I knew I had done quite a lot but not that much!

[Yaël Dillies]

Funnily, I am the third according to each metric.

[Ryan Lahfa]

FWIW, I have been trying to recompile many versions of Lean for emscripten and x86_64 in Nix for caching purpose, I have been doing it using emscripten v2+ which is supposedly a lot faster in terms of result than emscripten v1 (which the current Lean uses in its CI), this might induce a nice performance boost. I have also some patchs to detect when oleans are not provided and logging it in the JavaScript console.

It compiles quite well now: https://github.com/RaitoBezarius/nixexprs/actions/runs/1403562933 (using patched versions of Lean 3 source, patched versions of some JS libs and a very recent emscripten from upstream which included a patch for Nix).

Web editors can be built directly from Nix (external libraries like mathlib or whatever are more or less supported using FOD derivations).

[Bryan Gin-ge Chen]

If you don't mind making a PR to leanprover-community/lean with your improvements I'd be happy to take a look!

[Ryan Lahfa]

Bryan Gin-ge Chen said:

If you don't mind making a PR to leanprover-community/lean with your improvements I'd be happy to take a look!

I'd be definitely happy to do it, most of the patch to Lean is there: https://github.com/RaitoBezarius/nixexprs/blob/master/pkgs/science/lean/0001-cmake-emscripten-update-build-flags-for-emscripten-2.patch

But that's emscripten v2 specific I think and it will not behave well with the current CI, so my plan is to get something stable on my infrastructure, slowly collecting feedback by using it (I'd like to make it easy to deploy Lean games with recent Lean / recent mathlib versions) and then make the switch on the Lean community CI if that makes sense as @Gabriel Ebner seems to be the code owner of that part.

[Bryan Gin-ge Chen]

(I did some work on the emscripten CI as well, but I agree that Gabriel's feedback would be much appreciated!)

[Ryan Lahfa]

Bryan Gin-ge Chen said:

(I did some work on the emscripten CI as well, but I agree that Gabriel's feedback would be much appreciated!)

(You're right, I have been seeing your work too!)

[Ryan Lahfa]

But I'd like to improve a bit the lean-client-js-browser lib so I will be in your hands regarding this matter :)

[Ryan Lahfa]

Also, open question but is the model where we use a binary Lean on the backend and expose it over an API, and, we send sync commands and all through the network and the frontend is only Monaco + some thin client API layer, something that was considered? I guess it was excluded for security reasons, but if we could have more or less safe sandboxes (à la Gitpod in fact), that would be something people would use right?

[Bryan Gin-ge Chen]

I think it would definitely be used since it would likely be much faster to load. Assuming it gets set up then some questions to consider are how hard is it to maintain, and how much does it cost?

[Huỳnh Trần Khanh]

yeah and also could we make the web editor work on mobile? is it possible

[Bryan Gin-ge Chen]

I haven't thought about this in probably more than a year, but my recollection is that to get the web editor working on mobile, we would have to port the editor from Monaco to something like Codemirror 6 since Monaco was (is?) not so great with touchscreens.

[Gabriel Ebner]

But that's emscripten v2 specific I think and it will not behave well with the current CI, so my plan is to get something stable on my infrastructure, slowly collecting feedback by using it (I'd like to make it easy to deploy Lean games with recent Lean / recent mathlib versions) and then make the switch on the Lean community CI if that makes sense [...]

Feel free to submit PRs! Changing the emscripten build to use nix is fine with me as well if you'd prefer that.

[Ryan Lahfa]

Gabriel Ebner said:

But that's emscripten v2 specific I think and it will not behave well with the current CI, so my plan is to get something stable on my infrastructure, slowly collecting feedback by using it (I'd like to make it easy to deploy Lean games with recent Lean / recent mathlib versions) and then make the switch on the Lean community CI if that makes sense [...]

Feel free to submit PRs! Changing the emscripten build to use nix is fine with me as well if you'd prefer that.

I will definitely do so! Only some oleans not being picked up debugging is left, and I'm afraid this has to do with timestamps (as Nix enforces UNIX timestamp 0), once this gets solved: deploying lean games web bundles might be as simple as this:

https://github.com/RaitoBezarius/nixexprs/blob/master/pkgs/science/lean/lean-games/nng.nix