lean web editor on firefox

Stream: general

[Kevin Buzzard]

Here
's a proof that (2 : \R) + 2 = 4 in the Lean Web Editor. You can check it's working by clicking in between two of the characters in norm_num, where you should see "2 + 2 = 4" as the goal on the right hand side.

Works fine for me in Chrome, doesn't work for me in firefox (firefox quantum 65.0, 64 bit, I tried Ubuntu 16.04 LTS or 18.04 LTS).

I've been asked to give a talk about my teaching at some internal teaching thing and they want me to do "15 minutes of interactive Lean" with people who aren't mathematicians but are scientists. Apparently they will be told to bring their laptops. I don't fancy my chances getting it installed so it will have to be Lean Web Editor but I've had real problems with it on firefox recently.

[Bryan Gin-ge Chen]

Here's stuff from an earlier investigation -- I think it'll take someone with some knowledge about lean's webassembly build to get to the bottom of this https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/online.20leanprover/near/147928323

[Patrick Massot]

I really think using the web editor is a bad idea. What about using CoCalc? If you get CoCalc credits paid by your university, you can use those credits on a project and (after telling your audience to create CoCalc account if needed) enroll the audience in the project. This way (I think) they can use computing power you paid for. I'm sure you can ask William about this idea