Issue running this in gitpod

Stream: Equational

[Leo Shine]

Hello I'm quite busy so probably won't be able to try things you suggest immediately but when I try to open the project up in gitpod I get errors like below is there anything we can do to make this a nicer onboarding experience? I just forked then opened it up in gitpod and it wasn't working

/home/gitpod/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/lake setup-file /workspace/equational_theories/equational_theories/Basic.lean Init Mathlib.Data.Nat.Defs Mathlib.Tactic failed:

stderr:
⚠ [50/2301] Replayed Mathlib.Lean.Meta
warning: ././.lake/packages/mathlib/././Mathlib/Lean/Meta.lean:75:22: Lean.Elab.Tactic.TacticM.runCore' is missing a doc-string, please add one.
Declarations whose name ends with a ' are expected to contain an explanation for the presence of a ' in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.

[Leo Shine]

"error: external command 'npm' exited with code 255" seems to be lower down in this file so presumably thats just not installed somehow?

[Leo Shine]

Or can it be turned off?

[Damiano Testa]

Can you give the gitpod link? The docPrime linter should be off by default in the project, so I would have to see why it is kicking off here.

[Shreyas Srinivas]

Did you open a file before cache and build ran?

[Leo Shine]

I bet I did that I'll try again being more patient later.

[Leo Shine]

Thank you

[Shreyas Srinivas]

Do let us know if that works

[Shreyas Srinivas]

The reason this wait is needed is that the docker image is setup to load a project as a volume (external folder) and cache needs to be run inside the project directory.

[Leo Shine]

Yes working great now thank you

[Kevin Buzzard]

Shreyas Srinivas said:

Did you open a file before cache and build ran?

This is a real gotcha for beginners who have not used Lean before. I was caught out by it a couple of times in the past before I realised what I was doing wrong. Is there a way we can somehow make this impossible?

[Shreyas Srinivas]

An ideal long term solution is to have a mathlib + cache installed with the toolchain

[Shreyas Srinivas]

Or in a central repository/directory

[Shreyas Srinivas]

And just linked into the project

[Shreyas Srinivas]

Short term, we have to create a container file for each project that packages the whole thing, and I think gitpod doesn't really work well with that. Someone who knows better can correct me on that point

[Shreyas Srinivas]

In fact I am quite certain on that point because docker containers don't persist any workspace edits by default

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

So they almost certainly use volumes or equivalent solutions

[Shreyas Srinivas]

And unfortunately we store mathlib and its build cache inside this workspace

[Shreyas Srinivas]

I'll check this point again. Maybe gitpod offers a workaround.

[Shreyas Srinivas]

Checked. We are already running the cache in their prebuild feature

[Shreyas Srinivas]

@Kevin Buzzard : your question and my response is probably of broader interest to lean4 devs and others. I request that we these messages to a suitable topic of the #lean4 channel.

[Shreyas Srinivas]

I want to bring this up again. It has become an irritant while I review PRs here because I have to wait 5 minutes, after the gitpod vscode has opened, before I can touch any lean files.

I believe if we had central mathlib installs rather than in-project installs, we could not only save space on our machines but also not wait for gitpod to run cache after the editor has opened. We could read the lean-toolchain file and have elan handle mathlib and get its cache downloaded before opening up the editor. I am really beginning to appreciate the opam + dune model now, where opam manages packages, not dune.

CC : @Joachim Breitner whom should I bring this up to?

[Joachim Breitner]

No idea, I don't know much about gitpod.

[Shreyas Srinivas]

This is more about the way lake manages packages. I believe if elan could manage packages, then we would be able to centrally install mathlib.

[Shreyas Srinivas]

If lean/mathlib could offer standard "switches" per toolchain, then all we would need it setup this "switch" (I am borrowing opam terminology) by reading the lean-toolchain file, and have elan install it. Then lake would just have to find and link it.

[Daniel Weber]

Shreyas Srinivas said:

If lean/mathlib could offer standard "switches" per toolchain, then all we would need it setup this "switch" (I am borrowing opam terminology) by reading the lean-toolchain file, and have elan install it. Then lake would just have to find and link it.

Mathlib has version tags (e.g. https://github.com/leanprover-community/mathlib4/tree/v4.12.0), is that a "switch"?

[Shreyas Srinivas]

Not quite. The closest thing we have to a switch in lean are the version tags we use in lakefile.lean.

[Shreyas Srinivas]

The idea I am borrowing from switches is to isolate toolchain + dependencies for one or more projects and store them centrally. Potentially also garbage collecting the unused ones.

[Michael Bucko]

Shreyas Srinivas schrieb:

I want to bring this up again. It has become an irritant while I review PRs here because I have to wait 5 minutes, after the gitpod vscode has opened, before I can touch any lean files.

I believe if we had central mathlib installs rather than in-project installs, we could not only save space on our machines but also not wait for gitpod to run cache after the editor has opened. We could read the lean-toolchain file and have elan handle mathlib and get its cache downloaded before opening up the editor. I am really beginning to appreciate the opam + dune model now, where opam manages packages, not dune.

I guess it'd be possible to pre-fetch and build dependencies before the editor starts (.gitpod.yml). Something like this (lake would just fetch the cached stuff). Would that help?

tasks:
  - init: |
      elan toolchain install $(cat lean-toolchain)
      lake exe cache get
      lake build
    command: code .

[Shreyas Srinivas]

We already do that

[Shreyas Srinivas]

Minus the lake build

[Shreyas Srinivas]

The issue is that these init tasks run after the editor has opened up. They need to be run inside the project folder that I think is mounted as a volume (or the other persistent option on gitpod).

[Shreyas Srinivas]

The elan install is part of the dockerfile

[Shreyas Srinivas]

Ideally we would like to do mathlib cache inside the dockerfile as well.

[Shreyas Srinivas]

But this is not possible since lake has to fetch Mathlib + cache and it can only learn the project's toolchain inside the folder and do the above setup after opening the project folder

[Shreyas Srinivas]

In my idea we have docker files specific to a toolchain / switch(hypothetical) and elan can install Mathlib + cache as part of this switch. This step would be accomplished when the docker image is compiled, which happens before the editor launch .The project can then picks its "switch" and dependency subset and can get linked to it by talking to elan or searching the include directories provided by elan

[Shreyas Srinivas]

For local purposes since people try to stick to the latest toolchain, the unused ones can be garbage collected like nix does