Web editor not working

Stream: general

[Eric Wieser]

As a heads up, the bump to Lean 3.51 has broken the web editor. I've found two of the problems:

• https://github.com/leanprover-community/lean/pull/808. You can apply this manually by adding another breakpoint at the second error, and running this.ERRNO_CODES = {}.
• https://github.com/leanprover/lean-client-js/pull/58. You can apply this manually by sticking a breakpoint at the line where the first error occurs, and running Module.FS.createFolder = Module.FS.createPath.

With these applied, it now complains that it can't find library/init/default.lean; indeed, the filesystem only haslibrary/init/default.olean (you can test with Module.FS.lookupPath('/library/init/default.olean')

[Eric Wieser]

(Lean 3.51 also included a bump to the emscripten build tools, because the old one didn't run any more)

[Eric Wieser]

@Bryan Gin-ge Chen, do you have any suggestions of what to look at next?

[Eric Wieser]

This comment suggests that the web editor should not need the .leans, and indeed Lean was modified long ago

[Eric Wieser]

Ah nevermind, setting ERRNO_CODES to the right value makes everything work. So merging the above two PRs (and bumping mathlib again) is a solution.

[Kevin Buzzard]

Thanks for the debugging! There are still people who use this old interface.

[Eric Wieser]

Unfortunately this creates a bunch of release work for @Gabriel Ebner...

[Bryan Gin-ge Chen]

If Gabriel is busy, I can try to put together a new release of Lean later today.

[Bryan Gin-ge Chen]

Lean 3.51.1c, which includes this fix, has just been released. Thanks to Eric for tracking this down!

[Eric Wieser]

#19088 bumps mathlib

[Eric Wieser]

Thanks for making the release! We'll need to release lean-client-js too, though the PR there has a bit of bike-shedding wiggle room that's easier to explore once the mathlib build is out

[Eric Wieser]

Eric Wieser said:

#19088 bumps mathlib

I took the liberty of sending this to bors without review, since it's a one character change; I'm pretty sure I made it correctly, and there's nothing else on the queue for it to hold up right now

[Eric Wieser]

I can confirm that with https://github.com/leanprover/lean-client-js/pull/58 applied manually, the web editor works again; though that still need to be merged and released.

[Eric Wieser]

@Gabriel Ebner, am I right in saying you both the only person who knows how to release this, and the only person (other than Leo?) with sufficient github permissions to merge that PR?

[Eric Wieser]

There's some unrelated cleanup in CI, but (edit: no longer) the web editor seems to be working again!