gitpod

Stream: general

[Scott Morrison]

@Johan Commelin mentioned to me https://gitpod.io/, and I spent a little while setting it up for mathlib. It seems to work great. The upshot is that you can open mathlib (master, or a branch) in a copy of VSCode running "in your browser".

At the moment the configuration file is only available on branch#gitpod, which you can check out by visiting https://gitpod.io/#https://github.com/leanprover-community/mathlib/tree/gitpod

(There's also a gitpod chrome extension which adds buttons directly on github.)

My understanding is that if we merged that branch then you'd be able to open any branch on gitpod.

[Scott Morrison]

I had to create new docker layers that install lean and leanproject, but it seems to work fine. I've even managed to convince gitpod to download compiled oleans if available, so it is quite responsive.

[Yakov Pechersky]

You could probably use one of the python gitpod images

[Scott Morrison]

That stuff seems to just work: I rolled my own Dockerfile that follows the standard Lean install instructions.

[Yakov Pechersky]

Oh, I guess the -full one already has python

[Scott Morrison]

The problem I'm having now is that I can't push back to github from a gitpod editor. I can't work out how to authenticate.

[Scott Morrison]

In any case, I better sleep. Hopefully someone will play with it!

[Yakov Pechersky]

Is it that leanproject by default uses ssh?

[Scott Morrison]

I'm only using leanproject to collect the oleans.

[Scott Morrison]

It's just plain git that is having the problem.

[Scott Morrison]

Presumably, given how big a deal they make of github integration, this "just works" normally?

[Eric Wieser]

Are github codespaces still in closed beta?

[Eric Wieser]

Because they're likely even easier to set up than gitpod

[Eric Wieser]

https://github.com/features/codespaces

[Scott Morrison]

It is still closed (and makes no suggestion it will be free for open source projects after the closed beta).

[Scott Morrison]

Check out things like:
https://gitpod.io/#https://github.com/leanprover-community/mathlib/blob/gitpod/src/combinatorics/pigeonhole.lean

Loading a file from a particular branch, and although gitpod does not load instantly, when it does the yellow bars disappear instantly!

[Scott Morrison]

Anyone available to try out "shared workspaces"? Ping me and visit https://crimson-pig-qoopfdpx.ws-us03.gitpod.io/.

[Bryan Gin-ge Chen]

The infoview and underlining on errors / warnings doesn't seem to work for me, but everything else seems to.

[Bryan Gin-ge Chen]

Ah, there's a suspicious console error:

 Loading failed for the <script> with source “http://127.0.0.1:37485/gckj5j3cdxq//tmp/vscode-extensions/jroesch.lean@0.16.24/extension/media/index.js”.

I guess the extension is using localhost for something and that's not allowed?

[Yakov Pechersky]

image.png

[Adam Topaz]

@Scott Morrison do you still need someone to try out a shared workspace? This looks really cool!

[Scott Morrison]

Sorry, the shared one seems broken to me to.

[Adam Topaz]

Oh, I'm getting the same error as Yakov's screeshot

[Scott Morrison]

I closed the shared session.

[Alex J. Best]

Bryan Gin-ge Chen said:

The infoview and underlining on errors / warnings doesn't seem to work for me, but everything else seems to.

Ok I went down the debugging rabbit hole :rabbit:
vscode-lean uses a static server to serve the info view to work around a bug in vscode versions < 1.47 https://github.com/leanprover/vscode-lean/blob/master/src/infoview.ts#L353 .
The check if this is necessary is here https://github.com/leanprover/vscode-lean/blob/master/src/extension.ts#L119 by checking the vscode version number.
Theia / gitpod seems to override this version number at https://github.com/eclipse-theia/theia/blob/ef9d9eed2b2e9400c22097b1ab2c026f77e6d748/packages/plugin-ext-vscode/src/node/plugin-vscode-init.ts#L55 .
I can't find what the gitpod default is right now, but simply setting the right environment variable in the docker file to override this gets the extension to use webviews instead of the static server and it loads, go to definition even works!
I made this change on branch#gitpod-alex so you can try it at:
https://gitpod.io/#https://github.com/leanprover-community/mathlib/tree/gitpod-alex

[Alex J. Best]

@Scott Morrison this is really really amazing, I've dreamt of being able to step through code in PRs in lean without having to checkout the branch on my computer for ages, I'd never have thought that running a full vscode lookalike in the browser via docker would work though!

[Scott Morrison]

Fantastic!

[Scott Morrison]

I worked out how to push (sorry, I pushed a trivial commit to your branch and then reverted it).

[Scott Morrison]

I had to visit https://gitpod.io/access-control/ and select "read/write private repos", and then once I was at the github authorization page, grant access for the leanprover-community organization.

[Scott Morrison]

It's annoying this isn't obvious/automatic.

[Scott Morrison]

I wonder if we should turn branch#gitpod-alex into a PR, so this is available on all branches.

[Bryan Gin-ge Chen]

That seems like a good idea to me, unless there are some potential downsides I'm missing. After the PR is merged, we should also add some instructions on how to use gitpod to the community website.

[Scott Morrison]

I think the only downside is maintaining the two new files .gitpod.yaml and .gitpod.dockerfile. Perhaps the yaml will need an update whenever the VSCode extension gets a new version.

[Scott Morrison]

It is not currently particularly fast to load. When I told it use leanproject to download oleans, I think I did this in an "init" step that delays the start of the session. Perhaps we could run this asynchronously instead, so the editor appears faster. (But potentially without oleans...)

[Scott Morrison]

Hopefully we can also work out a trick to load a random chunk of text as a new file, just like the current web version.

[Alex J. Best]

You would still need to ensure it downloads the oleans before the extension starts lean I guess? I'd rather wait a little than get yellow bars and have to remember to restart the server, put it that way.

[Bryan Gin-ge Chen]

For the random chunk of text, maybe we could set up a skeleton "playground" repo depending on mathlib with an empty file to edit?

[Alex J. Best]

And while there are possibly some kinks to iron out still, I'd definitely vote for adding a link to the corresponding gitpod page to the PR template at some point for visibility.

[Johan Commelin]

Scott Morrison said:

It is not currently particularly fast to load. When I told it use leanproject to download oleans, I think I did this in an "init" step that delays the start of the session. Perhaps we could run this asynchronously instead, so the editor appears faster. (But potentially without oleans...)

I think they have a screencast on how to have prebuilt pods... that way loading everything should be "instant" (< 5 seconds)?

[Johan Commelin]

That would still be less time than grabbing a terminal, asking leanproject to clone the branch, download oleans, and open the branch in VScode locally.

[Johan Commelin]

@Scott Morrison @Alex J. Best thanks so much for looking into this!

[Scott Morrison]

I think this is as prebuilt as possible. There's a Dockerfile which has already installed lean and leanproject once and for all.

[Scott Morrison]

I'm pretty sure the remaining time is for them to boot the static image (nothing we can improve there), and to fetch the olean files from azure.

[Johan Commelin]

I was thinking of this https://www.youtube.com/watch?v=KR8ESjGYsXI

[Scott Morrison]

I see!

[Johan Commelin]

It might be possible to do the "fetch the oleans" step prior to the moment that the user wants to boot the image

[Scott Morrison]

I haven't watched, but I agree.

[Scott Morrison]

Hopefully we could even trigger it from our CI, once the oleans are ready.

[Scott Morrison]

But I think all this sort of optimisation should wait. It's pretty usable already.

[Johan Commelin]

Yes, because there is no good in having gitpod fetch oleans 5 seconds after a PR is opened.

[Scott Morrison]

@Alex J. Best, it occurs to me that the symptoms that you fixed were perhaps similar to the problems we were seeing with shared sessions in VSCode. I wonder if the underlying issue and fix are the same.

[Johan Commelin]

Oooh, that would be a pretty awesome side effect!

[Eric Wieser]

If we put the docker config in a new repo, then it would be possible to use github to publish a built docker image, and use it from things like lean-liquid too

[Scott Morrison]

My understanding of gitpod is that the customisable docker image that the end user can create does not actually contain the VSCode magic --- it's just all the command line level stuff. After you point .gitpod.yaml at a particular docker image they still layer their secret sauce on top.

[Eric Wieser]

Right, but it contains the elan /python faff that downstream projects might want to reuse

[Eric Wieser]

And I think the same image could be used by both codespaces and gitpod, although I now buy the argument that the latter is better anyway

[Scott Morrison]

It looks like enabling prebuilds is easy, and described at https://www.gitpod.io/docs/prebuilds/.

We go to https://github.com/apps/gitpod-io to turn on a switch. I think we would want to turn off automatic prebuilds of branchs and PRs, because there is no point allowing gitpod to start building until our CI that produces oleans has finished. So we would add a step in CI that pings a URL in the format https://gitpod.io/#prebuild/https://github.com/leanprover-community/mathlib/pull/6497/commits/73231b81d28e47d9077efe9abab0a354b556601a once oleans are ready.

[Scott Morrison]

Although I think we probably shouldn't bother doing this at first. No need to add needless load to their servers while we're deciding if we like it.

[Alex J. Best]

I guess the prebuild will be built using the credit associated to the leanprover-community account? Whereas individuals loading a workspace only use their own credits (this looks to be 50h per month, 100h upgrade free for people with github education)?

[Alex J. Best]

@Scott Morrison do you have any idea how hard it would be to add gitpod support to external projects importing mathlib, e.g. lean-liquid? Given that the #6515 will push docker containers which already contain lean and mathlib, is it as simple as having a .docker/blah/Dockerfile that is FROM leanprover-community/mathlib and fetches oleans for the project, or something like that?
PS: I tried out the PR the other day from an ipad and it worked great, I never though I'd be able to do lean from such a locked down device, its really cool!

[Scott Morrison]

I think this is the case, but haven't tested it yet. Hopefully you should just need FROM leanprovercommunity/mathlib:gitpod.

[Scott Morrison]

In fact, there should not be any need to have your own Dockerfile: you can directly use the image leanprovercommunity/mathlib:gitpod by creating a .gitpod.yml in the home directory of the other project, containing:

image: leanprovercommunity/mathlib:gitpod

vscode:
  extensions:
    - jroesch.lean

tasks:
  - command: . /home/gitpod/.profile && leanproject get-mathlib-cache

[Scott Morrison]

Someone should try it out!

[Scott Morrison]

If it works, we should add this to the .docker/README.md in #6515.

[Scott Morrison]

Yup, this "just works": https://gitpod.io/#github.com/leanprover-community/lean-liquid/

[Scott Morrison]

And I've added instructions to #6515.

[Bryan Gin-ge Chen]

(lean-liquid is getting big enough now that it took a few minutes to actually compile in gitpod. Another reason for PRing as much as possible back into mathlib!)

[Bryan Gin-ge Chen]

Not sure if it's just a temporary thing or if it's just me, but the vscode-lean extension doesn't seem to get installed anymore when using https://gitpod.io/#https://github.com/leanprover-community/mathlib/tree/docker or the lean-liquid gitpod link above. When I try installing it from open VSX it also doesn't seem to do anything. Everything worked yesterday with the lean-liquid gitpod, and I can't think of anything that changed that could have affected this.

[Scott Morrison]

I'm seeing the same.

[Scott Morrison]

I just tried installing from the extensions tab in gitpod. It acts like it works, but nothing has changed by the end of the process.

[Scott Morrison]

Hmm, after trying a second time it worked.

[Scott Morrison]

And now everything is working "out of the box" again, with a fresh gitpod VM. Perhaps just a transient issue?

[Alex J. Best]

I'm seeing the same thing, could it be https://github.com/leanprover/vscode-lean/commit/e5196ea7d0a29dcd2186e62ddeefdfb63df310ed ?

[Bryan Gin-ge Chen]

The gitpod link to the docker branch is working for me right now.

[Alex J. Best]

Weird its working again for me too, but it wasnt the last 5 times I tried

[Bryan Gin-ge Chen]

It might just be very flaky :sad:

[Bryan Gin-ge Chen]

gtsiolis from gitpod just posted a comment on the merged PR:

Great to see this PR getting merged! Let us know if run into any issues with Gitpod. Feel free to reach out in the communty forum or the issue tracker. :umm:

In case you've missed these:

• We recently switched the default editor (IDE) to VS Code, see relevant product roadmap item.
• We're also working on adding access to the remote dev environments through local VS code, see relevant PR and relevant product roadmap item. :map:️

Thanks for adding this @semorrison! :tada:

[Eric Wieser]

I had a lot of trouble with gitpod recently because my default editor was still stuck on the old non-vscode version - it seems the changed default might only apply to new users, and old users have to go change their settings to get the new default

[Eric Wieser]

(The non-vscode editor doesn't seem to work with the lean extension any more)

[Eric Wieser]

But after fixing that, everything works great and I regularly use it to try out PR suggestions

[Kevin Buzzard]

so computer novices like me can now start to use gitpod?

[Eric Rodriguez]

gitpod seemed really user-friendly to me after first trying it! just click the button on the PR and you get VSCode open with mathlib

[Eric Rodriguez]

didn't know it was advanced before

[Scott Morrison]

Until recently it wasn't working out of the box --- the VS Code extension for Lean was meant to be installed, but it seemed most of the time it mysteriously wasn't there.

[Scott Morrison]

Now (mysteriously? :-) it is there, so yes, @Kevin Buzzard should try it out. :-)

[Sebastian Ullrich]

Gitpod has been an absolute blessing for our Lean 4 course, with virtually no issues so far. Only too bad they activated VS Code by default just a few days after we told our students how to do so manually, haha.

[Kevin Buzzard]

It still doesn't work for me :-( I click on the gitpod link on a PR and I just get the error "Oh, no! Something went wrong!" and "NotFoundError; Learn more about supported context URLs". I had just assumed it wasn't working yet.

[Kevin Buzzard]

I get sent to this link which is not something I'm prepared to read https://www.gitpod.io/docs/context-urls

[Kevin Buzzard]

My day has already been derailed once by having to learn gimp instead of working on lean-liquid :-)

