Zulip Chat Archive

Stream: general

Topic: VScode in the browser


view this post on Zulip Johan Commelin (Apr 27 2018 at 12:58):

Has anyone seen https://spiffcode.github.io/ghedit/ before?

view this post on Zulip Johan Commelin (Apr 27 2018 at 12:59):

Pretty cool stuff. Now we only need a server farm to run lean in the backend, and then we can have an online workflow that actually works (I hope)

view this post on Zulip Johan Commelin (Apr 27 2018 at 13:07):

Maybe this is something the CoCalc is interested in. I might actually send William Stein an email. Then we can have collaborative lean. That would be a lot of fun.

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 15:43):

I have spent some time talking to William about Lean, and I have used Lean within cocalc.

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 15:43):

But we're not ready

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 15:43):

because we are waiting for a stable lean and a stable mathlib

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 15:44):

and the moment we have it

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 15:44):

we will have multiplayer lean

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 15:45):

@Sebastian Ullrich -- are we currently waiting for a new stable Lean? I am unsure what is happening.

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 15:45):

Johan, please email William with your ideas.

view this post on Zulip Johan Commelin (Apr 27 2018 at 16:30):

Johan, please email William with your ideas.

Done

view this post on Zulip Sebastian Ullrich (Apr 28 2018 at 07:50):

@Kevin Buzzard I'm planning to release 3.4.1 today

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 14:59):

That is half of the great news I am looking forward to.

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 14:59):

The other half being when Mario says that mathlib works fine with it.

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:02):

@Sebastian Ullrich I stayed up for 24 hours straight yesterday talking on this forum about how to get Lean to accurately model an extremely subtle concept which mathematicians take for granted and which is deeper than they think. Lean is a perfect language for mathematicians and I am continually reminded of this. Thank you to you and @Gabriel Ebner for being the bridge between Lean and mathematicians and I really look forward to working together in the future.

view this post on Zulip Kenny Lau (Apr 28 2018 at 15:03):

lol you have a lecture in 2 days and you just messed up your sleeping schedule

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 15:03):

A powerful and stable release of Lean and Mathlib makes teaching so much easier, and I feel that we are nearly there.


Last updated: May 10 2021 at 00:31 UTC