Zulip Chat Archive

Stream: mathlib4

Topic: lean core nightly bump


Arthur Paulino (Apr 05 2022 at 15:36):

Starting out this thread so we can post nightly bump PRs since they should be merged ASAP.

mathlib4#257 (by @Edward Ayers )

Edward Ayers (Apr 05 2022 at 15:39):

Maybe it's a sensible policy that as long as the CI passes and no really big changes are happening in the PR for a nightly bump it's ok to merge? @Gabriel Ebner does that sound ok?

Arthur Paulino (Apr 05 2022 at 15:41):

Still good to post though, just to make everyone aware that we're up to date

Mario Carneiro (Apr 05 2022 at 16:11):

yeah I don't think we need to chronicle these

Arthur Paulino (Apr 05 2022 at 16:17):

Some bumps do need reviews tho. I'll be posting the ones I make here

Gabriel Ebner (Apr 05 2022 at 16:37):

Maybe it's a sensible policy that as long as the CI passes and no really big changes are happening in the PR for a nightly bump it's ok to merge?

Yes, that's perfectly ok. Please bors r+ them as you see fit. mathlib4#254 has/had some nontrivial changes though, so it was good to wait for reviews.


Last updated: Dec 20 2023 at 11:08 UTC