Zulip Chat Archive

Stream: general

Topic: community web editor


view this post on Zulip Kevin Buzzard (Feb 20 2020 at 20:42):

The community web editor is telling me file '/library/init/default.lean' not found. Is that bad?

view this post on Zulip Patrick Massot (Feb 20 2020 at 20:43):

Yes, something went really wrong

view this post on Zulip Bryan Gin-ge Chen (Feb 20 2020 at 20:43):

Yeah, something is broken. I'll look into it.

view this post on Zulip Patrick Massot (Feb 20 2020 at 20:44):

In the mean time you can use https://www.imo.universite-paris-saclay.fr/~pmassot/enseignement/math114/leanweb/

view this post on Zulip Patrick Massot (Feb 20 2020 at 20:44):

And indeed it also displays the annoying help

view this post on Zulip Bryan Gin-ge Chen (Feb 20 2020 at 20:46):

I added it because I thought it would be easier to read there than having to fiddle with the hover popups. I'll see if there's an easy way to toggle it on / off.

view this post on Zulip Bryan Gin-ge Chen (Feb 20 2020 at 21:22):

I found the issue that caused the web editor to break. There was a bug in the script that downloads the latest JS / WASM files to Scott's server. The editor should work now, though you may need to pop open the (?) modal and click the "Clear JS / WASM cache and refresh" button.

Thanks to Scott for the quick response!

view this post on Zulip Bryan Gin-ge Chen (Feb 23 2020 at 06:28):

@Patrick Massot I just added an checkbox in the (?) modal which allows you to toggle display of the tactic help in the infoview panel.

The various settings are also now saved to the browser's "local storage" so that they should persist between sessions (at least until you clear your cache).


Last updated: May 16 2021 at 22:14 UTC