vscode eternally loading

Stream: new members

[Luke Mantle]

I opened my local copy of the branch of mathlib I'm working on (to make some changes to my PR). However, the infoview shows nothing and the yellow loading indicators at the left side of the screen light up for the whole file. If I copy-paste the code into a different file (in the local repository I originally wrote it in before creating a branch of mathlib and submitting a PR), then the file loads fine. Any idea what's happening? One possibly relevant piece of information is that I recently merged master into my branch.

[Kevin Buzzard]

If you recently merged master into your branch then you have changed your version of mathlib so you either need to compile it or download precompiled binaries for precisely that version.

[Kevin Buzzard]

If you push the current version of your branch to github then mathlib's continuous integration will compile for you. If you already did this a while ago then perhaps it's done already and you can get your compiled binaries with leanproject get-cache

[Luke Mantle]

I committed and pushed the current version of my branch to Github, and then ran leanproject get-cache from the directory where my branch is saved locally. I got this result, and the same behaviour in vscode remains:

Looking for mathlib oleans for 9a4f789258
  locally...
  remotely...
No cache available for revision 9a4f789258
Looking for mathlib oleans for 61c4eea577
  locally...
  remotely...
  Found remote mathlib oleans
No cache was available for 9a4f789258. A cache was found for the ancestor 61c4eea577.
To see the intermediate commits, run:
  git log --graph 9a4f789258 61c4eea577^!
Run `leanproject get-cache --rev` on one of the available commits above.
Failed to fetch cached oleans

[Ruben Van de Velde]

The workflow is that you push to github, _you wait_, and when the cloud ("someone else's computer") is done compiling for you, you can download the results. But the waiting really is necessary - there's no such thing as a free compilation

[Eric Wieser]

I doubt it is necessary here

[Eric Wieser]

leanproject get-cache --fallback=download-first will almost certainly do the right thing

[Eric Wieser]

I got this result, and the same behaviour in vscode remains

The result is an error message that tells you what to do next! The behavior will remain until you do what it says (the --fallback suggestion I make above does it automatically for you).

[Kevin Buzzard]

You can't just randomly create a new version of mathlib (e.g. by merging two branches) and then expect it to work -- it needs to be built. It takes hours to compile mathlib. Either you do it manually or you push the result to github and let github do it for you, but it will take time.

[Luke Mantle]

Ah, ok, thanks for the explanations. By now it had finished compiling online so leanproject get-cache got it

[Eric Wieser]

create a new version of mathlib (e.g. by merging two branches) and then expect it to work

If you only modified a single new file, then you can expect it to work and leanproject get-cache --fallback=download-first will get you a cache that is right for everything except that new file