[Kevin Buzzard]

Just to be clear -- I'm clicking on the "open in Gitpod" link near the top of this URL https://github.com/leanprover-community/mathlib/pull/7322 , and the URL it's taking me to is https://gitpod.io/#https://github.com/

[Eric Wieser]

In what browser / OS?

[Eric Wieser]

I've read that the from-referrer links are blocked by some browser settings

[Eric Wieser]

They rely on gitpod being able to ask "what github page did you come from"

[Eric Wieser]

And many privacy controls say "I won't tell you that, you're only allowed to know I came from github, not the specific page"

[Kevin Buzzard]

Firefox on Ubuntu.

[Eric Rodriguez]

yep, trims referrers: https://blog.mozilla.org/security/2021/03/22/firefox-87-trims-http-referrers-by-default-to-protect-user-privacy/

[Eric Rodriguez]

that's the first time i've seen the referrer stuff not used to track you everywhere though, wow

[Kevin Buzzard]

Indeed I'm on 87. Can I fix this? I don't really want to switch to Chrome.

[Eric Wieser]

Nice find, I added a comment with that link to https://github.com/gitpod-io/gitpod/issues/688

[Eric Rodriguez]

for the mo, may be worth hard-writing the gitpod links because these updates seem to be happening everywhere

[Eric Wieser]

