Zulip Chat Archive
Stream: condensed mathematics
Topic: gitpod
Johan Commelin (Mar 15 2021 at 07:14):
@Scott Morrison what does it take to enable gitpod for lean-liquid?
Scott Morrison (Mar 15 2021 at 07:16):
I think I did it already. :-)
Scott Morrison (Mar 15 2021 at 07:17):
Just prefix https://gitpod.io/# to a git URL
Johan Commelin (Mar 15 2021 at 07:19):
Oooh cool!
Johan Commelin (Mar 15 2021 at 07:19):
Do you know if we can now use gitpod for (brief?) pair programming sessions?
Kevin Buzzard (Mar 15 2021 at 07:25):
Why brief?
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
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...
Scott Morrison (Mar 15 2021 at 08:10):
Gah... same thing is happening on mathlib :-(
Eric Wieser (Apr 17 2021 at 15:37):
I can't seem to install the lean extension through the gui either (on mathlib)
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"
Eric Wieser (Apr 17 2021 at 15:56):
Last updated: Dec 20 2023 at 11:08 UTC