gitpod/codespaces/local installation for Lean repo

Stream: general

[Kevin Buzzard]

My go-to template for the three things I want to tell undergraduates about installing projects is the README from my IISc repo here. I wrote notes to myself explaining how I set all this stuff up, and took screenshots which were specific to that project etc so it's going to be a pain updating them. But what I'm really worried about is whether those files are now out of date.

1) Local installation.

Right now my instructions say to use the command line. This is no good for my clients today (1st year maths undergrads). Is there yet a safe command-line-free path to installing everything needed to painlessly run a random Lean repo which depends on mathlib? I think there surely should be now is but where do I read about it? The community page tells me to use the command line, and the official instructions on the Lean website doesn't mention projects which depend on mathlib. If I follow the Lean website instructions and click on upside-down-A->documentation->show setup guide and then "Set up Lean 4 project" and then "Download an existing project" and then I type https://github.com/ImperialCollegeLondon/IUM/ into the box, hitting enter does nothing. Is this somehow the wrong format? It looks like the same format that mathlib and MIL are using. git@github.com:ImperialCollegeLondon/IUM.git doesn't work either. What am I doing wrong? I cannot figure out a command-line free path to getting the repo https://github.com/ImperialCollegeLondon/IUM/ running locally.

2) Running remotely.

The files which I seem to have to add to my project are .gitpod.yml and .docker/gitpod/Dockerfile (for gitpod) and .devcontainer/devcontainer.json and .devcontainer/Dockerfile (for codespaces), and I just tend to copy these files around, changing what needs to be changed. I'm a bit unhappy about this because I might not have the "latest version" and I don't really understand any of these files. Where is a safe place to get possibly updated versions of these files?

[Marc Huisinga]

Kevin Buzzard said:

If I follow the Lean website instructions and click on upside-down-A->documentation->show setup guide and then "Set up Lean 4 project" and then "Download an existing project" and then I type https://github.com/ImperialCollegeLondon/IUM/ into the box, hitting enter does nothing.

It should open a file selection dialog that you can use to select the location of where the project should be downloaded to. It seems to work for me. Can anyone else confirm this issue?

[Marc Huisinga]

Did you select the "Git repository URL" entry?

[Kim Morrison]

Worked beautifully for me, I have a new copy of IUM now.

[Kim Morrison]

Actually there was one problem: while lake is cloning Mathlib, which takes quite a while, there is no visual feedback.

[Kim Morrison]

i.e. lake exe cache get prints nothing for almost a minute while the clone happens.

[Sebastian Ullrich]

For Codespaces, I believe it is possible to add these files to a public index where they can be versioned and easily be added to a workspace using "Dev Containers: Add Dev Container Configuration Files": https://containers.dev/features

[Kim Morrison]

We need to fix that --- ideally lake could make a shallow clone?

[Kim Morrison]

Otherwise perhaps it can special case cloning Mathlib and print something before it starts, so there is some indication that the user really should wait --- the cancel button becomes very tempting with no feedback.

[Sebastian Ullrich]

Sebastian Ullrich said:

For Codespaces, I believe it is possible to add these files to a public index where they can be versioned and easily be added to a workspace using "Dev Containers: Add Dev Container Configuration Files": https://containers.dev/features

And Gitpod is working on supporting the same files as well: https://github.com/gitpod-io/gitpod/issues/7721#issuecomment-2187465251

[Marc Huisinga]

Kim Morrison said:

Actually there was one problem: while lake is cloning Mathlib, which takes quite a while, there is no visual feedback.

Is there no progress bar in the bottom right?

[Marc Huisinga]

Ah, I see, you're referring to the initial part of lake exe cache get not yielding output for a long time? I.e. this part?

/home/mhuisi/Lean/MathlibTest> lake exe cache get
info: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'
info: importGraph: cloning https://github.com/leanprover-community/import-graph to '././.lake/packages/importGraph'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient to '././.lake/packages/LeanSearchClient'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli'

[Marc Huisinga]

Oops, I missed that this comment was about IUM, not Mathlib, sorry. Yes, that indeed shows no progress for a while.

