mathlib PR workflow(?) question(s)

Stream: new members

[George McNinch]

Hi--

I don't think I see an answer to this question in the "how to contribute to mathlib" docs though I may well have missed it.

After making a PR in August, I didn't touch my fork for for a while. I just now set upstream on the fork to the "actual mathlib", and merged the current mathlib with the branch on my fork. Now the build artifacts for my on-disk fork are out of date and need to be rebuilt, but this seems to be a big compile job.

lake exe cache get did something, but didn't seem to put my fork in a working state.

And lake build seems like it'll take a while.

Is there some better way to proceed? Maybe I shouldn't do this merge? Or perhaps I've just made a silly mistake?

(I'm pretty sure this difficulty has nothing to do with my PR, which just added a single fairly short file...)

Thanks for any advice!

[Aaron Liu]

George McNinch said:

lake exe cache get did something, but didn't seem to put my fork in a working state.

What did it do? Maybe if you run lake clean first and then lake exe cache get it'll work?

[George McNinch]

Actually, sorry. Now it does look like lake exe cache get did work, apparently.

(A few minutes ago, I was pretty sure I saw reports of build-jobs running in the VSCode InfoView when I opened "my file" in the fork. But now I don't see them.)

Sorry for the false-alarm!

(lake clean is a good suggestion though.)

[Yuval Filmus]

I'm working on several PRs simultaneously using different git branches.
Each time I switch to a different branch I need to download the cache again (lake exe cache get), or otherwise to wait for mathlib to compile locally.
Is there a way to avoid this?

[Sébastien Gouëzel]

When you switch to a branch you've already used, lake exe cache get should normally not need to download anything from the network, as the files are already cached on your computer, and it should only unpack them. Isn't it what you see?

[Etienne Marion]

You can download only the cache needed for the file you are working on. In VSCode you can click on the forall symbol, then go to Project Actions... -> Fetch Mathlib build cache for current imports. lake exe cache get <file> also works I think.