merging master into bump/v4.8.0

Stream: nightly-testing

[Ruben Van de Velde]

I can take a look at merging master into bump/v4.8.0, unless you already started

[Kim Morrison]

That would be great. Dinner time here.

[Kim Morrison]

If merging master itself goes badly, we can instead try whichever commit on master bump/nightly-2024-04-14 came from. (That might be a chore to identify anyway...)

[Ruben Van de Velde]

It's a bit annoying, but not terrible so far

[Ruben Van de Velde]

Making good progress, hoping to have something that builds later today

[Notification Bot]

5 messages were moved here from #nightly-testing > #11997, adaptations for nightly-2024-04-07 by Ruben Van de Velde.

[Ruben Van de Velde]

https://github.com/leanprover-community/mathlib4/tree/merge-bump/v4.8.0 is green. I think it'd be best if a maintainer fast-forward merged it into bump/v4.8.0 manually; not sure what github would make of it.

[Kim Morrison]

Ruben Van de Velde said:

https://github.com/leanprover-community/mathlib4/tree/merge-bump/v4.8.0 is green. I think it'd be best if a maintainer fast-forward merged it into bump/v4.8.0 manually; not sure what github would make of it.

Done!

[Kim Morrison]

bump/v4.8.0 still builds after the merge, thanks @Ruben Van de Velde!

[Kim Morrison]

I think the next step is merging bump/v4.8.0 into bump/nightly-2024-04-14. There are about 30 conflicts. I have a few things to do first, but hopefully in a few hours I can tackle this. If anyone is keen please go ahead. :-)