LinearPMap properties removed by toolchain bump

Stream: mathlib4

[Moritz Doll]

Hi,
I've noticed that some properties I've proved in mathlib4#6537 were removed during a toolchain bump mathlib4#7703 and mathlib4#7710. Following that there were a couple of commit that reverted (and subsequently restored that commit.
The file in question is Mathlib/Analysis/InnerProductSpace/LinearPMap.lean and the commits are

• 26eb2b0ade1d7e252d07b13ea9253f9c8652facd
• f3695eb20c685cfcb5e45f75b1e68a59b8de7efb
• 26eb2b0ade1d7e252d07b13ea9253f9c8652facd
• f3695eb20c685cfcb5e45f75b1e68a59b8de7efb
• ab56fa28da38a962b7952fc9e52edb14bef2bc5a
  I have no idea what was going on there, and I wonder whether there was more lost in the chaos @Kim Morrison @Matthew Ballard

[Matthew Ballard]

I think you are going to have to dig in the nightly testing branch to see if the change can be localized more. My memory of my PR was that something was broken with the new toolchain and we needed to go back very briefly.

[Matthew Ballard]

The value of expressive PR descriptions...

[Matthew Ballard]

Oh wait, I just glazed past the commit hashes

[Moritz Doll]

Yeah, I found something related to the Lean server crashing, but reverting mathlib commits that just happen to be merged in that timeframe is not ideal.

[Matthew Ballard]

That is odd.

[Matthew Ballard]

I am guessing I wasn't up of date and git didn't catch it. Actually I don't know what happened here. Apologies. Can you look at https://github.com/mattrobball/mathlib4_fork/tree/fix_7f121a4 and make sure everything looks in order?

[Matthew Ballard]

This is not a PR yet in the case you want rework the git history to remove me from the authoring.

[Moritz Doll]

Can you check whether there where more commits that got removed, I am on mobile, so it would be a pain? Mine looks good. I don't care about the github authorship :smile: also thanks for fixing it so quickly

[Matthew Ballard]

I am looking now at that now

[Matthew Ballard]

Ok, I figured it out. Yours is the only commit that got sandwiched between bumping the std/batteries dependency and the toolchain itself and probably got lost in the continuous reconciliation process that is nightly testing.

[Matthew Ballard]

Then each commit after was revert/revert-revert of that

[Bryan Gin-ge Chen]

Do we need tooling to make sure this doesn't happen again? (Are we sure it hasn't happened before?)

[Matthew Ballard]

In theory we should freeze commits to master X hours before a bump

[Matthew Ballard]

For some X

[Matthew Ballard]

#29595

[Bryan Gin-ge Chen]

It is possible to manually turn on/off bors and prevent new commits for a while; we could add it to a script too if necessary.

[Matthew Ballard]

Does bors remember calls while it is sleeping?

[Matthew Ballard]

This has to be a solved problem

[Bryan Gin-ge Chen]

If something is in the queue and finishes its build while bors is offline, then we might have to re-run it.

[Bryan Gin-ge Chen]

If it's offline, it's not listening for calls.

[Bryan Gin-ge Chen]

Actually, it might not be too hard to build in a mode where we pause it pushing to master for a while.

[Matthew Ballard]

Maybe not for bors in particular but don't merge anything in some time frame before some set of events is a universal problem

[Matthew Ballard]

Ah right the phrase is "feature freeze"

[Kim Morrison]

Sorry, does someone understand what happened here?

[Eric Wieser]

Moritz Doll said:

and the commits are

• 26eb2b0ade1d7e252d07b13ea9253f9c8652facd - chore: bump toolchain to v4.2.0-rc2 (#7703)
• f3695eb20c685cfcb5e45f75b1e68a59b8de7efb - chore: revert #7703 (#7710)
• ab56fa28da38a962b7952fc9e52edb14bef2bc5a - Revert "chore: revert #7703 (#7710)"

Linked and with duplicates removed for convenience

[Matthew Ballard]

Matthew Ballard said:

Ok, I figured it out. Yours is the only commit that got sandwiched between bumping the std/batteries dependency and the toolchain itself and probably got lost in the continuous reconciliation process that is nightly testing.

@Kim Morrison