Ensuring a repo builds on top of mathlib PRs

Stream: mathlib4

[Geoffrey Irving]

If I have an existing lake repo, and move some of its theorems into a mathlib PR, how does one best ensure the repo builds on top of the PR? Should I make the branch inside the lake-packages directory, or would that be clobbered?

[Yaël Dillies]

I usually make sure everything builds before I first open the PR and don't bother fixing downstream stuff every time someone asks for a change.

[Yaël Dillies]

You can also make your project depend on a specific commit of mathlib, be it on master or on your PR.

[Geoffrey Irving]

Everything builds already, so roughly I’ve already done step one. Yoloing the rest is okay I suppose.

[Jon Eugster]

Concretely, the "correct" way to do this is to modify the lakefile.lean of your project to contain

require mathlib from git
  "https://github.com/leanprover-community/mathlib4" @ "7d308680dc444730e84a86c72357ad9a7aea9c4b"

where you specify the commit of the mathlib-PR you build on. That way you can use the cache that CI built for the PR

Then you call the usual

lake update
lake exe cache get
lake build

in your project.

Don't do any manual git-stuff inside lake-packages, that will only be prone to problems down the line.

[Geoffrey Irving]

The cache never works for me (on M1 or M2 Mac); not sure if that’s expected.

[Anatole Dedecker]

No that’s not! If you’re going to work on mathlib we should definitely work on solving that

[Geoffrey Irving]

Fixed: This was just me not running the command (I hadn't tried since learning it didn't work on Lean 3).

Edit: No, still doesn't work in the ray repo. It works fine for mathlib itself, though, so I'm not immediately blocked.

[Yaël Dillies]

What do you mean by "doesn't work on the ray repo"? Do you mean the whole command fails when you call it inside the ray repo, or that is doesn't find cache for the ray repo but does find cache for mathlib? The latter is expected: you probably haven't set up a caching mechanism for your repo. The former would be quite bad and unexpected.

[Geoffrey Irving]

It downloads cached files without complaint, but then for some reason it proceeds to build 1800 mathlib files anyways on lake build. Here is a from scratch reproduction...no, actually checking out a fresh repo at the same CL doesn't have the same problem. So somehow my checkout is corrupted, and this seems not worth chasing down.

Fixed!

[Yaël Dillies]

Just in case you don't know about it, lake exe cache get! forces the redownload of all files.

[Geoffrey Irving]

Great, that seems to have fixed the initial repo too. :)

[Scott Morrison]

(And often merely lake clean && lake exe cache get suffices, but lake clean && lake exe cache get! is even more thorough!)