Zulip Chat Archive

Stream: general

Topic: lean web editor on firefox


view this post on Zulip Kevin Buzzard (Feb 11 2019 at 17:43):

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.

view this post on Zulip 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

view this post on Zulip 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: May 17 2021 at 21:12 UTC