Zulip Chat Archive

Stream: general

Topic: lean web editor slow


Huỳnh Trần Khanh (Oct 28 2021 at 11:01):

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 (Oct 28 2021 at 11:02):

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

Huỳnh Trần Khanh (Oct 28 2021 at 11:04):

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 (Oct 28 2021 at 11:04):

Aah, is multithreading an issue?

Johan Commelin (Oct 28 2021 at 11:04):

Because Lean is using that a lot.

Eric Wieser (Oct 28 2021 at 11:12):

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

Mario Carneiro (Oct 28 2021 at 15:31):

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 (Oct 28 2021 at 15:35):

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 (Oct 28 2021 at 15:39):

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

Johan Commelin (Oct 28 2021 at 15:40):

which helps if you only want to do some demlo with

Johan Commelin (Oct 28 2021 at 15:41):

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

Eric Wieser (Oct 28 2021 at 15:46):

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

Eric Wieser (Oct 28 2021 at 15:46):

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 (Oct 28 2021 at 15:52):

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 (Oct 28 2021 at 15:52):

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 (Oct 28 2021 at 15:53):

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 (Oct 28 2021 at 15:53):

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 (Oct 28 2021 at 15:55):

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 (Oct 28 2021 at 15:56):

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 (Oct 28 2021 at 15:57):

then they have to log into something?

Eric Wieser (Oct 28 2021 at 15:57):

Yes, just github I think

Eric Wieser (Oct 28 2021 at 15:57):

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 (Oct 28 2021 at 15:58):

and I have no infoview :-/

Eric Wieser (Oct 28 2021 at 15:58):

Oh, I think there's some setup too

Eric Wieser (Oct 28 2021 at 15:59):

Add this file to your repo:

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

Bryan Gin-ge Chen (Oct 28 2021 at 15:59):

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

Eric Wieser (Oct 28 2021 at 16:00):

Good point

Eric Wieser (Oct 28 2021 at 16:00):

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 (Oct 28 2021 at 16:00):

or maybe get-mathlib-cache

Eric Wieser (Oct 28 2021 at 16:01):

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

Eric Wieser (Oct 28 2021 at 16:01):

Oh, good point

Eric Wieser (Oct 28 2021 at 16:01):

Since this isn't mathlib

Kevin Buzzard (Oct 28 2021 at 16:01):

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

Bryan Gin-ge Chen (Oct 28 2021 at 16:02):

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

Eric Wieser (Oct 28 2021 at 16:02):

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

Eric Wieser (Oct 28 2021 at 16:03):

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

Kevin Buzzard (Oct 28 2021 at 16:05):

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 (Oct 28 2021 at 16:06):

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 (Oct 28 2021 at 16:08):

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

Yaël Dillies (Oct 28 2021 at 16:09):

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 (Oct 28 2021 at 16:09):

Worth a try for sure

Eric Wieser (Oct 28 2021 at 16:09):

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

Yaël Dillies (Oct 28 2021 at 16:09):

WIll give it a try then!

Eric Wieser (Oct 28 2021 at 16:11):

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 (Oct 28 2021 at 16:13):

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

Yaël Dillies (Oct 28 2021 at 16:13):

Funnily, I am the third according to each metric.

Ryan Lahfa (Oct 31 2021 at 14:38):

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 (Oct 31 2021 at 14:41):

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 (Oct 31 2021 at 14:42):

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 (Oct 31 2021 at 14:43):

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

Ryan Lahfa (Oct 31 2021 at 14:44):

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 (Oct 31 2021 at 14:45):

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 (Oct 31 2021 at 14:47):

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 (Oct 31 2021 at 14:53):

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 (Oct 31 2021 at 17:43):

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

Bryan Gin-ge Chen (Oct 31 2021 at 19:08):

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 (Nov 01 2021 at 08:58):

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 (Nov 01 2021 at 12:09):

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


Last updated: Aug 03 2023 at 10:10 UTC