workflow for fixing breaking changes to Batteries

Stream: mathlib4

[Edward van de Meent]

Last week, a workflow has been added for PRs to Batteries to be automatically tested against mathlib, but i don't know there has been a discussion on how to proceed when a breaking change is suggested.

In the particular case i'm working with (Batteries#948), it is the case that a mathlib test (for the #help command, i.e. in ./test/help_cmd.lean) now fails due to the addition of a command with syntax for which "#chec" is a prefix.

The adaptation for mathlib is easy, adding the reported documentation to the expected message in the test, and i have a commit to that effect ready, to be added on top of branch#batteries-pr-testing-948 ...

How should we proceed?

[Edward van de Meent]

Edward van de Meent said:

to be added on top of branch#batteries-pr-testing-948

or maybe there should be a branch nightly-batteries-testing for such fixes to be added on top of, once it's merged into batteries?

[Edward van de Meent]

also feel free to move this topic elsewhere if this was not the appropriate place to ask this question...

[François G. Dorais]

Actually, the feature was added yesterday! batteries#948 was the first PR to "unintentionally" test it.

[François G. Dorais]

There hasn't been much discussion about this. The plan was to add this tool to give Batteries maintainers a heads up that there will be a Mathlib adaptation after a PR is merged.

[François G. Dorais]

Of course, nobody would complain if a user proposed an adaptation instead.

[Mario Carneiro]

The mathlib test for #help should be migrated to batteries in the same PR that migrates #help itself

[Kim Morrison]

The workflow that would result in the least work for others would be:

• if you get a breaks-mathlib label, push changes to batteries-pr-testing-NNNN until you get a builds-mathlib (or ask for help if you can't)
• then open a PR to Mathlib from that branch, adding the depends-on-batteries-PR label, linking to the batteries PR, and ask for a delegation
• (This label doesn't prevent things being on the #queue, right?)
• Once the Mathlib PR is delegated, a maintainer can merge the Batteries PR
• and then the author can change the batteries branch on the Mathlib PR back to main and hit merge (or anyone can do this step if needed to avoid a breakage in to the automatic lake update processes on Mathlib's master and nightly-testing branches)

[François G. Dorais]

That requires a lot of responsiveness from the users. Especially the last two steps require a fair amount of timeliness.

[François G. Dorais]

I would change the first step to:

• if you get a breaks-mathlib label, don't worry, that's not necessarily unexpected
• after the review process, a maintainer may ask you to assist with a Mathlib adaptation PR

[Kim Morrison]

Hmm, I disagree, that will just push the work back on maintainers.

The breaks-mathlib label should come with much better explanation of what the author needs to do next, of course.

[François G. Dorais]

How about this:

• if you get a breaks-mathlib label, don't worry, that's not necessarily unexpected and there is nothing to do until the review process has completed
• after the review process, a maintainer will ask you to make a Mathlib adaptation PR, if necessary

I don't want users to worry about the breaks-mathlib label until after the review process.

[François G. Dorais]

I guess the Batteries maintainer could do the last few steps on the Mathlib side (i.e. point batteries in the lakefile back to main, run lake update batteries, and ask bors to merge). That way there's not too much need for timeliness in the last step.

[François G. Dorais]

In fact, that can be simplified to two easy steps for the maintainer by packing editing lakefile, running lake update batteries and push in a script that we sneak into every batteries-pr-testing-NNNN branch.

[François G. Dorais]

I don't know much about bors but perhaps it can be used to simplify further to one easy step?

[Kim Morrison]

Yes, we really should have a bot that will detect when a Batteries PR is merged, and if there is a delegated PR from the corresponding batteries-pr-testing-NNNN branch, just sends it to bors...

[Kim Morrison]

(A little scary having a bot run bors merge...?)

[Kim Morrison]

Maybe that's too much, and better is just that the bot posts in #mathlib reviewers asking for someone to merge.

[Kim Morrison]

François G. Dorais said:

I don't want users to worry about the breaks-mathlib label until after the review process.

I think I disagree here. Certainly we don't have enough documentation / automatic explanation of what you're meant to do, but I'd prefer this work is by default belonging to the authors, not the maintainers.

[François G. Dorais]

Kim Morrison said:

François G. Dorais said:

I don't want users to worry about the breaks-mathlib label until after the review process.

I think I disagree here. Certainly we don't have enough documentation / automatic explanation of what you're meant to do, but I'd prefer this work is by default belonging to the authors, not the maintainers.

There's too much other stuff to worry about in the early stages of a PR. The user should focus on making the PR suitable for Batteries. Working on the Mathlib adaptation is only relevant after that's achieved, it's a waste of time to work on that before.

[François G. Dorais]

Making the builds-mathlib criterion a target will more than likely decrease the utility of the criterion. Users will be encouraged to use quick but mediocre solutions just to pass the test, or create extremely messy solutions because of dozens of pointless edits. I strongly prefer to deemphasize the builds-mathlib tag early on in the PR process.

[Edward van de Meent]

I'd say that since mathlib depends on batteries, surely it's not the responsibility of a batteries contributor to also make sure mathlib builds?

[Edward van de Meent]

And although it is nice to have as little breakage as possible, that should not withhold us from making some changes

[Kim Morrison]

If we merge a Batteries PR that will break Mathlib, in practice that means most times I get to fix it. At present Batteries and Mathlib are too tightly coupled, and many things are unpleasant if they get out of sync. So I'm not planning on merging anything where I expect Mathlib to break, and the fix not to be available!

[Kim Morrison]

^most: at least, over the last year. Not necessarily going forward. :-)

[Kim Morrison]

Kim Morrison said:

So I'm not planning on merging anything where I expect Mathlib to break, and the fix not to be available!

This is still compatible with François' preference above that during initial review there is no need to get Mathlib fixed. It would mean that there's a later stage of review where we get this sorted.

[François G. Dorais]

Kim Morrison said:

Kim Morrison said:

So I'm not planning on merging anything where I expect Mathlib to break, and the fix not to be available!

This is still compatible with François' preference above that during initial review there is no need to get Mathlib fixed. It would mean that there's a later stage of review where we get this sorted.

I've tested the bot on a bunch a lot of recent PRs. I've seen both false positives and false negatives. The error rate is significant and sometimes for really menial issues like network errors.

I think we can all agree that this needs to be a two-stage process where users are instructed to ignore the builds-mathlib/breaks-mathlib tags until a maintainer says that a Mathlib adaptation is needed. Then, the maintainers will not merge until the Mathlib adaptation is ready.

Now we need to hash out the implementation of this two-stage review process.

[Kim Morrison]

Let's see if we can fix the some of the false positive / negatives!

[François G. Dorais]

They were all very contextual so fixing is not really an option.

• The false builds-mathlib were because no part of Mathlib imported both the conflicting parts of Batteries and Mathlib. This is a consequence of minimizing imports, which should not be compromised for the purpose of this test.
• There were many false causes for breaks-mathlib. One was a network error (rare and not hard to diagnose). Most were because Mathlib itself wasn't quite up to date when the check started.

In almost all cases I've observed, there was no systematic thing that the bot could reasonably do to fix the error.

[Kim Morrison]

For the first problem, I don't understand. There's a test file that imports Mathlib and Batteries.

[François G. Dorais]

This is batteries#969. This is an unusual case. Just importing Mathlib and Batteries isn't enough since the two help commands are in different namespaces.

[Kim Morrison]

Okay, in that case it sounds like on acceptable false positive.