Zulip Chat Archive

Stream: general

Topic: community web editor

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?

Patrick Massot (Feb 20 2020 at 20:43):

Yes, something went really wrong

Bryan Gin-ge Chen (Feb 20 2020 at 20:43):

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

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/

Patrick Massot (Feb 20 2020 at 20:44):

And indeed it also displays the annoying help

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.

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!

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: Aug 03 2023 at 10:10 UTC