Zulip Chat Archive

Stream: general

Topic: community web editor broken?


view this post on Zulip Kevin Buzzard (Apr 19 2020 at 18:15):

I'm giving a talk in about 15 hours and I was going to demo the community web editor but it's broken for me (on Chrome and firefox). webeditor.png

Is there any chance it will be back up and running by 2pm UK time tomorrow?

view this post on Zulip Kenny Lau (Apr 19 2020 at 18:15):

(UK time is GMT+1)

view this post on Zulip Bryan Gin-ge Chen (Apr 19 2020 at 18:30):

Ugh, sorry about that. I thought I fixed all the hiccups that happen when the latest released Lean and the latest released mathlib are out of sync, but it looks like something went wrong because mathlib's 3.9.0 upgrade occurred while the daily web editor build was happening. I'll rerun the job now (should finish in 3 hours or so) and in the meantime I'll see if I can make this more robust.

view this post on Zulip Kevin Buzzard (Apr 19 2020 at 19:10):

Many thanks Bryan.

view this post on Zulip Kevin Buzzard (Apr 20 2020 at 10:35):

It works again :tada: Many thanks indeed Bryan!

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

Hope the talk went well!

view this post on Zulip Kevin Buzzard (Apr 20 2020 at 22:12):

Yeah it went fine. Thanks for asking :-) I had an hour of questions afterwards :-)


Last updated: May 11 2021 at 13:22 UTC