norm_add₄_le

Stream: PrimeNumberTheorem+

[Terence Tao]

With the new mathlib bump, my local copy of ZetaBounds.lean is longer compiling, because the theorem norm_add₄_ledefined in https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/main/PrimeNumberTheoremAnd/ZetaBounds.lean#L1602 is now already defined in Mathlib as of 5 days ago, see https://github.com/leanprover-community/mathlib4/commit/c605a8b4af261801243d4141c605c798f4933dbb . I could probably fix this by removing the theorem from ZetaBounds.lean, but what puzzles me is that the mathlib bump seemed to pass CI without incident (and without any change to the actual Lean code), so is there a gap in the CI?

[Yury G. Kudryashov]

lake-manifest pins Mathlib to the parent of the commit that adds the lemma to Mathlib.

[Yury G. Kudryashov]

Probably, you've run lake update locally but didn't push the new lake-manifest to Github.

[Terence Tao]

I did... but the problem seems to not be entirely local because PNT#826 is also broken

[Pietro Monticone]

That's just because you locally executed lake update and then pushed the updated lake-manifest.json.

[Terence Tao]

Hmm... so I should abandon this branch and check out main again?

[Pietro Monticone]

If you want to keep the branch, you can just add rev = "v4.28.0-rc1" to the lakefile.toml for Mathlib, then run lake update ; lake exe cache get ; lake build and you should be fine.

[Terence Tao]

OK good to know in the future but I think this time I will simply cut and paste the PR changes into a new branch as there aren't that many of them

[Pietro Monticone]

Sure, as you prefer.

[Yury G. Kudryashov]

Lake uses the following model: lakefile.toml (or lakefile.lean) specify revision or branch. When you run lake update, it records the actual SHA sum into lake-manifest.json. If your package is sensitive to the revision of the upstream package (which is usually the case), the recommended way is to specify rev = in the lakefile.

[Alastair Irving]

We used to record the Mathlib revision in the lakefile but we seem to have stoppped doing so recently. Its possibly a good idea to put it back.

[Ruben Van de Velde]

The rule is not to run lake update unless you know how to fix the resulting errors

[Ruben Van de Velde]

I'm not sure I saw why it was run in this thread

[Terence Tao]

It was complicated. With the recent mathlib bump I accidentally started rebuilding all of mathlib. I halted that and tried to grab the cache instead, but something went wrong (C:\Users\teort\.cache\mathlib\eb1600b86215baa3.ltar: The requested operation cannot be performed on a file with a user-mapped section open. (os error 1224)) so I exited VSCode and tried to build lake from scratch, and at some point must have run lake update at a point where I should not have. I think I have finally managed to disentangle myself from this mess by manually adding the rev entry to lakefile.toml as Pietro suggested.

[Yury G. Kudryashov]

What's wrong with tracking rev in lakefile.toml? IMHO, -1 footgun is a good thing.

[Ruben Van de Velde]

It causes more work for the people who have learned what the command does and confuses the people who haven't, depriving them of the chance to learn