batteries#887 breaking Mathlib

Stream: batteries

[Kim Morrison]

@Matthew Ballard, @Mario Carneiro, Mathlib needs adaptations for batteries#887. The automatic bump process is reporting failures: https://leanprover.zulipchat.com/#narrow/stream/345428-mathlib-reviewers/topic/Mathlib.20.60lake.20update.60.20failure/near/472580810

[Kim Morrison]

(Also noting that batteries changes that Mathlib needs adapation for also break Mathlib's nightly-testing branch, and hence delay being able to test Lean PRs against Mathlib.)

[Mario Carneiro]

point me to what to do to avoid messing up your process

[Kim Morrison]

In some form, we need to have adaptations for Mathlib ready to go.

1. We could do this manually: if a maintainer judges that it is likely that a change will break Mathlib, we ask if there is an adaptation ready before merging.
2. We could automate this, like Lean automatically tests Batteries and Mathlib. That is, a CI process would continue after normal Batteries CI completes, creating a batteries-pr-testing-NNNN branch of Mathlib and updating the lakefile there to depend on the PR branch of Batteries. Then run normal CI on that branch, and report back via a label breaks-mathlib or builds-mathlib on the Batteries branch.
3. Or we could do this reactively -- the notifications are all already in place --- by having enough people watching the Mathlib update failures topic or the Mathlib status updates topic in #nightly-testing to notice when Batteries has introduced a Mathlib breakage, and fixing it promptly. (Here "enough" just means "not primarily me". :-)

[Kim Morrison]

Ideally, we can do all three. 1. will mostly stop things breaking, and 3. will backstop that when needed. If we can get started (either implementing or asking for help) on 2., that can gradually take the workload off maintainers.

[Kim Morrison]

But I think we need to do at least one!

[Mario Carneiro]

is there a way to make this fail in the merge queue?

[Kim Morrison]

So, variants of 2. would be possible, where rather than just reporting back with labels, we actually fail a CI check (that is either run all the time, or --- as you suggest --- only in the merge queue) if Mathlib doesn't cleanly adapt.

[Mario Carneiro]

How does lean core do it? Seems like breaking changes are merged all the time without adaptations ready to go

[Kim Morrison]

Yes, just judgement about whether testing is needed. If you want downstream testing, then you make sure your PR is based off nightly-with-mathlib (which is a branch tracking the most recent nightly for which we know Mathlib succeeds).

[Mario Carneiro]

For this PR, I expect the adaptations to be very simple, since it's just a rename in some namespaces that will be used in a handful of tactics

[Kim Morrison]

If you don't want downstream testing (either because you're confident it isn't needed, because you know Mathlib is currently badly out of sync (thankfully this is rare recently), or because you know that I'm available to clean up), then you don't base off nightly-with-mathlib, and instead the bot just reports that it isn't going to test Batteries+Mathlib.

[Kim Morrison]

Yes, for this PR option 3. above is perfectly fine. Just I'd like it to happen without me be the sole person to notice it needs to happen. :-)

[Kim Morrison]

(i.e. option 3 is only fine if the "enough" clause there holds!)

[Kim Morrison]

Note a virtuous cycle here: the more often Mathlib is compatible with lean's nightlies, the higher expectations Lean PR authors will have that testing against Mathlib will give useful signal, and the more likely they are to do the testing, and thus have adaptations (at either the Mathlib or Lean end!) ready before merging.

[Kim Morrison]

Okay, I am going to go fix this manually now.

[Kim Morrison]

#17117

[Kim Morrison]

and cherry-picked onto nightly-testing.

[Kim Morrison]

Ooops, and my local build found another problem, which I've now deployed in both places.

[Matthew Ballard]

@Kim Morrison sorry messing up the process and thanks for fixing it.

I asked earlier about handling downstream breakage (of course not thinking it was in process) so it is good to get some answers and plans to make things smoother (hopefully).

Is there anyway to get that Zulip message from the bump automation to be more specific about what is being bumped?

[Kim Morrison]

I guess we could have the bot link to the diff on the lake-manifest.json?

[Kim Morrison]

It is usually 75% batteries, 25% aesop, at least recently.

[François G. Dorais]

Is there a convenient way to trigger 2 on-demand? (The manual process is time consuming and prone to error.)

[Kim Morrison]

@François G. Dorais, option 2. for a Batteries PR doesn't exist at all at the moment. Are you talking about for a Lean PR? What would "on demand" look like?

[François G. Dorais]

Could be triggered by a maintainer or by the author on a case by case basis. For example, if I believe a PR might break Mathlib but I'm not sure how, then I could press the button to create a batteries-pr-testing-NNNN branch to check it out. (But it might be easier to do it for all PRs.)

[Kim Morrison]

Yeah, seems easier to do it for everything than for some!

[François G. Dorais]