[Yaël Dillies]

Kevin Buzzard said:

The files which I seem to have to add to my project are .gitpod.yml and .docker/gitpod/Dockerfile (for gitpod) and .devcontainer/devcontainer.json and .devcontainer/Dockerfile (for codespaces), and I just tend to copy these files around, changing what needs to be changed.

I have a solution to the middle file: Make your .gitpod.yml file be

# This is run when starting a Gitpod workspace on this repository

image: leanprovercommunity/gitpod4

vscode:
  extensions:
    - leanprover.lean4 # install the Lean 4 VS Code extension

tasks:
  - init: |
      elan self update
      lake exe cache get

[Yaël Dillies]

leanprovercommunity/gitpod4 is the name of one the community-curated docker images hosted on dockerhub (and I am the one maintaining those image up to date), precisely the one meant to be used in gitpod with Lean 4. That image plays the same role as your .docker/gitpod/Dockerfile, except that it's hosted online.

[Shreyas Srinivas]

The default gitpod file is not tied to any specific version of mathlib

[Eric Wieser]

Kevin Buzzard said:

I'm a bit unhappy about this because I might not have the "latest version"

Depending your goal, this may be a good thing. Having the latest version in a git repo where everything else is fixed can lead to things no longer working in the long run.

Shreyas Srinivas said:

The default gitpod file is not tied to any specific version of mathlib

This is true for now, but may not remain true forever. For instance, I believe the current container includes a partial python installation to enable polyrith. If a future version of mathlib implements polyrith from scratch, then this dependency might end up dropped from the container (using every dependency that mathlib ever once had is messy and hard to enforce).

[Ruben Van de Velde]

I think the point re: "latest version" is more that there should be a place that hosts templates/documentation, which are kept up to date and you can follow/copy when creating a new project

[Shreyas Srinivas]

I want to suggest adding some template repos in the community repository (ideally organised under one project or something similar). Example: tagged math project template where each git tag is pinned to a corresponding toolchain and whose gitpod and devcontainer files use a local docker image working with that toolchain version

[Shreyas Srinivas]

A similar idea came up on the coq zulip a few weeks ago

[Kim Morrison]

Marc Huisinga said:

Oops, I missed that this comment was about IUM, not Mathlib, sorry. Yes, that indeed shows no progress for a while.

I created an issue to track this at lean#5615.

[Kevin Buzzard]

Kim Morrison said:

Worked beautifully for me, I have a new copy of IUM now.

Thanks a lot Kim for taking the time -- this is clear evidence that the problem is at my end. Sounds like I might be doing something bone-headed.

Right now I'm opening VS Code in an empty directory, hitting ctrl-N to make a new file (this making the upside-down A appear), then upside-down A -> open project -> download project -> type https://github.com/ImperialCollegeLondon/IUM/ into the text box that appears -> now I'm stuck.

stuck.png

Enter/return/whatever that key is called nowadays does nothing, and the box is greyed out as if to indicate "you didn't put something I recognise in that box yet".

[Kevin Buzzard]

Indeed, typing in https://github.com/leanprover-community/mathlib/ manually into that box gives me the same result (no ability to progress). Selecting mathlib from the dropdown tool (rather than typing in the URL manually) works fine, I get a popup window asking me where I want to download the repo and then, as I think has been pointed out already, I get a very long pause where it's not at all clear that anything is happening, but things are happening. This is on Ubuntu 20.04, I could update if necessary, my instinct with older laptops is "don't upgrade OS unless necessary" but this is based on experiences from 20 years ago where I've hugely degraded performance by upgrading.

[Markus Himmel]

The trick is to click on "Git repository URL" while the text box is empty and then paste in the URL and then hit the Enter key. This is indeed confusing, I'll open an issue to make it less confusing.

[Markus Himmel]

https://github.com/leanprover/vscode-lean4/issues/530

[Kevin Buzzard]

Indeed this was exactly my error: I was just dumping the URL straight into the text box. Sorry for the noise and thanks!