Seems fixable: https://privacyinternational.org/guide-step/4148/change-http-referer-settings-firefox

[Eric Rodriguez]

all browser vendors are caring about privacy now sadly (or in the case of google, pretending to care)

[Eric Wieser]

The long-term solution here is to pressure github to add a header say "I am fine with this URL being shared"

[Eric Wieser]

If github sent Referrer-Policy: no-referrer-when-downgrade in their HTTP headers, then they would be opting into allowing gitpod (and other arbitrary sites) to read the referrer

[Kevin Buzzard]

I'm quite happy not to be tracked in general. Is there no way I can switch this off on a per-site basis or something? I'm not even sure what I get at the end of this -- is this just "the same as" git checkout [branch I want to review] + leanproject get-cache?

[Eric Wieser]

(also, fun fact: "referer" is a mispelling that is now part of the HTTP standard)

[Eric Rodriguez]

as far as I can tell yes Kevin

[Eric Rodriguez]

(as in git-command-wise, I don't think firefox will let you change the ref settings per-site)

[Eric Wieser]

There's a bookmarklet here: https://github.com/Carbon-Monoxide/GitPod-Bookmarklet

[Eric Wieser]

So you could add that to your bookmark bar isntead of using the button in the PR text

[Eric Wieser]

Or literally just paste https://gitpod.io/# at the start of the PR url by hand

[Kevin Buzzard]

Progress! I have a bouncing G which has now taken about as long as the git commands would have done. ooh and now I get some errors:

 HISTFILE=/workspace/.gitpod/cmd-0 history -r; {
. /home/gitpod/.profile && leanproject get-mathlib-cache
}
ls: cannot access '/home/gitpod/.bashrc.d/*': No such file or directory
gitpod /workspace/mathlib $  HISTFILE=/workspace/.gitpod/cmd-0 history -r; {
> . /home/gitpod/.profile && leanproject get-mathlib-cache
> }
ls: cannot access '/home/gitpod/.bashrc.d/*': No such file or directory
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/e1f0dff356f716f0d9c71abd4e9a86ade444d59d.tar.xz to /home/gitpod/.mathlib/e1f0dff356f716f0d9c71abd4e9a86ade444d59d.tar.xz
100% 40.9M/40.9M [00:01<00:00, 36.5MiB/s]
Found mathlib oleans at https://oleanstorage.azureedge.net/mathlib/
gitpod /workspace/mathlib $

[Eric Wieser]

I think the errors are just noise

[Eric Wieser]

Which obviously would be nice to fix, but shouldn't get in your way

[Julian Berman]

I'm on Firefox 88 and it seems to work for me with no changes

[Alex J. Best]

For chrome at least there is an official gitpod plugin / add on that adds a gitpod button in a way that blends in with githubs ui.

[Eric Wieser]

A cautionary tale on relying on gitpod too much:

image.png

[Adam Topaz]

Oh capitalism...

[Gabriel Ebner]

There are unlimited student accounts for €8/month.

[Eric Wieser]

Indeed, and github gives me a 6 month trial. It's handy for PR reviews but I'm not going to pay for that convenience.

[Gabriel Ebner]

You could also try to apply for a "professional open source plan", which is €0/month. https://www.gitpod.io/docs/professional-open-source

[Eric Wieser]

Ideal, thanks - I just applied

[Joe Hendrix]

If a VSCode plugin isn't showing up in Gitpod, you may want to check that the "Default IDE" under preferences is "VS Code" and not "Theia". I just ran into that issue with another plugin.

[Eric Wieser]

I'm finding that gitpod is once again no longer loading the lean extension - is it working for anyone else?

[Eric Wieser]

Oh, here's why: https://open-vsx.org/

[Eric Wieser]

Oops, something went wrong and we're completely broken down.

[Eric Rodriguez]

can someone else check if gitpod currently works for them? for me, whenever I load anything, it doesn't have a leanpkg.path, and when I make it and restart the lean server, the infoview just stays blank

[Eric Wieser]

You have to run leanpkg configure manually

[Eric Wieser]

Although the UI provides a button to do that which should work

[Alex J. Best]

I've had to do the leanpkg configure and then restart the lean server thing every time I've used it for the past month at least. I'm not sure why though, we never used to have to do it?

[Eric Wieser]

depending on how you look at it, this is either a regression in leanproject, or a bug in the gitpod setup; is it leanproject get-caches job to configure the path?

[Eric Wieser]

(the regression was partly accidental by me, because the comment around the internal call to configure was written incorrectly in a way that suggested it was no longer relevant after the other changes)

[Alex J. Best]

Yeah i guess I'd err on the side of adding leanpkg configure to the gitpod script, or maybe to the docker image itself?

[Eric Rodriguez]

The issue isn't that (well not majorly), it's that afterwards for me the info view is non functional (it shows as an empty window). That may just be the computer, though, which is why Iask.

[Eric Wieser]

I guess the questions is; what's the expected flow for someone who runs git clone; whose job is it to run leanpkg configure? If someone doesn't depend on mathlib, then leanproject get-cache doesn't make sense for them anyway

[Patrick Massot]

If you run git clone instead of leanproject get then of course there is no guarantee things will work.

[Patrick Massot]

Eric Wieser said:

If someone doesn't depend on mathlib, then leanproject get-cache doesn't make sense for them anyway

Why?

[Patrick Massot]

You can still use the local cache mechanism without depending on mathlib

[Eric Wieser]

Sure, but if you're cloning a repository for the first time that cache will always be empty

[Eric Wieser]

So telling users to run it for the first time in a newly cloned repo, to have it run leanpkg configure but then fail with "no caches" isn't very ergonomic

[Alex J. Best]

@Eric Rodriguez can you try a different web browser?

[Eric Rodriguez]

I'll try, it was a public PC running firefox on Ubuntu fwiw

[Patrick Massot]

I'm sorry Eric W, I still don't know what you are talking about.

[Eric Wieser]

Sorry, I didn't make that very clear. Let's say there is a project lean-foo that depends on a project lean-bar but not mathlib. Here's the workflow that has always not worked:

git clone lean-foo
vscode  # uh-oh; vscode can't find `lean-bar`because no-one ran configure

Here's the workflow that has always worked:

git clone lean-foo
leanpkg configure
vscode  # ok

Here's the workflow that used to work, but no longer does after I separated get-cache from get-mathlib-cache :

git clone lean-foo
leanproject get-cache && true  # this command fails because there is no cache available, but we still need it
vscode  # ok on older versions of `leanproject` that eagerly tried `leanpkg configure`

[Patrick Massot]

What if you use leanproject get lean-foo?

[Eric Wieser]

Then none of these problems exist

[Eric Wieser]

Gitpod doesn't do leanproject get mathlib though, presumably because the container loads up with the repo already present.

[Kevin Buzzard]

Is it possible to make gitpod work on a random github Lean repo with mathlib as a dependency such as https://github.com/ImperialCollegeLondon/formalising-mathematics-2022 ?

The use case I am envisaging is someone who wants to try filling in sorries in files which have mathlib imports but who doesn't want to install Lean. Users would not need the ability to push their work or anything like that.

[Eric Wieser]

Yes, it's already set up on your M400001 or whatever repo

[Kevin Buzzard]

Is it also possible to fix the issue which I have with gitpod, which is that none of the links on the mathlib repo work for me because I'm using firefox and there's some trust issue with passing on some information? I never use gitpod and part of the reason for this is that I simply can't remember the fix, although no doubt it's documented here on Zulip. The error I always get is

broken.png

I'm not asking what the fix is (I can just plough through Zulip until I find it again), I'm asking whether I can make better links which work for everyone.

[Kevin Buzzard]

Eric Wieser said:

Yes, it's already set up on your M400001 or whatever repo

Eric I have a ton of repos with that silly phrase in :-/ If you tell me how to detect the setup I'm sure I can find it though.

[Kevin Buzzard]

I think I'm asking whether there's just some way to construct a URL which I can host somewhere which points to a file in one of my github repos and will work for everyone.

[Kevin Buzzard]

Actually now I phrase it like this I see that I can just use the web editor. What are the relative advantages/disadvantages of the two setups? I never use either of them myself. Is one of them noticably faster?

[Eric Rodriguez]

gitpod is way faster and is basically a full vscode, the web editor takes about 50 years to load nad is very slow

[Eric Wieser]

This repo: https://github.com/ImperialCollegeLondon/M40001_lean

[Eric Wieser]

Kevin Buzzard said:

I'm not asking what the fix is (I can just plough through Zulip until I find it again), I'm asking whether I can make better links which work for everyone.

Making the link work for everyone (by hard-coding your repo link into it instead of using from-referrer) comes at the expense of having it do the wrong thing on forks. The tracking issue for this problem is https://github.com/gitpod-io/gitpod/issues/6410

[Kevin Buzzard]

Thanks Eric for all the info. Doing the wrong thing on forks is fine by me.

[Jeremy Avigad]

@Kevin Buzzard Here's an example of a lean project based on mathlib that runs on Gitpod:
https://github.com/starkware-libs/formal-proofs
Once you launch it, you have to wait a couple of minutes for it to compile all the files in the repository. It is possible to set things up so that everything is prebuilt, but I am still fuzzy on the details. I also used a project based on Lean 4 for a class I was teaching (no external Mathlib 4, just a copy of an early version):
https://github.com/avigad/lamr
During the class, it started up almost immediately (and the terminal would give me a friendly message telling me how much time I saved because of the pre-build), but when I just tried it now, I had to wait a little while for it to compile.

[Kevin Buzzard]

Thank you Jeremy and Eric. I have got it all working now after your helpful clues, even on firefox. I totally agree that gitpod is amazingly fast!

[Kevin Buzzard]

Aargh no I haven't: the orange bars are gone and the Lean is working fine, I'm sure a server is running, but the infoview doesn't work:

Error loading webview: Error: Could not register service workers: SecurityError: The operation is insecure..

Update: I have it working with Chrome.

[Patrick Massot]

Kevin, could you write a very detailed howto explaining how you manage to get gitpod working for you before you forget? That would be very useful.

[Kevin Buzzard]

I literally didn't do anything other than moving a dot file which I found in one of my github repos into another one. Then it all just worked

[Kevin Buzzard]

I think Eric must have put the dot file there

[Kevin Buzzard]

I didn't even change the file

[Kevin Buzzard]

Detailed explanation of how to get gitpod working on a repo with mathlib as a dependency: add an exact copy of this file https://github.com/ImperialCollegeLondon/formalising-mathematics-2022/blob/master/.gitpod.yml to the root directory of your repo

[Kevin Buzzard]

And then you have two choices for the link to gitpod, one of which doesn't work on Firefox

[Kevin Buzzard]

https://gitpod.io/#/https://github.com/ImperialCollegeLondon/formalising-mathematics-2022/ is the one which works on Firefox

[Patrick Massot]

@Kevin Buzzard How can students access gitpod? Do they need to have a GitHub account?

[Johan Commelin]

Yes, gitpod gives you several ways to login. Reusing your github account is the most convenient option.

[Alex J. Best]

Students can also make use of github education to get an upgraded version of gitpod for free https://www.gitpod.io/github-student-developer-pack/

[Patrick Massot]

what are those several ways? I see only: use Github, Gitlab or bitbucket

[Johan Commelin]

That's what I meant

[Johan Commelin]

I didn't remember whether they also allowed other things like facebook or google

[Patrick Massot]

It's really crazy

[Johan Commelin]

They just outsource the whole authentication / user management.

[Patrick Massot]

Creating an account on some huge and frightening website only to access class resources sounds really crazy to me.

[Patrick Massot]

Johan Commelin said:

They just outsource the whole authentication / user management.

That doesn't make sense without an option to authenticate through google etc.

[Johan Commelin]

I can't argue against that

[Kevin Buzzard]

All I know about gitpod is that it works if you use your github credentials, I don't know if the students are using it

[Arthur Paulino]

Does gitpod run on a GitHub machine? Or is it configured to run somewhere else like Azure?

It makes sense to ask for a proper authentication so they have a bare minimum protection against bots spinning up infinite tasks on their machines

[Arthur Paulino]

In the worst case scenario they can at least ban evil accounts

[Arthur Paulino]

Wait, Azure is Microsoft's cloud environment. I forgot :joy:

[Heather Macbeth]

Kevin Buzzard said:

Detailed explanation of how to get gitpod working on a repo with mathlib as a dependency: add an exact copy of this file https://github.com/ImperialCollegeLondon/formalising-mathematics-2022/blob/master/.gitpod.yml to the root directory of your repo

Could someone help me troubleshoot these gitpod instructions?

When I try them on a small repo I set up for teaching,
https://gitpod.io/#/https://github.com/hrmacbeth/math2001
I get red underlines everywhere and horrible errors in the infoview:

invalid import: data.option.defs
invalid object declaration, environment already has an object named 'option.elim._main'

[Heather Macbeth]

I wondered if the problem might be that my repo is not on exact latest mathlib. Do I need to run leanproject up on the project every day right before class?

[Patrick Massot]

You can have a look at what I did at https://github.com/PatrickMassot/MDD154, it may help

[Heather Macbeth]

Thanks for the hint, Patrick. Do you know whether I can link to the same
https://raw.githubusercontent.com/PatrickMassot/MDD154/master/mdd154-1.0.0.vsix
file, or need to roll my own?

[Heather Macbeth]

(I see a vsix is a "Visual Studio extension" file, but I don't immediately understand the purpose.)

[Patrick Massot]

Sorry about the red herring. This is my custom version of the Lean VSCode extension.

[Heather Macbeth]

I see, so I can omit that line?

[Patrick Massot]

Its only purpose is to get syntax highligthing for my controlled natural language tactics.

[Patrick Massot]

You should replace that line with a line getting the regular extension.

[Patrick Massot]

Replace https://raw.githubusercontent.com/PatrickMassot/MDD154/master/mdd154-1.0.0.vsix with jroech.lean or something

[Heather Macbeth]

I see, thanks! Do I need - usernamehw.errorlens still?

[Patrick Massot]

It depends whether you want the error lens extension.

[Patrick Massot]

My experience is students have a very hard time paying attention to little red squiggles

[Patrick Massot]

And to be honest I also use it now.

[Heather Macbeth]

I see, so that's independent. Then the only substantive change should be changing command to init in the last line?

[Patrick Massot]

I guess my eyes aren't what they used to be

[Yaël Dillies]

They are always sooo little or misplaced :sad:

[Yaël Dillies]

Patrick Massot said:

I guess my eyes aren't what they used to be

Don't worry, I never see them either

[Patrick Massot]

Nobody ever told me my eyes little and misplaced

[Patrick Massot]

:grinning:

[Heather Macbeth]

He has eyes in the back of his head!

[Patrick Massot]

The change from command to init tells gitpod to get mathlib oleans before opening the workspace.

[Heather Macbeth]

OK, great. Let me try this out.

[Patrick Massot]

But it should work too with command I guess.

[Patrick Massot]

https://www.gitpod.io/docs/prebuilds

[Heather Macbeth]

No, with command (that was the only real difference between your script and Kevin's) I got the horrible errors.

[Heather Macbeth]

Or, you're saying that if I set up a prebuild then I can use command?

[Patrick Massot]

My understanding is setting up a prebuild allows to take advantage of init

[Patrick Massot]

But I didn't spend a lot of time understanding the details. I stopped as soon as I got something working.

[Patrick Massot]

At least I hope it still works. Can you get it to work?

[Patrick Massot]

I mean: does it work for you when you go to https://gitpod.io/#/https://github.com/PatrickMassot/MDD154/?

[Heather Macbeth]

Well, mine works now!

[Heather Macbeth]

Et oui, la tienne aussi.

[Heather Macbeth]

Thank you!

[Patrick Massot]

You're welcome!

[Jeremy Avigad]

I didn't realize that we could get away so simply with this:
image: leanprovercommunity/mathlib:gitpod

It looks like a nice setup, thanks to Scott. If I understand correctly, it always uses the most recent version of mathlib. Is there a way to link a project to a particular version of mathlib?

[Heather Macbeth]

@Jeremy Avigad It seems to be working on my project with a few-days-out-of-date mathlib!

[Jeremy Avigad]

Oh! I realize now that leanproject will just get the version of mathlib indicated in the .toml file. The setup is very nice.

[Heather Macbeth]

Indeed it is!

[Johan Commelin]

When I open mathlib3 in a gitpod instance, the goal view isn't working. Can anyone reproduce, or did I do something stupid?

[Eric Wieser]

Does closing the goal view and reopening it work?

[Johan Commelin]

nope

[Eric Wieser]

What type of not working?

[Johan Commelin]

It's an empty white pane.

[Johan Commelin]

I haven't been able to get any symbol on it

[Jeremy Tan]

Try another browser. I have the same issue with my usual Firefox browser, but it works on Chromium (Chrome)

[Johan Commelin]

aah, I'll try that

[Johan Commelin]

@Jeremy Tan awesome! That works

[Johan Commelin]

Maybe we should add a warning next to the gitpod icon

[Yaël Dillies]

It sometimes does the same for me in Chrome, I have to reload the tab.