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

[Ruben Van de Velde]

@Yaël Dillies could you take look at the deprecations in https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/253 (Nat.Icc_succ_left etc)? The replacements don't seem to work because of confusion between SuccOrder.succ and Nat.succ

[Yaël Dillies]

Deprecating lemmas properly would have either involved significantly increasing imports or moving the deprecated lemmas elsewhere (mostly nullifying the point of deprecation)

[Yaël Dillies]

Therefore the deprecated lemmas point to the correct lemmas up to Order.succ n = n + 1

[Yaël Dillies]

If you replace succ/pred with add_one/sub_one in the relevant lemma names and add more imports if necessary, then everything will work as expected

[Ruben Van de Velde]

Oh, there's add_one variants too? Those might have been better deprecation targets. Thanks for the pointer!

[Ruben Van de Velde]

Also, should there be a lemma about what SuccOrder.succ means on Nat? I didn't find it

[Yaël Dillies]

It's docs#Nat.succ_eq_succ or docs#Order.succ_eq_add_one, depending on what you want the RHS to be

[Ruben Van de Velde]

Wait, what's the relation between Order.succ and SuccOrder.succ?

[Yaël Dillies]

docs#SuccOrder.succ is an implementation detail for docs#Order.succ

[Bhavik Mehta]

Yaël Dillies said:

Deprecating lemmas properly would have either involved significantly increasing imports or moving the deprecated lemmas elsewhere (mostly nullifying the point of deprecation)

I don't see why it forces either of those: the deprecation message can point to the lemma we actually want to deprecate in favour of, it doesn't need to import that one. (I also ran into the problem of these deprecations being unhelpful)

[Ruben Van de Velde]

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/314 for 4.21

[Ruben Van de Velde]

Working on 4.22

[Ruben Van de Velde]

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

[Alex Kontorovich]

Thank you!

[Ruben Van de Velde]

@Alex Kontorovich , could I have a review on https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/387 ?

[Ruben Van de Velde]

Ruben Van de Velde said:

Alex Kontorovich , could I have a review on https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/387 ?

Ping

[Alex Kontorovich]

Oh sorry, I left a whole bunch of notes in the review; did you have a chance to look through them? (Basically lots of non-terminal simps)

[Ruben Van de Velde]

I don't see it - did you submit them? The nonterminal simps are mostly preexisting (as field_simp), and I was planning to fix them in a followup PR, but I can do them here as well if you prefer

[Alex Kontorovich]

Strange; this is what I see on github; do you not see the same?
image.png
I don't think field_simp counts as a non-terminal simp, does it? I suppose it too could change in the future (and just did...), so it should also not be terminal. Anyway, if you're planning on fixing that in a follow-up, that's fine with me, I can merge as is; please let me know. Thanks!

[Rémy Degenne]

The "pending" word next to your review messages means that you have not submitted your review yet, and they are only visible to you.

[Alex Kontorovich]

Ha! :) What an idiot. One day I'll learn to use github....

[Ruben Van de Velde]

That tag could be more prominent :)

[Ruben Van de Velde]

I should have time to look at them tonight

[Kevin Buzzard]

Alex Kontorovich said:

Ha! :)

You're certainly not the only person to have done this! (indeed some of us have fallen into this trap more than once...)

[Ruben Van de Velde]

@Alex Kontorovich should be better now

[Ruben Van de Velde]

4.24: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/403

[Alex Kontorovich]

Thank you!!

[Ruben Van de Velde]

4.25: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/412 (wip; heading off now in case anyone wants to take a look)

[Ruben Van de Velde]

Should build now

[Alex Kontorovich]

Great thank you!!

[Ruben Van de Velde]

Hoping https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/418 is the last one this cycle

[Alex Kontorovich]

Something happened with the latest PR that's giving a strange error message: error: could not download nonexistent lean version leanprover/lean4:v4.25.1`` Can anyone please help figure out what went wrong? Thank you!

[Ruben Van de Velde]

Seems like someone deleted the tag - cc @Kim Morrison

[Julian Berman]

The URL being downloaded from is very strange, it has https://releases.lean-lang.org/lean4/v4.25.1/lean-4.25.0-linux.tar.zst in it so something clearly is confused about the version number, but yeah it does seem clear that that URL worked previously in the last successful build.

[Kim Morrison]

It's been fixed in the meantime. Sorry this caught you out. :woman_facepalming:

[Alex Kontorovich]

No worries, thanks for your help! Rerunning failed jobs now...

[Alex Kontorovich]

Oops now the error is: uncaught exception: Failed to fetch ProofWidgets cloud release: lake failed with error code 1?

[Kim Morrison]

Can you tell us what state you're in? e.g. a commit at some repo, and a command to run to observe this error?

[Alex Kontorovich]

This is the build on main: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/

[Alex Kontorovich]

Here's the full error message: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/actions/runs/19668741297/job/56413302297

[Alex Kontorovich]

Thanks for your help!

[Alex Kontorovich]

CCing @Ian Jauslin as we have some non-standard features set up...

[Alastair Irving]

I get the same error if I build locally. There seems to be a confusion of tags between mathlib and proofwidgets and I haven't managed to find a combination which works:

• Currently PNT points at mathlib v4.25.1. That tag no longer exists but we still have the hash in the lake-manifest. However That mathlib version points at a proofwidgets for which there isn't a tagged release and that's why we're getting an error.
• I thought the fix should be to update to mathlib 4.25.2. The v4.25.2 mathlib tag exists but points at a proofwidgets commit which has been force pushed over. There's also a branch of mathlib, releases/v4.25 which maybe points at a correct proof widgets. That seems to work but it would maybe be best if the tag was updated and we used that rather than pointing at a branch.

[Alastair Irving]

It looks like @Kim Morrison fixed the tags, thank you. I've ran lake update and created https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/422 which builds.

I thought about bumping to V4.25.2 at the same time but that didn't work because there isn't a corresponding tag on Docgen4.

[Eric Rodriguez]

for docgen you should be able to use the v4.25.1 tag with few issues I would think

[Ruben Van de Velde]

I don't know what the deal is this release cycle, but bumping to 4.25.2 fixes the cache for me locally - https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/425

[Ruben Van de Velde]

https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/pull/429 is open for 4.26