community lean web editor

Stream: general

[Bryan Gin-ge Chen]

It seems that mathlib has finally gotten too large for the current community web editor setup, so updates will be paused for a few days / weeks until I or someone else has the time to figure out something new. Sorry for any issues this may cause!

The details: Currently the web editor is hosted on GitHub pages and the file containing the oleans (library.zip) file has just exceeded the 100MB limit and so the build is failing. In the short term, it hopefully shouldn't be too hard to push that file to Azure or somewhere else instead, but at some point forcing web editor users to download such large ZIP files won't work either...

[Johan Commelin]

100 MB :scared:

[Eric Wieser]

cc @Luis Castillo who was PM'ing me about this same problem in a lean game maker website.

[Eric Wieser]

We think that the new github pages workflow might solve this problem

[Eric Wieser]

Because that avoids ever actually commiting large binaries into git

[Bryan Gin-ge Chen]

Great! I'm not familiar with that workflow but let me know if there's something I can help with.

[Patrick Massot]

In the game maker context you shouldn't need all of mathlib. For instance Luis's game uses only import tactic from mathlib...

[Eric Wieser]

The new workflow seems to work (https://github.com/luisscastillo/lean-game/actions/runs/2876925259)

[Eric Wieser]

So I guess we need to do the same thing for the web editor

[Jireh Loreaux]

FYI: I get errors here: https://luisscastillo.github.io/lean-game/?world=2&level=1

[Eric Wieser]

Where's the CI that handles the web editor? https://github.com/leanprover-community/lean-web-editor/tree/gh-pages hasn't been deployed to since travis times

[Bryan Gin-ge Chen]

Should be in here: https://github.com/leanprover-community/lean-web-editor/blob/master/.github/workflows/build.yml

There are still some old hacks in there for my Observable notebooks which I'm OK with us removing.

[Eric Wieser]

Maybe what I meant to ask about is where it is being deployed to?

[Eric Wieser]

Aha, it goes to https://github.com/bryangingechen/lean-web-editor-dist it seems

[Luis Castillo]

Jireh Loreaux ha dicho:

FYI: I get errors here: https://luisscastillo.github.io/lean-game/?world=2&level=1

These import errors are present from Level 5 of Tutorial World onwards. They don't depend neither on the deployment of the game nor on the size of the files. So you can adapt my .yml file without problems if you meant that errors :+1:

[Kyle Miller]

If it's not already being done (and if there is any such data), is it possible to strip the oleans of any data that isn't necessary for the web editor?

It might also be nice to work out how to chunk the library so that only a subset is dynamically downloaded. (I remember seeing a neat demonstration of using sqlite online with a large database on the server, and the javascript client is able to request specific chunks to evaluate sql queries.)

[Ruben Van de Velde]

Hardly a long term fix, but is it possible to use higher compression settings when generating the zip or use another archive format?

[Eric Wieser]

Changing to a different deployment strategy should make the problem go away, I just don't understand the build system enough to make the change. I'd hope @Bryan Gin-ge Chen can work it out, assuming they know how the current system works

[Matt Diamond]

While we're on this topic, I had a feature request: it would be nice if there was an option to disable the automatic checking until a button is manually clicked. Ideally there would be some indication that the editor is in an unchecked state (maybe a gray bar at the top instead of green).

I just feel like the web editor gets very slow when it keeps trying to check incomplete iterations of your work.

[Matt Diamond]

@Bryan Gin-ge Chen How does the Lean website use library.zip? Is that unpacked in the deploy process?

[Matt Diamond]

I'm wondering if it needs to be in version control at all

[Matt Diamond]

like could you just .gitignore and remove it?

[Bryan Gin-ge Chen]

The website is hosted on GitHub pages, so all the files that end up deployed need to be in a branch in the repo, unfortunately.

library.zip is used directly by the wasm version of Lean (it's been ages since I've looked at this, but I think the juicy bits are around here).

[Matt Diamond]

ah I see

[Matt Diamond]

the workflow that @Eric Wieser linked to uses actions/upload-pages-artifact to upload everything, so perhaps moving the deploy script fully into the workflow and using that action could get around the problem?

[Matt Diamond]

I've got some spare time, perhaps I can look into it? would be nice to have the web editor up to date

[Matt Diamond]

(deleted)

[Bryan Gin-ge Chen]

Sure, I'd appreciate the help! Feel free to ask if you've got any questions!

[Bryan Gin-ge Chen]

Though I think the key part of what Eric is suggesting is moving from GitHub pages to another host which is more flexible with file sizes.

[Matt Diamond]

I'm not sure... the deploy thing he linked to really just seemed to use a different way for uploading files to Github Pages

you can see the key workflow steps here: https://github.com/luisscastillo/lean-game/blob/36ffe2fd06b1fe00d93e25d3b233dc9f0b6b8d48/.github/workflows/euclidgame.yml#L94-L110

and this looks similar to the files in lean-web-editor-dist:
image.png

[Matt Diamond]

so it's really about deploying to Pages in a different way, not switching to a different host (or at least that's how it came across to me)

[Bryan Gin-ge Chen]

I see, if that's the case then I don't think we'll be able to get around the underlying issue which is that GitHub repos aren't allowed to have files > 100 MB: https://docs.github.com/en/repositories/working-with-files/managing-large-files/about-large-files-on-github#file-size-limits

[Matt Diamond]

ah darn

[Matt Diamond]

perhaps we could try Git Large File Storage? I think it may be free (but I haven't really investigated it that deeply)

[Matt Diamond]

ah nvm, GitHub Pages doesn't support LFS... I give up, heh

[Eric Wieser]

I think that my earlier suggestion should get around the large file limit

[Eric Wieser]

Because the new method doesn't store the content in a git repo

[Eric Wieser]

The lean web editor is now running Lean 3.49.0 and the latest mathlib!

[Eric Wieser]

Eric Wieser said:

I think that my earlier suggestion should get around the large file limit

This did indeed solve the problem

[Bryan Gin-ge Chen]

Thanks Eric! I think this should be fine until we hit 1GB...

[Eric Wieser]

I think we might even be safe up to 5GB

[Eric Wieser]

Turns out the web editor stopped updating due to inactivity four months ago; I've restarted the CI so we should have the latest mathlib for another 3 months