naive gitpod questions

Stream: general

[Kevin Buzzard]

I'm facing the issue of having to give a talk using someone else's fixed Windows machine rather than my own laptop. In this particular case I will be able to have access to the machine and install git/python/VSCode beforehand, but this will still take me a while.

However, one option which is perhaps now available to me is using gitpod. I've not used this service at all really, I tried it once when reviewing a PR but it didn't work for me (some issue with firefox not passing on links or something) and then I tried it using a workaround which I no longer remember and it did work (but because I don't remember the workaround I'm unlikely to try it again, unless the issue has been fixed). But it seemed to me that the initial startup time was comparable to the time taken to run the old-fashioned git checkout pr_branch; git pull; leanproject get-cache method which I've been using for years, and the machines I use Lean on have plenty of ram and disc space, so I'm not motivated to change.

What does motivate me to think about gitpod however is firstly this issue with giving talks on machines which aren't my own, and secondly occasional social media posts where you want to e.g. post a one-liner on Twitter which does something and I usually go with the web editor, which is very reliable but also quite slow. My questions then:

1) Is there a gitpod way to do this lean web editor link -- a URL which just demonstrates Lean in action? If so, does it actually get to the point where it's running, more quickly than waiting for "Lean is busy" to turn into "Lean is ready"?

2) Is there some kind of canonical and reliable link that I can bookmark and which just fires up a working lean+mathlib session and a scratch file open so that I can start coding e.g. in front of a live audience on a machine with no Lean installed? If so, is it the kind of link I can go to in a browser before a talk has started, and then switch to the browser and just have Lean online and responsive immediately, without having timed out or anything like that?

[plus this time next year I'll be asking the same questions about Lean 4 and its mathlib]

[Eric Wieser]

Here's an example of the type of gitpod link you can share, which should directly go to a file you care about:

https://gitpod.io/#https://github.com/ImperialCollegeLondon/M40001_lean/blob/master/src/2020/problem_sheets/sheet1.lean

Here's the canonical one for just opening mathlib

https://gitpod.io/#https://github.com/leanprover-community/mathlib

[Eric Wieser]

I'm not sure you can avoid a timeout, but the default of half an hour might be ok for a talk

[Kevin Buzzard]

Thanks!

[Kevin Buzzard]

Oh I see -- it runs leanproject get-cache on the server? So in terms of speed it's probably actually slower than reviewing locally, assuming you're on a reasonable machine?

[Eric Wieser]

I find that leanproject get-cache runs a lot faster on the server; something to do with un-tar.gz-ipping on windows (via Python) being slow

[Eric Wieser]

Once you've opened the workspace once though, you don't need to get the cache again after reviving it from a timeout

[Eric Wieser]

When gitpod times out, it saves all your work then throws away the VM you were running on, as far as I can tell; meaning all the oleans are still there when you revive it.

[Kevin Buzzard]

Thanks for all this info!

[Alex J. Best]

Yeah I also found the download speed for caches to gitpod very fast (possibly due to everything being on a server in some data center, rather than having to pass through my home wifi)

[Eric Rodriguez]

does anyone else have problems firing up gitpod now that we've bumped to 3.46?