mathlib bump

Stream: PrimeNumberTheorem+

[Sébastien Gouëzel]

I am bumping mathlib in https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/178, to use that mathlib knows that Fourier transform is a bijection on Schwartz space. The bump went really well thanks to deprecations (apart from the nat_cast renaming, on which we forgot to add deprecations). And Lean became more powerful at several places (less bugs in typeclass inference, gcongr more powerful), so most fixing was just removing things because the goal was already closed!

[Yaël Dillies]

Sébastien Gouëzel said:

apart from the nat_cast renaming, on which we forgot to add deprecations

Was this mine?

[Sébastien Gouëzel]

Probably, yes. I'll look if I can generate the deprecations automatically.

[Sébastien Gouëzel]

Deprecations in #13368 (around 275 deprecations...).

[Yaël Dillies]

Oh I see. Deprecations were not really "forgotten". Since there were so many of them and the name change was so mechanical, it was decided to not bother.

[Alastair Irving]

Maybe you should have specified specific commits for Mathlib and the other dependencies rather than just the master branch. When I run make I get an error:
error: ././.lake/packages/mathlib/lakefile.lean:86:2: error: unknown attribute [test_driver]
which I think is because Mathlib has now moved to Lean 4.9 but we're still on 4.8.

[Ruben Van de Velde]

This is what the JSON file is for

[Ruben Van de Velde]

Preparing one now

[Ruben Van de Velde]

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/192

[Alex Kontorovich]

Darn, this broke again... (Building docs...) Any help?

[Pietro Monticone]

Sure, doc-gen4 isn't in manifest.

Fixed, tested locally and opened PR.

[Mauricio Collares]

I believe there's no need to update the manifest, since make doc does that in CI (the last passing commit doesn't have doc-gen4 in the manifest, for example). Pointing to the correct doc-gen4 commit in lakefile.lean should suffice.

[Pietro Monticone]

When I locally run

lake -R -Kenv=dev build PrimeNumberTheoremAnd:docs

It returns:

error: dependency '«doc-gen4»' not in manifest; use `lake update «doc-gen4»` to add it

I tend to believe it's better to have all the dependencies in the manifest file, but I'm not sure.

[Mauricio Collares]

I don't mind either way, but CI doesn't run lake directly. It runs make LAKEBIN='~/.elan/bin/lake' doc, and the Makefile takes care of running $(LAKEBIN) -R -Kenv=dev update before running a documentation build.

[Pietro Monticone]

I see... the PNT+ workflow is different from those I'm used to.

Thanks @Mauricio Collares for pointing that out.

[Pietro Monticone]

The changes in this PR should work in any case.

[Alex Kontorovich]

It worked! Thank you!!

[Ruben Van de Velde]

Not sure what's wrong with the CI in https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/203 ; it builds locally

[Kevin Buzzard]

When I've seen errors like this, they're sometimes caused by the fact that even though a file builds locally, it somehow conflicts with another file in the repo which isn't imported. Can you get the error locally if you import the entire project all in one go?

[Ruben Van de Velde]

That shouldn't be it - I'm also running lake build locally. In fact, I did see that error before, but I fixed it by changing the version of mathlib I depended on

[Alex Kontorovich]

Paging @Ian Jauslin - any idea what's going on here?

[Mauricio Collares]

Note that CI on PRs essentially runs lake update; lake exe cache get; lake build. If your lakefile does not use a pinned commit, the lake update step could cause problems. CI on master does a similar thing.

With this command I can reproduce the build failures in the PR because mathlib's v4.13.0 tag moved from d5ab93e3a3afadaf265a583a92f7e7c47203b540 to d7317655e2826dc1f1de9a0c138db2775c4bb841.

[Mauricio Collares]

Ah, the same problem is being discussed at #general > v4.13.0 discussion I believe

[Ruben Van de Velde]

Oh, why is it doing that?

[Alex Kontorovich]

Ack! Docs failing to build again...

[Ruben Van de Velde]

Oh, same issue

[Ruben Van de Velde]

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/205 - alternatively I can pin the lake commit in the lakefile.lean

[Ian Jauslin]

We are using a pinned commit, so lake update should not cause issues, as long as there is no inherent incompatibility with the version of mathlib that is pinned.
So I'm adding lake update back into the workflow.

[Ian Jauslin]

The issue seems to be with the bump to version 4.13.0. Why is the bump needed? Should we revert to 4.12 for now?

[Ruben Van de Velde]

