gitpod bug?

Stream: general

[Huỳnh Trần Khanh]

the lean extension is not installed and when i open the gitpod.yml file i see this error

Gitpod Config
Source: gitpod-schema.json

jroesch.lean extension is not found in Open VSX   gitpod

yeah the error message is pretty clear... something is broken on your end i'm pretty sure :joy:

[Huỳnh Trần Khanh]

anyway i can quickly spin up a Docker container on my machine and continue coding :joy: but i'm posting this for your information

[Huỳnh Trần Khanh]

you can easily reproduce this bug by opening the mathlib repo on gitpod!

[Alex J. Best]

Looks like a open-vsx / gitpod issue

[Alex J. Best]

That will hopefully resolve itself after a while?