Std bump mess

Stream: mathlib4

[François G. Dorais]

Oh my! I think I just merged an Std bump with a bad lakefile! What's the best way to fix this?

[Eric Wieser]

Make a new PR to correct it ASAP? (And preferably add CI to catch this in future!)

[Eric Wieser]

Or maybe just create a revert the PR first, if the fix is not trivial

[François G. Dorais]

Tentative PR #8914

[François G. Dorais]

This was from a really old Std PR that just got merged. I was a bit too sleepy while prepping the Mathlib patch...

I'll add a CI test later so I don't do this one again!

[Eric Wieser]

Note that it seems @Tobias Grosser was not aware of your patch and ended up doing it from scratch themselves in another PR (but lost the race); perhaps we should put the mathlib PR into the std commit message to make it harder to miss

[François G. Dorais]

Yes, I just noticed that. It would have been easier to collaborate! It's featured in the PR itself but the commit message somehow omits it.

[François G. Dorais]

Build looks fine but CI is not quite done for #8914.

Thanks for the quick response @Eric Wieser, very much appreciated! I asked reviews form you and @Scott Morrison. Hopefully this quick patch can be rushed through before the bad PR causes any damage!

[François G. Dorais]

Thanks @Eric Wieser! I feel better now!

[Notification Bot]

François G. Dorais has marked this topic as resolved.

[Tobias Grosser]

Indeed, I missed this one. Sorry for duplicating work here. I think the conventions are actually perfectly fine. I just was not attentive enough. I now think I touched everything along the path, so expect for next time to have a better picture.

[Notification Bot]

François G. Dorais has marked this topic as unresolved.

[François G. Dorais]

No worries Tobias! We're all working toward a common goal. Little messes are part of the journey.