The issue is that a tag is not fixed, and the v4.13.0 tag changed after EulerProducts updated to it

[Ruben Van de Velde]

Why do you want to run lake update? What purpose does that serve?

[Ian Jauslin]

It downloads the appropriate versions of the dependencies, does it not?

[Ian Jauslin]

So if the tag is being moved, shouldn't we revert to 4.12 until things are settled?

[Mauricio Collares]

The tag was moved once to bump ProofWidgets (to get this fix), I don't think it's expected to change again. But since the tags point to master instead of a separate branch, applying the ProofWidgets bump meant picking up a bunch of unrelated commits as well.

[Ian Jauslin]

It seems that EulerProducts is not working properly with the newly tagged 4.13.0, as @Ruben Van de Velde mentioned. I'm guessing we should revert to the commit that was previously tagged as 4.13.0? Or revert everything to how it was with 4.12.0?

[Ruben Van de Velde]

Why do you want to revert things? What purpose does that serve?

[Ian Jauslin]

The project currently does not compile

[Ruben Van de Velde]

What makes you say that?

[Ian Jauslin]

In the CI, if we don't run lake update, then it keeps the old versions of the dependencies that are cached. So not running lake update is not a fix: it just prevents the version of mathlib and EulerProducts that was cached from being updated to the versions in the lakefile. If you download a fresh version of the repo and try to compile it, it fails, with an error related to EulerProducts.

[Ruben Van de Velde]

That's not true

[Ruben Van de Velde]

lake build will use the versions of dependencies that are listed in the JSON file

[Ruben Van de Velde]

Running lake update in CI will either do nothing or do the wrong thing

[Ian Jauslin]

But not the versions in the lakefile

[Ian Jauslin]

If lake update breaks the build, then there's a problem, wouldn't you agree?

[Ruben Van de Velde]

The JSON file is updated from the lake file locally

[Ruben Van de Velde]

No, that is expected

[Ian Jauslin]

Why should lake update break the build?

[Ruben Van de Velde]

Because it can change the versions of dependencies you're using - because that's its purpose

[Ruben Van de Velde]

And updating your dependencies will more likely than not break your build

[Ian Jauslin]

It changes the versions to those that are specified in the lakefile. We need to have a lakefile with the correct version.
If we don't get lake update to work, then whenever we want to bump a version a mathlib, we need to edit the JSON file. That does not seem to be the best way to proceed

[Ian Jauslin]

In fact, the JSON file has the mathlib commit that used to be pointed at by 4.13. So if we revert to that commit in the lakefile, then everything should run.

[Mauricio Collares]

I think the simplest option is to bump mathlib forward to match EulerProducts. It requires no code changes. I will submit a PR.

[Mauricio Collares]

Ian Jauslin said:

In fact, the JSON file has the mathlib commit that used to be pointed at by 4.13. So if we revert to that commit in the lakefile, then everything should run.

This will cause problems for people who don't have npm installed, since ProofWidgets is missing a cloud release for this version. See #mathlib4 > cache and proofwidgets

[Ian Jauslin]

I just submitted the PR, after checking it works

[Ian Jauslin]

Yeah... The alternative I see is to revert to 4.12 while we wait for EulerProducts to be updated to the new 4.13? Is that right?

[Mauricio Collares]

I think EulerProducts will never be updated to the new 4.13 since it's already at 4.14.0-rc2. Is using only stable releases a hard requirement? Otherwise there is an easy solution, as I mentioned above.

[Ian Jauslin]

Ah, to bump to 4.14.0-rc2. Let me see if that compiles.

[Mauricio Collares]

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/207 CI just finished successfully

[Ian Jauslin]

Great thanks!

[Michael Stoll]

I should perhaps mention that EulerProducts is currently moving fairly fast, as I am PRing the orthogonality material to Mathlib (and update Mathlib in EulerProducts after each PR has been merged). I hope this will not cause further problems for PNT+.

[Kim Morrison]

I would recommend not using lake update in CI for contributor PRs. This is dangerous: it means you are moving to different versions of dependencies underneath your contributors, and they will see failures in their PRs which are unrelated to their changes.

[Kim Morrison]

lake build is sufficient to bring the dependencies to the versions that are specified in the lake-manifest.json

[Kim Morrison]

Then lake update should be run by a human who is planning on handling the fallout of the upstream repositories changing (or by a bot which commits if all goes well, or asks for help if something goes wrong).

[Alex Kontorovich]

