Zulip Chat Archive

Stream: general

Topic: community web editor broken?

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?

Kenny Lau (Apr 19 2020 at 18:15):

(UK time is GMT+1)

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.

Kevin Buzzard (Apr 19 2020 at 19:10):

Many thanks Bryan.

Kevin Buzzard (Apr 20 2020 at 10:35):

It works again :tada: Many thanks indeed Bryan!

Bryan Gin-ge Chen (Apr 20 2020 at 22:12):

Hope the talk went well!

Kevin Buzzard (Apr 20 2020 at 22:12):

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

Last updated: Dec 20 2023 at 11:08 UTC