Zulip Chat Archive

Stream: general

Topic: community lean web editor


Bryan Gin-ge Chen (Aug 17 2022 at 16:33):

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 (Aug 17 2022 at 16:34):

100 MB :scared:

Eric Wieser (Aug 17 2022 at 16:43):

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

Eric Wieser (Aug 17 2022 at 16:43):

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

Eric Wieser (Aug 17 2022 at 16:43):

Because that avoids ever actually commiting large binaries into git

Bryan Gin-ge Chen (Aug 17 2022 at 16:47):

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

Patrick Massot (Aug 17 2022 at 16:47):

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 (Aug 17 2022 at 16:53):

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

Eric Wieser (Aug 17 2022 at 16:53):

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

Jireh Loreaux (Aug 17 2022 at 17:03):

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

Eric Wieser (Aug 17 2022 at 17:04):

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 (Aug 17 2022 at 17:04):

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 (Aug 17 2022 at 17:06):

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

Eric Wieser (Aug 17 2022 at 17:14):

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

Luis Castillo (Aug 17 2022 at 17:25):

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 (Aug 17 2022 at 18:15):

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 (Aug 17 2022 at 18:19):

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 (Aug 17 2022 at 18:23):

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 (Aug 18 2022 at 23:33):

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 (Sep 12 2022 at 23:28):

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

Matt Diamond (Sep 12 2022 at 23:34):

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

Matt Diamond (Sep 12 2022 at 23:35):

like could you just .gitignore and remove it?

Bryan Gin-ge Chen (Sep 12 2022 at 23:43):

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 (Sep 12 2022 at 23:46):

ah I see

Matt Diamond (Sep 12 2022 at 23:50):

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 (Sep 12 2022 at 23:54):

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 (Sep 13 2022 at 00:01):

(deleted)

Bryan Gin-ge Chen (Sep 13 2022 at 00:07):

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

Bryan Gin-ge Chen (Sep 13 2022 at 00:09):

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 (Sep 13 2022 at 00:15):

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 (Sep 13 2022 at 00:16):

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 (Sep 13 2022 at 00:16):

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 (Sep 13 2022 at 00:19):

ah darn

Matt Diamond (Sep 13 2022 at 00:20):

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 (Sep 13 2022 at 00:22):

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

Eric Wieser (Sep 13 2022 at 06:33):

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

Eric Wieser (Sep 13 2022 at 06:34):

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

Eric Wieser (Nov 13 2022 at 18:12):

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

Eric Wieser (Nov 13 2022 at 18:13):

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 (Nov 13 2022 at 18:15):

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

Eric Wieser (Nov 13 2022 at 18:17):

I think we might even be safe up to 5GB

Eric Wieser (May 05 2023 at 14:41):

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


Last updated: Dec 20 2023 at 11:08 UTC