lean-web-editor

[bryangingechen]

@cipher1024 suggested that I PR my version of the lean-web-editor here.

Thanks to @semorrison for kindly agreeing to host the emscripten files and the zip bundle that the web editor relies on!

[semorrison]

Hi @bryangingechen, could you quickly explain where this will end up deployed?

[bryangingechen]

Sure, I think it should end up at https://leanprover-community.github.io/lean-web-editor

[bryangingechen]

Oh wait, do I need to do something with the jekyll config to get this to work?

edit I guess not. But I realized I forgot to actually link to the web editor from the index page.

[robertylewis]

Thanks! This looks nice. When I test it locally, Lean runs extremely slowly. (The editor is perfectly responsive, but it takes ages to check a few lines.) Any idea why?

I suppose we can just merge and test it in production.

[robertylewis]

The production version is much faster. Not sure what the difference is!

[bryangingechen]

Strange - I'm getting CORS errors for the file https://tqft.net/lean/web-editor/lean_js_wasm.wasm when I visit https://leanprover-community.github.io/lean-web-editor. Following up with @semorrison on Zulip...

Edit: The issue is with the uBlock rule discussed here. Adding this custom filter @@||*$xmlhttprequest,domain=leanprover-community.github.io solved the problem.

[cipher1024]

Is there a way to make several versions available?

[bryangingechen]

Several versions of community Lean? Yes, but it would take some work. What did you have in mind?