community web editor

Stream: general

[Kevin Buzzard]

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

[Patrick Massot]

Yes, something went really wrong

[Bryan Gin-ge Chen]

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

[Patrick Massot]

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

[Patrick Massot]

And indeed it also displays the annoying help

[Bryan Gin-ge Chen]

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]

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]

@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).