Zulip Chat Archive

Stream: condensed mathematics

Topic: gitpod


view this post on Zulip Johan Commelin (Mar 15 2021 at 07:14):

@Scott Morrison what does it take to enable gitpod for lean-liquid?

view this post on Zulip Scott Morrison (Mar 15 2021 at 07:16):

I think I did it already. :-)

view this post on Zulip Scott Morrison (Mar 15 2021 at 07:17):

Just prefix https://gitpod.io/# to a git URL

view this post on Zulip Johan Commelin (Mar 15 2021 at 07:19):

Oooh cool!

view this post on Zulip Johan Commelin (Mar 15 2021 at 07:19):

Do you know if we can now use gitpod for (brief?) pair programming sessions?

view this post on Zulip Kevin Buzzard (Mar 15 2021 at 07:25):

Why brief?

view this post on Zulip Johan Commelin (Mar 15 2021 at 07:25):

Not sure how many CPUs gitpod throws at this... I can imagine that local lean will be snappier

view this post on Zulip Johan Commelin (Mar 15 2021 at 07:36):

@Scott Morrison It seems that the lean extension should be installed by default, but I don't have a goal view or syntax highlighting...

view this post on Zulip Scott Morrison (Mar 15 2021 at 08:10):

Gah... same thing is happening on mathlib :-(

view this post on Zulip Eric Wieser (Apr 17 2021 at 15:37):

I can't seem to install the lean extension through the gui either (on mathlib)

view this post on Zulip Eric Wieser (Apr 17 2021 at 15:53):

Ah - you have to go into your gitpod settings and change your IDE from "theia" (the old default) to "vscode"

view this post on Zulip Eric Wieser (Apr 17 2021 at 15:56):

https://gitpod.io/preferences


Last updated: May 09 2021 at 16:20 UTC