I now see two pull requests, PNT#204 and PNT#208; are those safe to merge?

[Ian Jauslin]

Hold off on 208

[Ian Jauslin]

Let me rerun the checks on 204, to make sure they are compatible with the new version of mathlib

[Ian Jauslin]

Kim Morrison said:

I would recommend not using lake update in CI for contributor PRs. This is dangerous: it means you are moving to different versions of dependencies underneath your contributors, and they will see failures in their PRs which are unrelated to their changes.

I see. But if the contributors don't mess with the lakefile, then things should not break. And if they do mess with the lakefile in a way that breaks the compilation, shouldn't their PR be rejected?

[Alex Kontorovich]

I only ever merge things with the green checkmark. Is CI on PR's somehow doing something different from compiling once its merged...?

[Ian Jauslin]

Yeah, the green checkmark should be good enough. In this case, because we bumped up the mathlib version after the PR was submitted, the checkmark was awarded on the old version of mathlib, so I just wanted to check that the bump doesn't break the PR.

[Ian Jauslin]

Looks like it's all good, so you can go ahead and merge PR 204. I canceled 208

[Kim Morrison]

Ian Jauslin said:

But if the contributors don't mess with the lakefile, then things should not break.

If the lakefile points exclusively to tags or commit SHAs, then lake update is a noop. Otherwise, if it points to branches, then it moves the upstream repos to different commits. That's the thing you don't want happening!

[Ian Jauslin]

Right. That's why our lakefile points exclusively to tags and commit SHAs. So running lake update checks that the lake-manifest is the one corresponding to the lakefile, and wasn't changed manually. If we are doing version control through the lakefile and not the manifest, isn't that something we would want to check for? (Especially since running lake update does not have a downside given that we do not (and do not want to) point to branches?

[Kim Morrison]

Yes, you're right. I'm sorry for jumping the gun and assuming that the lakefile was pointing to upstream branches (in my defense, it's pretty common!). You're doing it right. :-)

[Alastair Irving]

I started to look at what changes would be needed to bump to Mathlib 4.14 and the latest EulerProducts. So far the biggest changes come from https://github.com/leanprover-community/mathlib4/pull/19442 which changes the notation for $C^\infty$ functions but mostly that just means replacing the notation. There's also various deprications which are easy to fix and one line which no longer compiles with Lean 4.14 (no idea why).

Is this worth doing? It would allow us to replace Abel summation in Consequences.lean with the one now in Mathlib and also keeping current with Mathlib seems like a good idea. I'm happy to keep working on this and submit a PR if it would be helpful.

[Ruben Van de Velde]

EulerProducts is at 4.14 already - do you mean 4.15?

[Ruben Van de Velde]

I think we'll definitely want to bump once 4.15 is officially released this week or next - but feel free to already make a PR with the changes you need so far

[Alastair Irving]

Sorry, I wasn't clear. I meant bumping the dependnecies of PNT to Mathlib 4.14 and to the latest EulerProducts (which as you say is already at 4.14).

[Ruben Van de Velde]

Oh no, I just didn't read properly

[Ruben Van de Velde]

Yes, good idea

[Michael Stoll]

Mathlib at version 4.14.0 should contain everything that PNT+ was using from EulerProducts, so you can probably remove EulerProducts as a dependency at this point.

[Alastair Irving]

I've got everything working with Mathlib 4.14, see https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/214 for details.

[Michael Stoll]

If you tell me which parts of EulerProducts.Auxiliary you need, I can try to get them into Mathlib.

[Ruben Van de Velde]

Michael Stoll said:

Mathlib at version 4.14.0 should contain everything that PNT+ was using from EulerProducts, so you can probably remove EulerProducts as a dependency at this point.

I did this in PNT#225. I do need explicit permission from @Michael Stoll and @Moritz Firsching to relicense the last bit of code we depend on away from the GPL, though.

I'll look at bumping after that

[Michael Stoll]

Permission granted!

[Moritz Firsching]

Permission granted!

[Ruben Van de Velde]

Michael Stoll said:

Permission granted!

Would you mind writing that on the PR as well? :)

[Alex Kontorovich]

Perfect, thank you!!

[Ruben Van de Velde]

And PNT#226 for the first bump

[Ruben Van de Velde]

And straight on to v4.16: PNT#227

[Ruben Van de Velde]

4.18: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/248

(Didn't debug why additive_combination broke)

[Ruben Van de Velde]

4.19: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/252