Zulip Chat Archive

Stream: general

Topic: lean web editor on firefox

Kevin Buzzard (Feb 11 2019 at 17:43):

'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 (Feb 11 2019 at 18:53):

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 (Feb 11 2019 at 20:14):

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

Last updated: Dec 20 2023 at 11:08 UTC