Agreed, I was mostly wondering if it already existed and I had been missing out.

[Kim Morrison]

No, this all exists for Lean, but no where else.

[François G. Dorais]

It would be great to have that for Batteries but I'm not sure about the implementation costs. It doesn't look like an easy task at all even though a working model already exists in Lean.

[Kim Morrison]

I think would just be a matter of copying .github/workflows/pr-release.yml (from the lean4 repo), dropping everything before line 284, and adapting a bit.

[Kim Morrison]

We'd also need to update at the mathlib end to report back to Batteries for failures on batteries-pr-testing-NNNN branches.

[Kim Morrison]

I think it would suffice to just always test Mathlib master, so it's actually a good bit simpler than the Lean case.

[Kim Morrison]

If someone could sanity check batteries#958, that is hopefully most of what is needed.

[Kim Morrison]

#17144 is the mathlib end of it.

[Kim Morrison]

Again, sanity check please, and then I'll set up the tokens and we can test in production.

[François G. Dorais]

That was really fast! LGTM

[Johan Commelin]

Kim Morrison said:

#17144 is the mathlib end of it.

LGTM

[Kim Morrison]

Okay, I will install tokens soon!

[Kim Morrison]

Hmm, we did it again, and batteries#956 breaks Mathlib and nightly-testing.

[Kim Morrison]

:-(

[François G. Dorais]

Looks like this is just about deleting the lemmas from Mathlib.Data.List.OfFn that were moved to Batteries as well as the obsolete _go lemmas. So I just need to do that directly on nightly-testing. Is there some kind of signal so that we don't step on each other's toes?

[François G. Dorais]

Got it. I figured out the workflow.

[Kim Morrison]

Where did length_ofFn go?

[Kim Morrison]

In this case we shouldn't be touching nightly-testing.

[Kim Morrison]

It's getting lake update to work on master that is the problem.

[Kim Morrison]

Fixing that and nightly-testing will come good automatically.

[François G. Dorais]

It's on Batteries now.

[Matthew Ballard]

Protected? never mind

[Kim Morrison]

Unfortunately the bot that posts about lake update breakages on master is in a private stream that @François G. Dorais doesn't have access to.

[Kim Morrison]

I'll work out how to make that happen.

[Kim Morrison]

Oh, it's just imports that need fixing, in that case.

[Kim Morrison]

We need to import Batteries.Data.List.OfFn at the right place in Mathlib.

[François G. Dorais]

Yes, I'm fixing that now.

[Kim Morrison]

And I'm getting you access to things. :-)

[François G. Dorais]

Got it. I just push on nightly-testing directly or is there an intermediate step?

[Kim Morrison]

Ah, as I was saying above, it's better to fix this on master

[Kim Morrison]

i.e. a PR in which we lake update and then do this fix.

[Kim Morrison]

hopefully you could just take whatever change you've got and transplant it over

[Kim Morrison]

(If we fix it directly on master, a bot will merge the change to nightly-testing. If we just fix on nightly-testing, master will still need manual updating.)

[Kim Morrison]

(but besides that point yes, you are welcome to push direct to nightly-testing)

[François G. Dorais]

That makes sense!

[François G. Dorais]

#17159

[Kim Morrison]

Don't you also need a change in List.FinRange, since List.getElem_ofFn is protected now?

[Kim Morrison]

but with that :peace_sign: :-)

[François G. Dorais]

OK. It will take a bit to internalize the workflow but I will definitely be able to help more going forward.

[Kim Morrison]

Just a heads up that I have installed all the requisite tokens and secrets, and merged batteries#958 and #17144.

[Kim Morrison]

In an ideal world, this will result in every PR to Batteries automatically generating a batteries-pr-testing-NNNN branch on Mathlib which uses that PR, and then Mathlib CI reporting back with a label breaks-mathlib or builds-mathlib.

[Kim Morrison]

In the real world, where we have to test Github CI in production, none of this will work.

[Kim Morrison]

I don't have time right now to test this, but if no one else has in a few hours time I should be able to later today.

[Kim Morrison]

A fair number of fixes later, I think batteries#960 has demonstrated that it basically works!

[François G. Dorais]

batteries#966 was just labeled builds-mathlib!

[François G. Dorais]

And batteries#854 was labeled builds-mathlib after an update.

[François G. Dorais]

It's confirmed that batteries#960 works as intended in real life!

[François G. Dorais]

It already caught an unexpected error in batteries#948. (Not a major one, just a test that needs an update.)

[Edward van de Meent]

I'd like to mention that this change means https://leanprover-community.github.io/contribute/tags_and_branches.html may need an update about this feature, since it's not clear with whom the responsibilty for fixing the breaking change lies, and where/how this should be solved. i started a discussion of this in #mathlib4 > workflow for fixing breaking changes to Batteries , but feel free to move it here if that is more appropriate