Zulip Chat Archive

Stream: nightly-testing

Topic: Mathlib bump branch reminders

github mathlib4 bot (Apr 17 2024 at 09:16):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-04-16 branch from nightly-testing, and then PR that to "bump/v4.8.0".

github mathlib4 bot (Apr 17 2024 at 11:24):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-04-17 branch from nightly-testing, and then PR that to "bump/v4.8.0".

github mathlib4 bot (Apr 18 2024 at 02:23):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-04-17 branch from nightly-testing, and then PR that to "bump/v4.8.0".

github mathlib4 bot (Apr 18 2024 at 04:09):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-04-17 branch from nightly-testing, and then PR that to "bump/v4.8.0".

github mathlib4 bot (Apr 18 2024 at 07:47):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-04-17 branch from nightly-testing, and then PR that to "bump/v4.8.0".

github mathlib4 bot (Apr 19 2024 at 07:02):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-04-17 branch from nightly-testing, and then PR that to "bump/v4.8.0".

github mathlib4 bot (Apr 19 2024 at 14:01):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-04-19 branch from nightly-testing, and then PR that to "bump/v4.8.0".

Ruben Van de Velde (Apr 19 2024 at 14:44):

github mathlib4 bot said:

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-04-19 branch from nightly-testing, and then PR that to "bump/v4.8.0".

#12271

github mathlib4 bot (Apr 19 2024 at 16:46):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-04-19 branch from nightly-testing, and then PR that to "bump/v4.8.0".

github mathlib4 bot (Apr 19 2024 at 19:10):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-04-19 branch from nightly-testing, and then PR that to "bump/v4.8.0".

github mathlib4 bot (Apr 20 2024 at 09:13):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-04-19 branch from nightly-testing, and then PR that to "bump/v4.8.0".

Ruben Van de Velde (Apr 20 2024 at 10:51):

It looks like I need to take another look at that bot

github mathlib4 bot (Apr 20 2024 at 11:21):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-04-20 branch from nightly-testing, and then PR that to "bump/v4.8.0".

github mathlib4 bot (Apr 22 2024 at 01:35):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-04-21 branch from nightly-testing, and then PR that to "bump/v4.8.0".

github mathlib4 bot (Apr 22 2024 at 02:44):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-04-21 branch from nightly-testing, and then PR that to "bump/v4.8.0".

github mathlib4 bot (Apr 28 2024 at 01:13):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-04-25 branch from nightly-testing, and then PR that to "bump/v4.8.0".

github mathlib4 bot (May 01 2024 at 05:36):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-04-30 branch from nightly-testing, and then PR that to "bump/v4.8.0".

github mathlib4 bot (May 02 2024 at 03:25):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-01 branch from nightly-testing, and then PR that to "bump/v4.8.0".

github mathlib4 bot (May 08 2024 at 11:19):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-08 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 08 2024 at 13:42):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-08 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 08 2024 at 16:35):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-08 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 08 2024 at 19:31):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-08 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 08 2024 at 22:16):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-08 branch from nightly-testing, and then PR that to "bump/v4.9.0".

Kim Morrison (May 09 2024 at 01:00):

bad bot :-)

github mathlib4 bot (May 09 2024 at 04:37):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-08 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 09 2024 at 07:26):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-08 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 09 2024 at 09:58):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-09 branch from nightly-testing, and then PR that to "bump/v4.9.0".

Kim Morrison (May 09 2024 at 11:31):

#12782

Kim Morrison (May 09 2024 at 11:31):

(also backports of two files to master in #12783, but I don't think either needs to wait for the other)

github mathlib4 bot (May 09 2024 at 13:42):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-09 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 09 2024 at 15:59):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-09 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 09 2024 at 19:03):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-09 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 10 2024 at 01:55):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-09 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 10 2024 at 03:58):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-09 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 13 2024 at 01:51):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-11 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 13 2024 at 03:42):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-11 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 13 2024 at 07:45):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-11 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 13 2024 at 10:03):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-11 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 13 2024 at 13:49):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-11 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 13 2024 at 16:35):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-11 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 13 2024 at 19:46):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-11 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 14 2024 at 11:07):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-14 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 15 2024 at 00:20):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-14 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 15 2024 at 01:50):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-14 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 15 2024 at 04:48):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-14 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 15 2024 at 11:16):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-15 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 15 2024 at 13:50):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-15 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 15 2024 at 16:00):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-15 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 15 2024 at 19:43):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-15 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 15 2024 at 22:00):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-15 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 16 2024 at 01:59):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-15 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 16 2024 at 03:59):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-15 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 17 2024 at 02:33):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-16 branch from nightly-testing, and then PR that to "bump/v4.9.0".

Kim Morrison (May 17 2024 at 03:08):

No need for this branch, after #12969 nightly-testing and bump/v4.9.0 will be in sync besides the toolchain.

github mathlib4 bot (May 17 2024 at 04:44):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-16 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 20 2024 at 12:41):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-20 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 20 2024 at 13:36):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-20 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 20 2024 at 19:34):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-20 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 20 2024 at 22:46):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-20 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 21 2024 at 01:11):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-20 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 21 2024 at 03:53):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-20 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 21 2024 at 07:05):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-20 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 21 2024 at 13:54):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-21 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 21 2024 at 15:49):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-21 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 21 2024 at 19:20):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-21 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 21 2024 at 22:23):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-21 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 22 2024 at 01:32):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-21 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 22 2024 at 04:30):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-21 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 22 2024 at 07:24):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-21 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 22 2024 at 11:06):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-22 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 22 2024 at 13:02):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-22 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 22 2024 at 16:30):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-22 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 22 2024 at 19:27):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-22 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 22 2024 at 22:25):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-22 branch from nightly-testing, and then PR that to "bump/v4.9.0".

Mario Carneiro (May 22 2024 at 23:00):

I think the bot is trying to tell us something... :thinking:

Kim Morrison (May 22 2024 at 23:33):

I think I'm just going to turn this one off. It is only marginally useful even if it only said something at the right time.

Kim Morrison (May 22 2024 at 23:38):

Hmm, actually, it was a useful reminder. I thought I had already done #13129, but apparently not!

github mathlib4 bot (May 22 2024 at 23:58):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-22 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 23 2024 at 01:30):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-22 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 23 2024 at 04:29):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-22 branch from nightly-testing, and then PR that to "bump/v4.9.0".

Kim Morrison (May 23 2024 at 04:30):

Hmm, #13129 has been merged, so the bot really should have shut up by now. :-(

github mathlib4 bot (May 23 2024 at 07:17):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-22 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 23 2024 at 13:53):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-23 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 23 2024 at 15:57):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-23 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 23 2024 at 22:22):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-23 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 24 2024 at 01:01):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-23 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 24 2024 at 12:17):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-24 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 24 2024 at 13:36):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-24 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 26 2024 at 15:03):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-25 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 28 2024 at 13:36):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-28 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 29 2024 at 11:11):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-29 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 29 2024 at 13:00):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-29 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 29 2024 at 16:01):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-29 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 30 2024 at 11:24):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-30 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 30 2024 at 13:40):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-30 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 31 2024 at 11:25):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-31 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 31 2024 at 13:37):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-31 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (May 31 2024 at 14:54):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-31 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 01 2024 at 12:52):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-31 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 01 2024 at 16:37):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-31 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 01 2024 at 19:16):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-31 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 01 2024 at 22:07):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-31 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 02 2024 at 01:27):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-31 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 02 2024 at 03:51):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-31 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 02 2024 at 09:48):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-05-31 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 03 2024 at 13:57):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-02 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 03 2024 at 16:29):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-02 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 03 2024 at 19:12):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-02 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 03 2024 at 22:38):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-02 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 04 2024 at 01:14):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-02 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 04 2024 at 02:23):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-02 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 04 2024 at 22:56):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-04 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 05 2024 at 02:11):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-04 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 06 2024 at 04:58):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-05 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 06 2024 at 06:23):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-05 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 06 2024 at 13:03):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-06 branch from nightly-testing, and then PR that to "bump/v4.9.0".

github mathlib4 bot (Jun 16 2024 at 02:40):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-15 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 16 2024 at 07:13):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-15 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 17 2024 at 02:29):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-16 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 17 2024 at 11:05):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-17 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 17 2024 at 13:42):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-17 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 17 2024 at 15:57):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-17 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 17 2024 at 19:29):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-17 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 17 2024 at 22:30):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-17 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 18 2024 at 08:54):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-17 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 20 2024 at 05:36):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-19 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 20 2024 at 06:50):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-19 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 20 2024 at 09:46):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-19 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 20 2024 at 13:43):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-19 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 20 2024 at 16:10):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-19 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 20 2024 at 19:21):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-19 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 20 2024 at 22:00):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-19 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 21 2024 at 02:22):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-19 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 21 2024 at 03:45):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-19 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 22 2024 at 12:02):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-22 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 22 2024 at 13:10):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-22 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 23 2024 at 01:48):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-22 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 23 2024 at 03:46):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-22 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 23 2024 at 06:49):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-22 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 24 2024 at 02:56):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-23 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 24 2024 at 04:29):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-23 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 24 2024 at 11:14):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-24 branch from nightly-testing, and then PR that to "bump/v4.10.0".

Kim Morrison (Jun 24 2024 at 11:16):

@Johan Commelin, I'll leave today's one for you again. :-)

github mathlib4 bot (Jun 25 2024 at 11:57):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-25 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 25 2024 at 13:39):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-25 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 25 2024 at 16:39):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-25 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 25 2024 at 19:09):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-25 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 25 2024 at 22:03):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-25 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 27 2024 at 05:33):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-26 branch from nightly-testing, and then PR that to "bump/v4.10.0".

Kim Morrison (Jun 27 2024 at 05:36):

@Johan Commelin I'll let you run the newly landed script from #14178!

github mathlib4 bot (Jun 27 2024 at 07:02):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-26 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 28 2024 at 01:46):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-27 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 28 2024 at 06:47):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-27 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 28 2024 at 11:09):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-28 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 28 2024 at 13:44):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-28 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 28 2024 at 16:23):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-28 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 28 2024 at 18:46):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-28 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 28 2024 at 21:44):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-28 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 29 2024 at 01:06):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-28 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 29 2024 at 11:04):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-29 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 29 2024 at 13:38):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-29 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 29 2024 at 15:43):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-29 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 29 2024 at 17:24):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-29 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 29 2024 at 18:53):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-29 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 29 2024 at 21:43):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-29 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 30 2024 at 01:19):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-29 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 30 2024 at 08:57):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-29 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 30 2024 at 11:12):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-30 branch from nightly-testing, and then PR that to "bump/v4.10.0".

Kevin Buzzard (Jun 30 2024 at 12:48):

Why does this bot post the same message about eight times?

Michael Stoll (Jun 30 2024 at 12:53):

I may be wrong, but I think it is posting whenever CI on the nightly-testing branch has succeeded (without repeating the message in the other thread).

github mathlib4 bot (Jun 30 2024 at 13:36):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-30 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 30 2024 at 15:54):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-30 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 30 2024 at 19:36):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-30 branch from nightly-testing, and then PR that to "bump/v4.10.0".

github mathlib4 bot (Jun 30 2024 at 21:48):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-30 branch from nightly-testing, and then PR that to "bump/v4.10.0".

Kim Morrison (Jun 30 2024 at 23:31):

@Johan Commelin, I've just run scripts/create-adaptation-pr.sh v4.10.0 2024-06-30, which failed as follows:

% gh pr create -l awaiting-review -l awaiting-CI -B bump/v4.10.0

Creating pull request for bump/nightly-2024-06-30 into bump/v4.10.0 in leanprover-community/mathlib4

? Title chore: adaptations for nightly-2024-06-30
? Choose a template PULL_REQUEST_TEMPLATE.md
? Body <Received>
? What's next? Submit

X operation failed. To restore: gh pr create --recover /var/folders/bs/q5l2kjxd1w98zybcqqgdbml00000gn/T/gh839443417.json

pull request create failed: GraphQL: Body is too long (maximum is 65536 characters) (createPullRequest)

The problem here is that it wanted to fill in the body with a big summary of all the squashed commits.

Could you tweak this, if possible, to specify the title, and that there should be no body, as command line switches? Ideally we could also specify no template, and to submit right away, I guess?

github mathlib4 bot (Jul 01 2024 at 00:15):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-06-30 branch from nightly-testing, and then PR that to "bump/v4.10.0".

Kim Morrison (Jul 01 2024 at 00:41):

Ah, the problem was actually that it created an enormous commit message. I've had to --amend it, as this broken later CI steps.

Johan Commelin (Jul 04 2024 at 16:04):

Kevin Buzzard said:

Why does this bot post the same message about eight times?

Hopefully fixed in #14415

Ruben Van de Velde (Jul 08 2024 at 17:41):

This one is down now, though

Ruben Van de Velde (Jul 08 2024 at 17:42):

Because it's expecting the bump/v4.10.0 to be on a nightly

Kim Morrison (Jul 08 2024 at 18:39):

Almost: I hadn't created bump/v4.11.0. I've done that now, and made #14532, so hopefully it will come good.

Kim Morrison (Jul 08 2024 at 18:39):

I'll go add this step to the release checklist!

Kim Morrison (Jul 08 2024 at 18:42):

lean#4693

github mathlib4 bot (Jul 09 2024 at 23:47):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-09 branch from nightly-testing, and then PR that to "bump/v4.11.0".

github mathlib4 bot (Jul 11 2024 at 03:10):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-10 branch from nightly-testing, and then PR that to "bump/v4.11.0".

github mathlib4 bot (Jul 11 2024 at 14:27):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-11 branch from nightly-testing, and then PR that to "bump/v4.11.0".

github mathlib4 bot (Jul 15 2024 at 18:37):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-12 branch from nightly-testing, and then PR that to "bump/v4.11.0".

github mathlib4 bot (Jul 16 2024 at 17:07):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-16 branch from nightly-testing, and then PR that to "bump/v4.11.0".To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-16

Johan Commelin (Jul 16 2024 at 17:45):

#14806 fixes the missing space in the message

Kim Morrison (Jul 16 2024 at 19:19):

Sadly:

% ./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-16
./scripts/create-adaptation-pr.sh: line 152: syntax error near unexpected token `}'
./scripts/create-adaptation-pr.sh: line 152: `}'

Kim Morrison (Jul 16 2024 at 19:22):

Just some missing fi: #14810

Kim Morrison (Jul 16 2024 at 19:26):

After that, the script stops immediately because CI is still running on the last commit of nightly-testing. I think we want to allow the script to run in this case: otherwise there's too much waiting.

#14813

Kim Morrison (Jul 16 2024 at 19:29):

I also get:

### [auto] Conflict resolution
./scripts/create-adaptation-pr.sh: line 60: lean-toolchain: command not found
./scripts/create-adaptation-pr.sh: line 60: lake-manifest.json: command not found

Kim Morrison (Jul 16 2024 at 19:32):

### [user] Conflict resolution
There seem to be conflicts: please resolve them

should state again which branches we are merging: by this stage earlier message have scrolled off screen if git was busy.

Kim Morrison (Jul 16 2024 at 19:33):

### [auto/user] create a PR for the new branch
Create a pull request. Set the base of the PR to 'bump/v4.11.0'
Here is a suggested 'gh' command to do this:
> gh pr create -t "chore: adaptations for nightly-2024-07-16" -b '' -B bump/v4.11.0
Shall I run this command for you? (y/n)
y
grep: invalid option -- P
usage: grep [-abcdDEFGHhIiJLlMmnOopqRSsUVvwXxZz] [-A num] [-B num] [-C[num]]
        [-e pattern] [-f file] [--binary-files=value] [--color=when]
        [--context[=num]] [--directories=action] [--label] [--line-buffered]
        [--null] [pattern] [file ...]

Kim Morrison (Jul 16 2024 at 19:37):

@Johan Commelin, can I leave you to deal with the three problems starting from "I also get" above?

github mathlib4 bot (Jul 16 2024 at 20:02):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-16 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-16

Johan Commelin (Jul 16 2024 at 20:08):

Kim Morrison said:

Johan Commelin, can I leave you to deal with the three problems starting from "I also get" above?

Yes, I will look at them asap (which might be ~36 hrs from now).
Sorry for all the bugs that you uncovered.

Kim Morrison (Jul 16 2024 at 20:13):

No problem!

Kim Morrison (Jul 16 2024 at 20:13):

CI is hard

github mathlib4 bot (Jul 16 2024 at 22:31):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-16 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-16

github mathlib4 bot (Jul 17 2024 at 01:41):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-16 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-16

github mathlib4 bot (Jul 17 2024 at 03:46):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-16 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-16

Johan Commelin (Jul 17 2024 at 04:25):

@Kim Morrison I hope they are fixed in #14819

github mathlib4 bot (Jul 17 2024 at 04:37):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-16 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-16

Johan Commelin (Jul 17 2024 at 04:48):

I don't know why the bot posted the same message 3 times. We have

            # Get the last message in the 'Mathlib bump branch reminders' topic
            request = {
              'anchor': 'newest',
              'num_before': 1,
              'num_after': 0,
              'narrow': [{'operator': 'stream', 'operand': 'nightly-testing'}, {'operator': 'topic', 'operand': 'Mathlib bump branch reminders'}],
              'apply_markdown': False    # Otherwise the content test below fails.
            }
            response = client.get_messages(request)
            messages = response['messages']
            bump_branch_suffix = bump_branch.replace('bump/', '')
            payload = f"🛠: it looks like it's time to create a new bump/nightly-{current_version} branch from nightly-testing, and then PR that to {bump_branch}. "
            payload += "To do so semi-automatically, run the following script from mathlib root:\n\n"
            payload += f"```bash\n./scripts/create-adaptation-pr.sh {bump_branch_suffix} {current_version}\n```\n"
            if not messages or messages[0]['content'] != payload:
                # Post the reminder message
                request = {
                    'type': 'stream',
                    'to': 'nightly-testing',
                    'topic': 'Mathlib bump branch reminders',
                    'content': payload
                }
                result = client.send_message(request)
                print(result)

at the end of .github/workflows/nightly_detect_failure.yml

Does anyone see what might go wrong?

Damiano Testa (Jul 17 2024 at 05:04):

I do not know what happened, but, to debug, you may ask the step to print the message that it found, and then see what it fetched from here. That might give you some clues.

Johan Commelin (Jul 17 2024 at 05:10):

Done: chore(workflows/nightly_detect_failure): log messages #14821

github mathlib4 bot (Jul 17 2024 at 07:35):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-16 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-16

github mathlib4 bot (Jul 17 2024 at 16:36):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-17 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-17

Damiano Testa (Jul 17 2024 at 16:44):

Should this have already gotten printed twice?

Damiano Testa (Jul 17 2024 at 16:45):

Ah, the date changed wrt to the earlier message!

github mathlib4 bot (Jul 17 2024 at 20:21):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-17 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-17

github mathlib4 bot (Jul 17 2024 at 22:30):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-17 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-17

github mathlib4 bot (Jul 18 2024 at 01:34):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-17 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-17

github mathlib4 bot (Jul 18 2024 at 04:11):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-17 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-17

github mathlib4 bot (Jul 18 2024 at 07:29):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-17 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-17

Johan Commelin (Jul 18 2024 at 07:43):

https://github.com/leanprover-community/mathlib4/actions/runs/9987317244/job/27601446420#step:13:52

Why is the test failing? The messages in the log look identical to me.

Johan Commelin (Jul 18 2024 at 07:55):

Maybe zulip removes the trailing newline? Here is a PR that only compares the first 160 chars of the messages, which should be enough: #14862

github mathlib4 bot (Jul 19 2024 at 00:43):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-18 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-18

github mathlib4 bot (Jul 19 2024 at 00:59):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-18 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-18

github mathlib4 bot (Jul 19 2024 at 17:16):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-19 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-19

Kim Morrison (Jul 19 2024 at 17:42):

I'm about to go do battle with United, so I won't be able to do this. @Johan Commelin?

Ruben Van de Velde (Jul 19 2024 at 18:58):

Good luck

github mathlib4 bot (Jul 19 2024 at 19:31):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-19 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-19

Johan Commelin (Jul 20 2024 at 09:06):

@Kim Morrison I made an attempt. I hope I didn't mess up resolving the merge conflicts.

github mathlib4 bot (Jul 21 2024 at 12:37):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-20 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-20

github mathlib4 bot (Jul 22 2024 at 11:13):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-22 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-22

github mathlib4 bot (Jul 23 2024 at 13:48):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-23 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-23

Johan Commelin (Jul 23 2024 at 15:32):

@Joachim Breitner Are you interested in :up: ?

Joachim Breitner (Jul 23 2024 at 15:33):

I peeked at it already when I got nightly-testing working again, but didn’t learn anything useful from it. So no need to wait for me.

github mathlib4 bot (Jul 23 2024 at 16:51):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-23 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-23

github mathlib4 bot (Jul 25 2024 at 21:00):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-25 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-25

github mathlib4 bot (Jul 27 2024 at 01:59):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-26 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-26

github mathlib4 bot (Jul 28 2024 at 03:30):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-27 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-27

github mathlib4 bot (Jul 29 2024 at 14:17):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-29 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-29

Kim Morrison (Jul 30 2024 at 00:24):

Running now.

github mathlib4 bot (Jul 30 2024 at 02:04):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-29 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-29

github mathlib4 bot (Jul 30 2024 at 14:10):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-30 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-30

github mathlib4 bot (Jul 31 2024 at 12:23):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-31 branch from nightly-testing, and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-31

github mathlib4 bot (Aug 01 2024 at 11:39):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-07-31 branch from nightly-testing (specifically ), and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-07-31

github mathlib4 bot (Aug 02 2024 at 10:58):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-02 branch from nightly-testing (specifically 743a5e8b688cdb0cae231901dc222e469268d5a8), and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-08-02

github mathlib4 bot (Aug 02 2024 at 16:22):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-02 branch from nightly-testing (specifically ), and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-08-02

github mathlib4 bot (Aug 03 2024 at 09:29):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-03 branch from nightly-testing (specifically 76800560a1efa8663ed89214fc1196c97b89ff89), and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-08-03

github mathlib4 bot (Aug 03 2024 at 10:43):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-03 branch from nightly-testing (specifically ), and then PR that to "bump/v4.11.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.11.0" 2024-08-03

github mathlib4 bot (Aug 10 2024 at 07:15):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-09 branch from nightly-testing (specifically ), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-09

github mathlib4 bot (Aug 10 2024 at 13:41):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-10 branch from nightly-testing (specifically be734717404579a0b842c06f1786335dc526b514), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-10

github mathlib4 bot (Aug 10 2024 at 15:44):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-10 branch from nightly-testing (specifically ), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-10

github mathlib4 bot (Aug 11 2024 at 09:16):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-11 branch from nightly-testing (specifically 7e5b9c79c533fd8202193a1b9207a3d2f87ff9cc), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-11

github mathlib4 bot (Aug 11 2024 at 10:38):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-11 branch from nightly-testing (specifically ), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-11

Johan Commelin (Aug 12 2024 at 06:39):

Are there two different contexts in which CI runs this action? Because half of the time the commit hash is missing...

Kim Morrison (Aug 12 2024 at 07:16):

on:
  workflow_run:
    workflows: ["continuous integration"]
    types:
      - completed

Johan Commelin (Aug 12 2024 at 12:23):

Doesn't that mean there is only one context in which this action runs?

Johan Commelin (Aug 12 2024 at 12:23):

Or am I misunderstanding your response?

Kim Morrison (Aug 12 2024 at 12:59):

Sorry, excessively terse there. Yes: as far as I can see there is only one entry point, and I don't understand why there are two different runs with and without SHAs reported. :-(

Ruben Van de Velde (Aug 12 2024 at 12:59):

https://github.com/leanprover-community/mathlib4/actions/runs/10339075534/job/28617982381 seems to be the run that doesn't have a SHA

Ruben Van de Velde (Aug 12 2024 at 13:03):

Ah, I see

Ruben Van de Velde (Aug 12 2024 at 13:04):

The SHA is set in the "Update the nightly-testing-YYYY-MM-DD branch", but only if the branch doesn't exist yet

Ruben Van de Velde (Aug 12 2024 at 13:07):

(I'm not planning to try and fix it)

Johan Commelin (Aug 12 2024 at 14:57):

Thanks for debugging!

github mathlib4 bot (Aug 13 2024 at 02:40):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-12 branch from nightly-testing (specifically dcf33608c8706b1ee9e8a4d1a7e3e066282a036b), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-12

github mathlib4 bot (Aug 13 2024 at 07:34):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-12 branch from nightly-testing (specifically ), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-12

github mathlib4 bot (Aug 13 2024 at 09:26):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-13 branch from nightly-testing (specifically 7a9da2458527a3d008be0c061e897623fec034a5), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-13

github mathlib4 bot (Aug 13 2024 at 10:38):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-13 branch from nightly-testing (specifically ), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-13

github mathlib4 bot (Aug 15 2024 at 08:13):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-14 branch from nightly-testing (specifically b8ad879889282e043c011bdf4643eb4af5e3f99f), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-14

github mathlib4 bot (Aug 15 2024 at 10:15):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-14 branch from nightly-testing (specifically ), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-14

github mathlib4 bot (Aug 16 2024 at 03:03):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-15 branch from nightly-testing (specifically 626dfe1a5ad9509244c7dbd82d36e803b8995f46), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-15

github mathlib4 bot (Aug 16 2024 at 04:42):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-15 branch from nightly-testing (specifically ), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-15

Johan Commelin (Aug 16 2024 at 14:52):

Ruben Van de Velde said:

The SHA is set in the "Update the nightly-testing-YYYY-MM-DD branch", but only if the branch doesn't exist yet

#15888 fixes this

github mathlib4 bot (Aug 17 2024 at 04:43):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-16 branch from nightly-testing (specifically ab5eb1f399ea2e8d4ea27c7bc61b27364217fbef), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-16

Kim Morrison (Aug 17 2024 at 04:50):

Still not there yet, not sure what happened here:

% ./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-16

### Creating a PR for the nightly adaptation for 2024-08-16

### [auto] save the current branch name

### [auto] checkout master and pull the latest changes
Already on 'master'
Your branch is up to date with 'origin/master'.
Already up to date.

### [auto] checkout 'bump/v4.12.0' and merge the latest changes from 'origin/master'
Switched to branch 'bump/v4.12.0'
Your branch is ahead of 'origin/bump/v4.12.0' by 16 commits.
  (use "git push" to publish your local commits)
Already up to date.
Auto-merging Mathlib/Data/List/Indexes.lean
Auto-merging Mathlib/Tactic/FunProp/Core.lean
Auto-merging lake-manifest.json
CONFLICT (content): Merge conflict in lake-manifest.json
Automatic merge failed; fix conflicts and then commit the result.

### [auto] Conflict resolution
### Automatically choosing 'lean-toolchain' and 'lake-manifest.json' from the newer branch
### In this case, the newer branch is 'bump/v4.12.0'
Total 0 (delta 0), reused 0 (delta 0), pack-reused 0 (from 0)
To github.com:leanprover-community/mathlib4.git
   430e0140a4..f8f754936c  bump/v4.12.0 -> bump/v4.12.0

### [auto] create a new branch 'bump/nightly-2024-08-16' and merge the latest changes from 'origin/nightly-testing'
Switched to a new branch 'bump/nightly-2024-08-16'
Updating f8f754936c..ab5eb1f399
error: Your local changes to the following files would be overwritten by merge:
        Mathlib.lean
        Mathlib/Data/List/Basic.lean
Please commit your changes or stash them before you merge.
Aborting

### [auto] commit the changes and push the branch
[bump/nightly-2024-08-16 c7089b8ec5] chore: adaptations for nightly-2024-08-16
 64 files changed, 569 insertions(+), 442 deletions(-)
 rename Mathlib/GroupTheory/{Commutator.lean => Commutator/Basic.lean} (92%)
 create mode 100644 Mathlib/GroupTheory/Commutator/Finite.lean
 rename Mathlib/GroupTheory/{Coset.lean => Coset/Basic.lean} (94%)
 create mode 100644 Mathlib/GroupTheory/Coset/Card.lean
 create mode 100644 Mathlib/GroupTheory/GroupAction/CardCommute.lean
 rename Mathlib/GroupTheory/{QuotientGroup.lean => QuotientGroup/Basic.lean} (93%)
 create mode 100644 Mathlib/GroupTheory/QuotientGroup/Finite.lean
Enumerating objects: 222, done.
Counting objects: 100% (222/222), done.
Delta compression using up to 24 threads
Compressing objects: 100% (111/111), done.
Writing objects: 100% (119/119), 77.71 KiB | 12.95 MiB/s, done.
Total 119 (delta 94), reused 27 (delta 7), pack-reused 0 (from 0)
remote: Resolving deltas: 100% (94/94), completed with 94 local objects.
remote:
remote: Create a pull request for 'bump/nightly-2024-08-16' on GitHub by visiting:
remote:      https://github.com/leanprover-community/mathlib4/pull/new/bump/nightly-2024-08-16
remote:
To github.com:leanprover-community/mathlib4.git
 * [new branch]            bump/nightly-2024-08-16 -> bump/nightly-2024-08-16
branch 'bump/nightly-2024-08-16' set up to track 'origin/bump/nightly-2024-08-16'.

### [auto/user] create a PR for the new branch
Create a pull request. Set the base of the PR to 'bump/v4.12.0'
Here is a suggested 'gh' command to do this:
> gh pr create -t "chore: adaptations for nightly-2024-08-16" -b '' -B bump/v4.12.0
Shall I run this command for you? (y/n)

Kim Morrison (Aug 17 2024 at 04:52):

Ah: the problem is in this part:

# Check if there are merge conflicts
if git diff --name-only --diff-filter=U | grep -q .; then
  echo
  echo "### [auto] Conflict resolution"
  echo "### Automatically choosing 'lean-toolchain' and 'lake-manifest.json' from the newer branch"
  echo "### In this case, the newer branch is 'bump/$BUMPVERSION'"
  git checkout bump/$BUMPVERSION -- lean-toolchain lake-manifest.json
fi

# Check if there are more merge conflicts
if git diff --name-only --diff-filter=U | grep -q .; then
  echo
  echo "### [user] Conflict resolution"
  echo "We are merging the latest changes from 'origin/master' into 'bump/$BUMPVERSION'"
  echo "There seem to be conflicts: please resolve them"
  echo ""
  echo "  1) Open `pwd` in a new terminal and run 'git status'"
  echo "  2) Make sure to commit the resolved conflicts, but do not push them"
  read -p "  3) Press enter to continue, when you are done"
fi

git push

Here, if the only conflicts are solved via git checkout bump/$BUMPVERSION -- lean-toolchain lake-manifest.json, then we never get around to committing the changes. The next if block needs an else that finishes this commit.

Kim Morrison (Aug 17 2024 at 04:57):

#15910

Johan Commelin (Aug 17 2024 at 05:54):

Thanks :peace_sign:

Kim Morrison (Aug 17 2024 at 06:56):

I think #15910 was actually junk, and I've closed it.

Kim Morrison (Aug 17 2024 at 06:57):

I think the actual problem is the logic for detecting if there are still diffs is wrong.

Kim Morrison (Aug 17 2024 at 06:58):

Or rather, those else blocks that I wrote actually need to check if there are any diffs, and no conflicts, rather than just that there are no conflicts.

Kim Morrison (Aug 17 2024 at 06:58):

Because if the only diff had come from lean-toolchain, and then we fix that, running git commit will fail.

Kim Morrison (Aug 17 2024 at 06:58):

(because there is nothing to commit)

Johan Commelin (Aug 19 2024 at 05:19):

#15962 has another go at this (cc @Kim Morrison)

github mathlib4 bot (Aug 19 2024 at 05:48):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-17 branch from nightly-testing (specifically e82727aab149b1515caa9c29547ebf629b9bb195), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-17

Johan Commelin (Aug 19 2024 at 06:11):

The script did everything automatically today: #nightly-testing > #15963 adaptations for nightly-2024-08-17
(This was the script from #15962)

github mathlib4 bot (Aug 19 2024 at 07:25):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-17 branch from nightly-testing (specifically e82727aab149b1515caa9c29547ebf629b9bb195), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-17

github mathlib4 bot (Aug 19 2024 at 09:25):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-19 branch from nightly-testing (specifically 3b7ff954eebc4f837bfd98fc2aba23a79ec7affb), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-19

github mathlib4 bot (Aug 20 2024 at 13:48):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-20 branch from nightly-testing (specifically 7ae246da82c3e747578f861e28e0cafa801ef711), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-20

github mathlib4 bot (Aug 21 2024 at 12:01):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-21 branch from nightly-testing (specifically 2f0739b82177aca39b85f7a6a5dfec6bef27f90f), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-21

github mathlib4 bot (Aug 22 2024 at 10:36):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-22 branch from nightly-testing (specifically bc78dd4064260799592666fb0013b04d7a69f4c6), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-22

github mathlib4 bot (Aug 24 2024 at 05:44):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-23 branch from nightly-testing (specifically 2b617ccc55051120657715a15bc52a6def10b03c), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-23

github mathlib4 bot (Aug 24 2024 at 12:28):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-24 branch from nightly-testing (specifically cf3b406e1eb61883ac6c23c4cd309f305240007c), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-24

github mathlib4 bot (Aug 25 2024 at 12:35):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-25 branch from nightly-testing (specifically 74dc3f9df45b8768b3662c978c25cdf9de8f17b1), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-25

github mathlib4 bot (Aug 26 2024 at 09:59):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-26 branch from nightly-testing (specifically 5608be6564551cffcaf5048d7a3ff5330225e5b8), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-26

github mathlib4 bot (Aug 28 2024 at 11:35):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-28 branch from nightly-testing (specifically 8397433488042b9adf0d37952a2cef2d0abb8cfa), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-28

github mathlib4 bot (Sep 02 2024 at 06:03):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-08-31 branch from nightly-testing (specifically d2a59c1717b96952920b6d524e98452e6207e8e1), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-08-31

github mathlib4 bot (Sep 03 2024 at 00:41):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-02 branch from nightly-testing (specifically b21451955e08c69f627055e9f7fcb78105c7507b), and then PR that to "bump/v4.12.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.12.0" 2024-09-02

github mathlib4 bot (Sep 04 2024 at 07:23):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-03 branch from nightly-testing (specifically e5003139f419c2f87f122db01fe513dc34b784d3), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-03

github mathlib4 bot (Sep 05 2024 at 03:28):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-04 branch from nightly-testing (specifically b5a83ea0c40bb96f710a523dbf14796352c8ce31), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-04

github mathlib4 bot (Sep 06 2024 at 02:54):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-05 branch from nightly-testing (specifically dfbd837a1da3cc0257ec101c10561cb85c0ca325), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-05

github mathlib4 bot (Sep 06 2024 at 23:11):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-06 branch from nightly-testing (specifically 8e11f3bb7182ebae9b94343eae182c6866962dad), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-06

github mathlib4 bot (Sep 09 2024 at 00:10):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-08 branch from nightly-testing (specifically 45faa3eea1dbc6c8336f8a8d288b8871564d5da4), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-08

github mathlib4 bot (Sep 09 2024 at 09:23):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-09 branch from nightly-testing (specifically 1a0ce78731ee2c96b9823665cbb2052d1be9e400), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-09

github mathlib4 bot (Sep 10 2024 at 13:48):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-10 branch from nightly-testing (specifically a24b5c58241139e2f8d1d41d0ca75c77f66c1c6c), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-10

github mathlib4 bot (Sep 12 2024 at 00:18):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-11 branch from nightly-testing (specifically 9405e9af9c4db56c19da07c118e4153fee571727), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-11

github mathlib4 bot (Sep 12 2024 at 11:07):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-12 branch from nightly-testing (specifically c8f802fb69c54d2c197eb1c2a31409da21d98d57), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-12

github mathlib4 bot (Sep 13 2024 at 10:16):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-13 branch from nightly-testing (specifically 8cefabf7abc9875bcbe0656ebb4b83fa65a76a5c), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-13

github mathlib4 bot (Sep 14 2024 at 09:42):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-14 branch from nightly-testing (specifically 4f3889a86ffac7efae3ba1b0024b34f7ac1a8bc1), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-14

github mathlib4 bot (Sep 15 2024 at 09:09):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-15 branch from nightly-testing (specifically fcf04cd57e0d8399ce3f21dae009d2ca2d3abd26), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-15

github mathlib4 bot (Sep 16 2024 at 10:45):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-16 branch from nightly-testing (specifically e9842c947725cc37c92d023e414f946a318bfd86), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-16

github mathlib4 bot (Sep 18 2024 at 01:29):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-17 branch from nightly-testing (specifically e645d886ff9a51fe2ee08f962b5e51beaaba8119), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-17

github mathlib4 bot (Sep 18 2024 at 09:23):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-18 branch from nightly-testing (specifically 58d12e884e3ad7168e1278fcde332ba843964afe), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-18

github mathlib4 bot (Sep 19 2024 at 15:08):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-19 branch from nightly-testing (specifically 02caa3e1a58598830039cdfc9f277714e1846dfc), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-19

github mathlib4 bot (Sep 20 2024 at 12:30):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-20 branch from nightly-testing (specifically 8975918ef97a48d09b1b8706a91bdfd0e1a3361e), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-20

github mathlib4 bot (Sep 21 2024 at 09:21):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-21 branch from nightly-testing (specifically 4cebeb5b6632e5e738dcecc6831c6ea4ec20e9ee), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-21

github mathlib4 bot (Sep 23 2024 at 12:01):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-23 branch from nightly-testing (specifically b3bc833ae962ba9c7eafa4116e7dc8dfe967b0fe), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-23

github mathlib4 bot (Sep 24 2024 at 13:39):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-24 branch from nightly-testing (specifically 08a9b5c185b952bb4a0c628361f4b2f8fe7eb623), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-24

github mathlib4 bot (Sep 25 2024 at 12:01):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-25 branch from nightly-testing (specifically f22e9cb44e572aa5c27f2b3e5136e365e36bf1c3), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh "v4.13.0" 2024-09-25

github mathlib4 bot (Sep 27 2024 at 06:34):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-26 branch from nightly-testing (specifically 0510a8eb7a3628edd2b79c33efa04c93f377281d), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.13.0" --nightlydate=2024-09-26 --nightlysha=0510a8eb7a3628edd2b79c33efa04c93f377281d

github mathlib4 bot (Sep 28 2024 at 05:47):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-27 branch from nightly-testing (specifically c0c2c8fac501e8c0580177432e21fd461cb64580), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.13.0" --nightlydate=2024-09-27 --nightlysha=c0c2c8fac501e8c0580177432e21fd461cb64580

github mathlib4 bot (Sep 30 2024 at 00:25):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-29 branch from nightly-testing (specifically 4a9dd28c84b0d3bf0bc7b70e1767c367da41de99), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.13.0" --nightlydate=2024-09-29 --nightlysha=4a9dd28c84b0d3bf0bc7b70e1767c367da41de99

github mathlib4 bot (Sep 30 2024 at 10:37):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-09-30 branch from nightly-testing (specifically 0c3346c1787354ee3398f5cefa726ff51938f9b1), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.13.0" --nightlydate=2024-09-30 --nightlysha=0c3346c1787354ee3398f5cefa726ff51938f9b1

github mathlib4 bot (Oct 03 2024 at 11:04):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-03 branch from nightly-testing (specifically 5da739c04be092369c9258dd09eb3c9d47841108), and then PR that to "bump/v4.13.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.13.0" --nightlydate=2024-10-03 --nightlysha=5da739c04be092369c9258dd09eb3c9d47841108

Johan Commelin (Oct 08 2024 at 06:37):

I have created and pushed bump/v4.14.0. I hope this will get the bot back on track with posting reminders.

github mathlib4 bot (Oct 08 2024 at 09:27):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-08 branch from nightly-testing (specifically bbd5da4d2d2b4e5950ad78a8ee60a6b477ccab6e), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-08 --nightlysha=bbd5da4d2d2b4e5950ad78a8ee60a6b477ccab6e

github mathlib4 bot (Oct 08 2024 at 10:47):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-08 branch from nightly-testing (specifically bbd5da4d2d2b4e5950ad78a8ee60a6b477ccab6e), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-08 --nightlysha=bbd5da4d2d2b4e5950ad78a8ee60a6b477ccab6e

github mathlib4 bot (Oct 08 2024 at 13:48):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-08 branch from nightly-testing (specifically bbd5da4d2d2b4e5950ad78a8ee60a6b477ccab6e), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-08 --nightlysha=bbd5da4d2d2b4e5950ad78a8ee60a6b477ccab6e

github mathlib4 bot (Oct 08 2024 at 16:31):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-08 branch from nightly-testing (specifically bbd5da4d2d2b4e5950ad78a8ee60a6b477ccab6e), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-08 --nightlysha=bbd5da4d2d2b4e5950ad78a8ee60a6b477ccab6e

github mathlib4 bot (Oct 08 2024 at 19:37):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-08 branch from nightly-testing (specifically bbd5da4d2d2b4e5950ad78a8ee60a6b477ccab6e), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-08 --nightlysha=bbd5da4d2d2b4e5950ad78a8ee60a6b477ccab6e

github mathlib4 bot (Oct 09 2024 at 18:05):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-09 branch from nightly-testing (specifically ccfb9511e1875f89123857f93865228ade8d0cef), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-09 --nightlysha=ccfb9511e1875f89123857f93865228ade8d0cef

github mathlib4 bot (Oct 09 2024 at 19:38):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-09 branch from nightly-testing (specifically ccfb9511e1875f89123857f93865228ade8d0cef), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-09 --nightlysha=ccfb9511e1875f89123857f93865228ade8d0cef

github mathlib4 bot (Oct 09 2024 at 22:39):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-09 branch from nightly-testing (specifically ccfb9511e1875f89123857f93865228ade8d0cef), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-09 --nightlysha=ccfb9511e1875f89123857f93865228ade8d0cef

github mathlib4 bot (Oct 10 2024 at 01:50):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-09 branch from nightly-testing (specifically ccfb9511e1875f89123857f93865228ade8d0cef), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-09 --nightlysha=ccfb9511e1875f89123857f93865228ade8d0cef

github mathlib4 bot (Oct 10 2024 at 04:11):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-09 branch from nightly-testing (specifically ccfb9511e1875f89123857f93865228ade8d0cef), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-09 --nightlysha=ccfb9511e1875f89123857f93865228ade8d0cef

Johan Commelin (Oct 10 2024 at 08:59):

I don't have access to a Lean machine today. Would someone else mind trying to run the script?

github mathlib4 bot (Oct 10 2024 at 19:45):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-10 branch from nightly-testing (specifically 5c179825b962cca3ba1fae66444dea32a12de3f2), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-10 --nightlysha=5c179825b962cca3ba1fae66444dea32a12de3f2

github mathlib4 bot (Oct 11 2024 at 04:08):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-10 branch from nightly-testing (specifically 5c179825b962cca3ba1fae66444dea32a12de3f2), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-10 --nightlysha=5c179825b962cca3ba1fae66444dea32a12de3f2

github mathlib4 bot (Oct 11 2024 at 06:52):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-10 branch from nightly-testing (specifically 5c179825b962cca3ba1fae66444dea32a12de3f2), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-10 --nightlysha=5c179825b962cca3ba1fae66444dea32a12de3f2

github mathlib4 bot (Oct 13 2024 at 13:02):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-13 branch from nightly-testing (specifically 6125cddcb7541bb61d58f6f316cdd43b9c962e17), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-13 --nightlysha=6125cddcb7541bb61d58f6f316cdd43b9c962e17

github mathlib4 bot (Oct 13 2024 at 15:53):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-13 branch from nightly-testing (specifically 6125cddcb7541bb61d58f6f316cdd43b9c962e17), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-13 --nightlysha=6125cddcb7541bb61d58f6f316cdd43b9c962e17

github mathlib4 bot (Oct 13 2024 at 18:55):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-13 branch from nightly-testing (specifically 6125cddcb7541bb61d58f6f316cdd43b9c962e17), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-13 --nightlysha=6125cddcb7541bb61d58f6f316cdd43b9c962e17

github mathlib4 bot (Oct 13 2024 at 21:57):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-13 branch from nightly-testing (specifically 6125cddcb7541bb61d58f6f316cdd43b9c962e17), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-13 --nightlysha=6125cddcb7541bb61d58f6f316cdd43b9c962e17

github mathlib4 bot (Oct 13 2024 at 23:55):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-13 branch from nightly-testing (specifically 6125cddcb7541bb61d58f6f316cdd43b9c962e17), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-13 --nightlysha=6125cddcb7541bb61d58f6f316cdd43b9c962e17

github mathlib4 bot (Oct 14 2024 at 01:14):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-13 branch from nightly-testing (specifically 6125cddcb7541bb61d58f6f316cdd43b9c962e17), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-13 --nightlysha=6125cddcb7541bb61d58f6f316cdd43b9c962e17

Kim Morrison (Oct 14 2024 at 01:36):

@Johan Commelin, are we expecting this bot to keep posting, even though I've made the PR?

Kim Morrison (Oct 14 2024 at 01:36):

Seems like it should be quiet now!

Johan Commelin (Oct 14 2024 at 03:37):

Oh, weird! I removed the logic that checked if a message had been posted. Because I assumed the sha would be different each time anyway. Seems I was wrong.

Johan Commelin (Oct 14 2024 at 03:37):

I will restore that logic.

github mathlib4 bot (Oct 14 2024 at 03:50):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-13 branch from nightly-testing (specifically 6125cddcb7541bb61d58f6f316cdd43b9c962e17), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-13 --nightlysha=6125cddcb7541bb61d58f6f316cdd43b9c962e17

github mathlib4 bot (Oct 14 2024 at 10:38):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-14 branch from nightly-testing (specifically 663637410a7edbee9fc0737ff0fdd01edd35a4b4), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-14 --nightlysha=663637410a7edbee9fc0737ff0fdd01edd35a4b4

Johan Commelin (Oct 14 2024 at 13:41):

@Kim Morrison #17728 should restore the logic

github mathlib4 bot (Oct 14 2024 at 14:03):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-14 branch from nightly-testing (specifically 663637410a7edbee9fc0737ff0fdd01edd35a4b4), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-14 --nightlysha=663637410a7edbee9fc0737ff0fdd01edd35a4b4

github mathlib4 bot (Oct 16 2024 at 04:38):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-15 branch from nightly-testing (specifically 264cb92bc96c0f0e1a92ea20524a1de270b3f008), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-15 --nightlysha=264cb92bc96c0f0e1a92ea20524a1de270b3f008

github mathlib4 bot (Oct 17 2024 at 04:38):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-16 branch from nightly-testing (specifically e553fb0852ed7000d6b34eb25bb6d9a83ee069c4), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-16 --nightlysha=e553fb0852ed7000d6b34eb25bb6d9a83ee069c4

github mathlib4 bot (Oct 17 2024 at 13:26):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-17 branch from nightly-testing (specifically 71802680628fbeb426c7a0c17107eeb67ac18fe0), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-17 --nightlysha=71802680628fbeb426c7a0c17107eeb67ac18fe0

Kim Morrison (Oct 19 2024 at 11:30):

I'm hopeful we'll get a reminder here soon, but we need to remember that #17872 needs to be merged before we can create the next one.

github mathlib4 bot (Oct 19 2024 at 12:17):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-19 branch from nightly-testing (specifically 407a4459e2005e212bb230d2746afe980eba7003), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-19 --nightlysha=407a4459e2005e212bb230d2746afe980eba7003

github mathlib4 bot (Oct 21 2024 at 12:45):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-21 branch from nightly-testing (specifically 26dafbb134ad1635c84c2c81363140e1ba78005e), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-21 --nightlysha=26dafbb134ad1635c84c2c81363140e1ba78005e

github mathlib4 bot (Oct 22 2024 at 10:15):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-22 branch from nightly-testing (specifically 5d9876da9e139761f55a9d3bba56cbd11fe5ecf4), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-22 --nightlysha=5d9876da9e139761f55a9d3bba56cbd11fe5ecf4

github mathlib4 bot (Oct 23 2024 at 09:08):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-23 branch from nightly-testing (specifically 3ed0adc8f4c5f3c0b1cdd195e1c16c0e6fae8e8c), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-23 --nightlysha=3ed0adc8f4c5f3c0b1cdd195e1c16c0e6fae8e8c

github mathlib4 bot (Oct 24 2024 at 10:41):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-24 branch from nightly-testing (specifically 3307c67acbea9ff66f3a40e0c876b4af694000ab), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-24 --nightlysha=3307c67acbea9ff66f3a40e0c876b4af694000ab

github mathlib4 bot (Oct 25 2024 at 09:12):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-25 branch from nightly-testing (specifically 5b391bd6a2dafc56a16caeef82eb19c1c1518104), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-25 --nightlysha=5b391bd6a2dafc56a16caeef82eb19c1c1518104

github mathlib4 bot (Oct 27 2024 at 23:09):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-27 branch from nightly-testing (specifically be300cdc068254562106cb8ab789da120de5acf2), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-27 --nightlysha=be300cdc068254562106cb8ab789da120de5acf2

github mathlib4 bot (Oct 28 2024 at 11:28):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-28 branch from nightly-testing (specifically 347ad1b741a37bbe745a46cd0d0ff06aa4f80965), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-28 --nightlysha=347ad1b741a37bbe745a46cd0d0ff06aa4f80965

github mathlib4 bot (Oct 30 2024 at 00:26):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-29 branch from nightly-testing (specifically 4478d113e456c870c14d99246808b74783756287), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-29 --nightlysha=4478d113e456c870c14d99246808b74783756287

github mathlib4 bot (Oct 30 2024 at 11:05):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-30 branch from nightly-testing (specifically 19a2e289f248500411b87004e36f407e44c4c010), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-30 --nightlysha=19a2e289f248500411b87004e36f407e44c4c010

Kim Morrison (Oct 30 2024 at 11:25):

@Johan Commelin, how about we remove the "open an editor to confirm the git commit message" step from this script? I don't think I've ever done anything except close the editor.

Kim Morrison (Oct 30 2024 at 11:25):

Similarly we might not require the two confirmations for creating a PR and sending the zulip message.

Johan Commelin (Oct 30 2024 at 11:28):

Sounds good. I'll try to do that later this week.

github mathlib4 bot (Oct 30 2024 at 12:02):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-30 branch from nightly-testing (specifically 19a2e289f248500411b87004e36f407e44c4c010), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-30 --nightlysha=19a2e289f248500411b87004e36f407e44c4c010

Kim Morrison (Oct 30 2024 at 22:17):

This seems to be a repeat of the message above: it's also about 2024-10-30

github mathlib4 bot (Oct 31 2024 at 01:31):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-30 branch from nightly-testing (specifically 19a2e289f248500411b87004e36f407e44c4c010), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-30 --nightlysha=19a2e289f248500411b87004e36f407e44c4c010

Johan Commelin (Oct 31 2024 at 05:48):

Kim Morrison said:

This seems to be a repeat of the message above: it's also about 2024-10-30

Yup, but the workflow only checks against the latest message in the thread, which was my response to you. So occasionally we'll get repeats.

Johan Commelin (Oct 31 2024 at 07:02):

@Kim Morrison #18485 puts the script in auto mode by default, and adds --no-edit to the merge commands in the script.

github mathlib4 bot (Oct 31 2024 at 09:15):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-10-31 branch from nightly-testing (specifically 0af7fdf367d4a47093030a029e183fc2530cede4), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-10-31 --nightlysha=0af7fdf367d4a47093030a029e183fc2530cede4

github mathlib4 bot (Nov 01 2024 at 16:09):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-01 branch from nightly-testing (specifically 55da1f83fea32853a6da79f84316361e646fc365), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-11-01 --nightlysha=55da1f83fea32853a6da79f84316361e646fc365

github mathlib4 bot (Nov 02 2024 at 19:12):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-02 branch from nightly-testing (specifically ef5ff126f83dceb492b40f3b30c19cc071eac163), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-11-02 --nightlysha=ef5ff126f83dceb492b40f3b30c19cc071eac163

github mathlib4 bot (Nov 03 2024 at 09:12):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-03 branch from nightly-testing (specifically 022e83a3574b2369be549178ef7a785b7c716f51), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-11-03 --nightlysha=022e83a3574b2369be549178ef7a785b7c716f51

Kim Morrison (Nov 03 2024 at 22:48):

@Johan Commelin, I think your latest changes to the script now resulted in:

### [auto] Conflict resolution
### Automatically choosing 'lean-toolchain' and 'lake-manifest.json' from the newer branch
### In this case, the newer branch is 'bump/v4.14.0'
Auto mode enabled. Bailing out due to unresolved conflicts or uncommitted changes.

which wasn't intended?

Kim Morrison (Nov 03 2024 at 22:49):

It shouldn't be bailing out on merge conflicts.

github mathlib4 bot (Nov 04 2024 at 00:09):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-03 branch from nightly-testing (specifically 022e83a3574b2369be549178ef7a785b7c716f51), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-11-03 --nightlysha=022e83a3574b2369be549178ef7a785b7c716f51

Johan Commelin (Nov 04 2024 at 05:17):

Kim Morrison said:

It shouldn't be bailing out on merge conflicts.

Aaah, right. So just enabling auto mode wasn't the right fix. #18600 is a better version.

github mathlib4 bot (Nov 04 2024 at 11:21):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-04 branch from nightly-testing (specifically b28f0d7f7e9cc3949a9a3556a6b36513f37f690d), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-11-04 --nightlysha=b28f0d7f7e9cc3949a9a3556a6b36513f37f690d

github mathlib4 bot (Nov 10 2024 at 22:57):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-10 branch from nightly-testing (specifically db9c4895583aedbcffefebb9a1396e49dd353076), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-11-10 --nightlysha=db9c4895583aedbcffefebb9a1396e49dd353076

github mathlib4 bot (Nov 11 2024 at 10:43):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-11 branch from nightly-testing (specifically 3894c72cbd6f4baba45c79678e75503123a51756), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-11-11 --nightlysha=3894c72cbd6f4baba45c79678e75503123a51756

github mathlib4 bot (Nov 12 2024 at 21:26):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-12 branch from nightly-testing (specifically 6c3ffb61f93289ca8959e436efe546e7d3465f78), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-11-12 --nightlysha=6c3ffb61f93289ca8959e436efe546e7d3465f78

github mathlib4 bot (Nov 14 2024 at 02:01):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-13 branch from nightly-testing (specifically bae40f51101fe0dbebff6d6a5f56532ca845f1f4), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-11-13 --nightlysha=bae40f51101fe0dbebff6d6a5f56532ca845f1f4

Kim Morrison (Nov 14 2024 at 02:10):

Oops: @Johan Commelin, why is this script telling us to PR to bump/v4.14.0. It should be v4.15.0 by now!!

github mathlib4 bot (Nov 14 2024 at 02:45):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-13 branch from nightly-testing (specifically bae40f51101fe0dbebff6d6a5f56532ca845f1f4), and then PR that to "bump/v4.14.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.14.0" --nightlydate=2024-11-13 --nightlysha=bae40f51101fe0dbebff6d6a5f56532ca845f1f4

github mathlib4 bot (Nov 14 2024 at 23:33):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-14 branch from nightly-testing (specifically 5d03a2cd14f5dbfd233359a68d31fd12ad9a535e), and then PR that to "bump/v4.15.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.15.0" --nightlydate=2024-11-14 --nightlysha=5d03a2cd14f5dbfd233359a68d31fd12ad9a535e

github mathlib4 bot (Nov 17 2024 at 11:24):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-15 branch from nightly-testing (specifically 89e8f886145b9fbd4543ff7b8e1f0cf39a4e009c), and then PR that to "bump/v4.15.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.15.0" --nightlydate=2024-11-15 --nightlysha=89e8f886145b9fbd4543ff7b8e1f0cf39a4e009c

Kim Morrison (Nov 17 2024 at 11:24):

Note we are still blocked on review of #19059.

github mathlib4 bot (Nov 17 2024 at 12:55):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-15 branch from nightly-testing (specifically 89e8f886145b9fbd4543ff7b8e1f0cf39a4e009c), and then PR that to "bump/v4.15.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.15.0" --nightlydate=2024-11-15 --nightlysha=89e8f886145b9fbd4543ff7b8e1f0cf39a4e009c

github mathlib4 bot (Nov 19 2024 at 01:45):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-18 branch from nightly-testing (specifically 971d01d592ff5787e284ab48d59340f1715ad2d6), and then PR that to "bump/v4.15.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.15.0" --nightlydate=2024-11-18 --nightlysha=971d01d592ff5787e284ab48d59340f1715ad2d6

github mathlib4 bot (Nov 19 2024 at 09:21):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-19 branch from nightly-testing (specifically 60a189e5bc5c59e67faa3f3445229e76298ce4dc), and then PR that to "bump/v4.15.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.15.0" --nightlydate=2024-11-19 --nightlysha=60a189e5bc5c59e67faa3f3445229e76298ce4dc

Kim Morrison (Nov 19 2024 at 10:28):

Let's wait for the next build (today), I just pushed the revert of the notation change.

github mathlib4 bot (Nov 19 2024 at 11:14):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-19 branch from nightly-testing (specifically 60a189e5bc5c59e67faa3f3445229e76298ce4dc), and then PR that to "bump/v4.15.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.15.0" --nightlydate=2024-11-19 --nightlysha=60a189e5bc5c59e67faa3f3445229e76298ce4dc

github mathlib4 bot (Nov 20 2024 at 22:44):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-20 branch from nightly-testing (specifically 33e7503de887ec81d3b24de62cfce9440ffa55a8), and then PR that to "bump/v4.15.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.15.0" --nightlydate=2024-11-20 --nightlysha=33e7503de887ec81d3b24de62cfce9440ffa55a8

github mathlib4 bot (Nov 21 2024 at 11:13):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-21 branch from nightly-testing (specifically 8ce05c99ea86bd5531e5a84a45f04cefa20df502), and then PR that to "bump/v4.15.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.15.0" --nightlydate=2024-11-21 --nightlysha=8ce05c99ea86bd5531e5a84a45f04cefa20df502

github mathlib4 bot (Nov 22 2024 at 22:10):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-22 branch from nightly-testing (specifically 714674cc3646c9d15485e7cf26fb8c1b22655a64), and then PR that to "bump/v4.15.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.15.0" --nightlydate=2024-11-22 --nightlysha=714674cc3646c9d15485e7cf26fb8c1b22655a64

github mathlib4 bot (Nov 23 2024 at 11:43):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-23 branch from nightly-testing (specifically d1f4f68c3cd7162e8b86e5ae3a27eb0250fb8095), and then PR that to "bump/v4.15.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.15.0" --nightlydate=2024-11-23 --nightlysha=d1f4f68c3cd7162e8b86e5ae3a27eb0250fb8095

github mathlib4 bot (Nov 24 2024 at 10:47):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-24 branch from nightly-testing (specifically db0487a4dbe7caa9f45514455f4edddbc56d0505), and then PR that to "bump/v4.15.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.15.0" --nightlydate=2024-11-24 --nightlysha=db0487a4dbe7caa9f45514455f4edddbc56d0505

github mathlib4 bot (Nov 26 2024 at 00:00):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-25 branch from nightly-testing (specifically dbb613fb80683eeae413deddb3ad5189b7c3ba81), and then PR that to "bump/v4.15.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.15.0" --nightlydate=2024-11-25 --nightlysha=dbb613fb80683eeae413deddb3ad5189b7c3ba81

github mathlib4 bot (Nov 26 2024 at 11:01):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-26 branch from nightly-testing (specifically a10eba97bbf9fccde39aaa51c640a0716513b627), and then PR that to "bump/v4.15.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.15.0" --nightlydate=2024-11-26 --nightlysha=a10eba97bbf9fccde39aaa51c640a0716513b627

github mathlib4 bot (Nov 28 2024 at 01:24):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-27 branch from nightly-testing (specifically 606995ead3bc421c5ebd78e4112a588f188fada3), and then PR that to "bump/v4.15.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.15.0" --nightlydate=2024-11-27 --nightlysha=606995ead3bc421c5ebd78e4112a588f188fada3

github mathlib4 bot (Nov 28 2024 at 11:39):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-28 branch from nightly-testing (specifically 1ef016d640f5e5ff5f6b566e8f886073db310e80), and then PR that to "bump/v4.15.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.15.0" --nightlydate=2024-11-28 --nightlysha=1ef016d640f5e5ff5f6b566e8f886073db310e80

github mathlib4 bot (Nov 30 2024 at 10:27):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-29 branch from nightly-testing (specifically 1d86c526627b20fe1a580aae4341ff166747b8ea), and then PR that to "bump/v4.15.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.15.0" --nightlydate=2024-11-29 --nightlysha=1d86c526627b20fe1a580aae4341ff166747b8ea

github mathlib4 bot (Dec 01 2024 at 01:27):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-11-30 branch from nightly-testing (specifically 222e64d6bc042156d6e39860ad9f0c79552de8e0), and then PR that to "bump/v4.15.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.15.0" --nightlydate=2024-11-30 --nightlysha=222e64d6bc042156d6e39860ad9f0c79552de8e0

github mathlib4 bot (Dec 01 2024 at 23:52):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-01 branch from nightly-testing (specifically 5f67609288d56f40ab174ea90db3dda888223a81), and then PR that to "bump/v4.15.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.15.0" --nightlydate=2024-12-01 --nightlysha=5f67609288d56f40ab174ea90db3dda888223a81

github mathlib4 bot (Dec 05 2024 at 07:11):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-04 branch from nightly-testing (specifically 4745c02319412eeffd9dedd0284b48f8e30eeee1), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-04 --nightlysha=4745c02319412eeffd9dedd0284b48f8e30eeee1

github mathlib4 bot (Dec 05 2024 at 12:17):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-05 branch from nightly-testing (specifically b01be4bda23a785e988643a07f24c7e478b23c83), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-05 --nightlysha=b01be4bda23a785e988643a07f24c7e478b23c83

github mathlib4 bot (Dec 06 2024 at 09:26):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-06 branch from nightly-testing (specifically c6f4e015f5c536740ae52ea5926112e95d330f5a), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-06 --nightlysha=c6f4e015f5c536740ae52ea5926112e95d330f5a

github mathlib4 bot (Dec 08 2024 at 22:16):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-08 branch from nightly-testing (specifically 20b2fd4c7be9ad9e2acf3c4347aa02aac4209a68), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-08 --nightlysha=20b2fd4c7be9ad9e2acf3c4347aa02aac4209a68

github mathlib4 bot (Dec 09 2024 at 10:20):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-09 branch from nightly-testing (specifically ded531d92e509cb63d09ed490f49dbe45dde217e), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-09 --nightlysha=ded531d92e509cb63d09ed490f49dbe45dde217e

github mathlib4 bot (Dec 10 2024 at 11:20):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-10 branch from nightly-testing (specifically f0f251d299ff907bada73f4dbfba2dfd0d619b69), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-10 --nightlysha=f0f251d299ff907bada73f4dbfba2dfd0d619b69

github mathlib4 bot (Dec 11 2024 at 10:46):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-11 branch from nightly-testing (specifically d1a65ef8cb89d1abb40397f03aa58f55f7438556), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-11 --nightlysha=d1a65ef8cb89d1abb40397f03aa58f55f7438556

github mathlib4 bot (Dec 12 2024 at 10:20):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-12 branch from nightly-testing (specifically d337aa990393a12a169ce0198e119251442d574e), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-12 --nightlysha=d337aa990393a12a169ce0198e119251442d574e

github mathlib4 bot (Dec 13 2024 at 22:18):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-13 branch from nightly-testing (specifically 24a956e927a627c16a104adc19ceca8b33569ea7), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-13 --nightlysha=24a956e927a627c16a104adc19ceca8b33569ea7

github mathlib4 bot (Dec 15 2024 at 07:18):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-14 branch from nightly-testing (specifically ddcb85bddebd7fa5b7316dab25b7eae6e0ff1fbb), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-14 --nightlysha=ddcb85bddebd7fa5b7316dab25b7eae6e0ff1fbb

github mathlib4 bot (Dec 15 2024 at 10:20):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-15 branch from nightly-testing (specifically 13dbab738d85e172eaed1ba05012dd6b48c72039), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-15 --nightlysha=13dbab738d85e172eaed1ba05012dd6b48c72039

github mathlib4 bot (Dec 21 2024 at 04:57):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-20 branch from nightly-testing (specifically 8a4877456aa721f76724451be03284db54851891), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-20 --nightlysha=8a4877456aa721f76724451be03284db54851891

github mathlib4 bot (Dec 21 2024 at 20:45):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-21 branch from nightly-testing (specifically b774a65bf5d20fd92d63eb98d03be2b29dfd9f27), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-21 --nightlysha=b774a65bf5d20fd92d63eb98d03be2b29dfd9f27

github mathlib4 bot (Dec 22 2024 at 09:22):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-22 branch from nightly-testing (specifically 63618639886f3bea1260812a0e5b81aebdc8cc60), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-22 --nightlysha=63618639886f3bea1260812a0e5b81aebdc8cc60

github mathlib4 bot (Dec 23 2024 at 09:12):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-23 branch from nightly-testing (specifically ed546d89ba3b9fa2c93b3501b9f6aac3593c930d), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-23 --nightlysha=ed546d89ba3b9fa2c93b3501b9f6aac3593c930d

github mathlib4 bot (Dec 24 2024 at 09:24):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-24 branch from nightly-testing (specifically 9a6b101b298066238b15e3fbd66618c2088cc693), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-24 --nightlysha=9a6b101b298066238b15e3fbd66618c2088cc693

github mathlib4 bot (Dec 25 2024 at 09:24):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-25 branch from nightly-testing (specifically 8157db740f7cbf298fb4839f6b1b81b03f76d44e), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-25 --nightlysha=8157db740f7cbf298fb4839f6b1b81b03f76d44e

github mathlib4 bot (Dec 26 2024 at 09:23):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-26 branch from nightly-testing (specifically d97af69f33c3a73efddc6db118bf4ffdb0ff78cd), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-26 --nightlysha=d97af69f33c3a73efddc6db118bf4ffdb0ff78cd

github mathlib4 bot (Dec 27 2024 at 09:23):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-27 branch from nightly-testing (specifically 9cbdb8573d4029e6ae53898ae6002b9f9b95328c), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-27 --nightlysha=9cbdb8573d4029e6ae53898ae6002b9f9b95328c

github mathlib4 bot (Dec 28 2024 at 16:46):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-28 branch from nightly-testing (specifically 84397c9ac1acff58fe69934a8d8ee44e2b9d85a0), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-28 --nightlysha=84397c9ac1acff58fe69934a8d8ee44e2b9d85a0

github mathlib4 bot (Dec 29 2024 at 14:14):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-29 branch from nightly-testing (specifically 007c83315419f9d66e0056ac22cd99fabbad8069), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-29 --nightlysha=007c83315419f9d66e0056ac22cd99fabbad8069

github mathlib4 bot (Dec 30 2024 at 09:28):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-30 branch from nightly-testing (specifically 310c1aa3b3b315662b745a38d252e8668dbc15d5), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-30 --nightlysha=310c1aa3b3b315662b745a38d252e8668dbc15d5

github mathlib4 bot (Dec 31 2024 at 09:23):

:working_on_it:: it looks like it's time to create a new bump/nightly-2024-12-31 branch from nightly-testing (specifically c3cb62f4b4768c69484af8be1988e1d8ae00c3ce), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2024-12-31 --nightlysha=c3cb62f4b4768c69484af8be1988e1d8ae00c3ce

github mathlib4 bot (Jan 02 2025 at 14:50):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-02 branch from nightly-testing (specifically c7c1e06e17bc790c799baec988d32a7abaa51875), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2025-01-02 --nightlysha=c7c1e06e17bc790c799baec988d32a7abaa51875

github mathlib4 bot (Jan 03 2025 at 09:26):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-03 branch from nightly-testing (specifically 15d915fa08f4c49f024aa59d1954fde50cca38c1), and then PR that to "bump/v4.16.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.16.0" --nightlydate=2025-01-03 --nightlysha=15d915fa08f4c49f024aa59d1954fde50cca38c1

github mathlib4 bot (Jan 05 2025 at 01:34):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-04 branch from nightly-testing (specifically 33876800b00716486c19466df8efee1440a3e777), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-04 --nightlysha=33876800b00716486c19466df8efee1440a3e777

github mathlib4 bot (Jan 05 2025 at 09:47):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-05 branch from nightly-testing (specifically bc1d910c4bf47623e9e4038ec005877c38183305), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-05 --nightlysha=bc1d910c4bf47623e9e4038ec005877c38183305

github mathlib4 bot (Jan 06 2025 at 10:26):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-06 branch from nightly-testing (specifically 00495cea91b1d8614e4957572cb32d1679b4296f), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-06 --nightlysha=00495cea91b1d8614e4957572cb32d1679b4296f

github mathlib4 bot (Jan 07 2025 at 09:27):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-07 branch from nightly-testing (specifically 9f2fa6ce057e6b196523b83134f1db0b2adafada), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-07 --nightlysha=9f2fa6ce057e6b196523b83134f1db0b2adafada

github mathlib4 bot (Jan 08 2025 at 10:21):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-08 branch from nightly-testing (specifically a5e74b31f33ac8d48faaad46d8b6da297aa46fcb), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-08 --nightlysha=a5e74b31f33ac8d48faaad46d8b6da297aa46fcb

Kim Morrison (Jan 08 2025 at 10:56):

All quiet on the nightly-testing front.

github mathlib4 bot (Jan 08 2025 at 13:01):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-08 branch from nightly-testing (specifically a5e74b31f33ac8d48faaad46d8b6da297aa46fcb), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-08 --nightlysha=a5e74b31f33ac8d48faaad46d8b6da297aa46fcb

github mathlib4 bot (Jan 09 2025 at 14:19):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-09 branch from nightly-testing (specifically 1e7d93f1607609b889e37abf9cf87f9290b83b7c), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-09 --nightlysha=1e7d93f1607609b889e37abf9cf87f9290b83b7c

Kim Morrison (Jan 09 2025 at 22:10):

Another one we can skip, I think. Just one theorem removed (up streamed accidentally!) from Batteries.

github mathlib4 bot (Jan 10 2025 at 02:28):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-09 branch from nightly-testing (specifically 1e7d93f1607609b889e37abf9cf87f9290b83b7c), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-09 --nightlysha=1e7d93f1607609b889e37abf9cf87f9290b83b7c

github mathlib4 bot (Jan 10 2025 at 11:23):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-10 branch from nightly-testing (specifically 2a00a07c117d5c40c4bc779c66091fd8fc653155), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-10 --nightlysha=2a00a07c117d5c40c4bc779c66091fd8fc653155

github mathlib4 bot (Jan 14 2025 at 11:14):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-14 branch from nightly-testing (specifically ba207fbdbaa72544b58589ea3ae95a8ca6e5d595), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-14 --nightlysha=ba207fbdbaa72544b58589ea3ae95a8ca6e5d595

github mathlib4 bot (Jan 15 2025 at 10:43):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-15 branch from nightly-testing (specifically db3b11e6f0e79ec5e416d03fd29c873739e748dc), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-15 --nightlysha=db3b11e6f0e79ec5e416d03fd29c873739e748dc

github mathlib4 bot (Jan 16 2025 at 22:41):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-16 branch from nightly-testing (specifically b57abe19e88c3b836e84c3b6d5690065376f7f3b), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-16 --nightlysha=b57abe19e88c3b836e84c3b6d5690065376f7f3b

github mathlib4 bot (Jan 17 2025 at 10:35):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-17 branch from nightly-testing (specifically f059ccdd26b54901d17ae8cc90c0ee58b88bedb0), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-17 --nightlysha=f059ccdd26b54901d17ae8cc90c0ee58b88bedb0

Kim Morrison (Jan 17 2025 at 10:38):

Should be pretty trivial, let's skip.

github mathlib4 bot (Jan 17 2025 at 13:02):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-17 branch from nightly-testing (specifically f059ccdd26b54901d17ae8cc90c0ee58b88bedb0), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-17 --nightlysha=f059ccdd26b54901d17ae8cc90c0ee58b88bedb0

github mathlib4 bot (Jan 18 2025 at 10:25):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-18 branch from nightly-testing (specifically 7de4ea33f32d8a5fe224e82e755a342fde3a0fa4), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-18 --nightlysha=7de4ea33f32d8a5fe224e82e755a342fde3a0fa4

github mathlib4 bot (Jan 19 2025 at 11:09):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-19 branch from nightly-testing (specifically 5b336e4a3fbd4642747e804d86e4d31ba469119b), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-19 --nightlysha=5b336e4a3fbd4642747e804d86e4d31ba469119b

github mathlib4 bot (Jan 20 2025 at 14:12):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-20 branch from nightly-testing (specifically a17fe140cca9b29dfa7ec9727deabd7bc114ba63), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-20 --nightlysha=a17fe140cca9b29dfa7ec9727deabd7bc114ba63

github mathlib4 bot (Jan 21 2025 at 11:49):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-21 branch from nightly-testing (specifically dcf59332226749edf58a2cf191d2672c0083fa48), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-21 --nightlysha=dcf59332226749edf58a2cf191d2672c0083fa48

github mathlib4 bot (Jan 22 2025 at 09:33):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-22 branch from nightly-testing (specifically 9bfb7cd4e59c6c6d16d745f27e2370d1d8a4d638), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-22 --nightlysha=9bfb7cd4e59c6c6d16d745f27e2370d1d8a4d638

github mathlib4 bot (Jan 23 2025 at 09:33):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-23 branch from nightly-testing (specifically 681a0a09c81894fb47870c2d9b318360716f0b04), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-23 --nightlysha=681a0a09c81894fb47870c2d9b318360716f0b04

github mathlib4 bot (Jan 24 2025 at 13:25):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-24 branch from nightly-testing (specifically 3e696a8a9edeb0fca0e1a9df552c7e91d2aca018), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-24 --nightlysha=3e696a8a9edeb0fca0e1a9df552c7e91d2aca018

github mathlib4 bot (Jan 25 2025 at 10:23):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-25 branch from nightly-testing (specifically 578b8b9c0de205ff68df2d66f6c20828122e4242), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-25 --nightlysha=578b8b9c0de205ff68df2d66f6c20828122e4242

github mathlib4 bot (Jan 26 2025 at 09:34):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-26 branch from nightly-testing (specifically b36f8b22a2bdf77d064996493768f6f780d5f4c2), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-26 --nightlysha=b36f8b22a2bdf77d064996493768f6f780d5f4c2

github mathlib4 bot (Jan 27 2025 at 10:23):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-27 branch from nightly-testing (specifically 5011e4754518f50f90c05ead57ff20f753d60c98), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-27 --nightlysha=5011e4754518f50f90c05ead57ff20f753d60c98

github mathlib4 bot (Jan 28 2025 at 10:25):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-28 branch from nightly-testing (specifically 94b2ff5a02d742d2b90bc22e5a0da8f4bef2c68c), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-28 --nightlysha=94b2ff5a02d742d2b90bc22e5a0da8f4bef2c68c

github mathlib4 bot (Jan 30 2025 at 00:40):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-29 branch from nightly-testing (specifically 7b2d9ab953bba5cceb441b1641eae8ee62fe03fd), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-29 --nightlysha=7b2d9ab953bba5cceb441b1641eae8ee62fe03fd

github mathlib4 bot (Jan 30 2025 at 11:05):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-30 branch from nightly-testing (specifically e36c2b838cb650a07a6b95ae8eb96dc39b7468b2), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-30 --nightlysha=e36c2b838cb650a07a6b95ae8eb96dc39b7468b2

github mathlib4 bot (Jan 31 2025 at 11:59):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-01-31 branch from nightly-testing (specifically 432e7f81b666b3821733768a4e87bd2a77dda052), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-01-31 --nightlysha=432e7f81b666b3821733768a4e87bd2a77dda052

github mathlib4 bot (Feb 01 2025 at 09:31):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-01 branch from nightly-testing (specifically ee185c77453acccd00a506f01cd01692a7e55a5c), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-02-01 --nightlysha=ee185c77453acccd00a506f01cd01692a7e55a5c

github mathlib4 bot (Feb 02 2025 at 11:27):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-02 branch from nightly-testing (specifically b9329078bf12b90531207e8efd16c6ad543ee0d5), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-02-02 --nightlysha=b9329078bf12b90531207e8efd16c6ad543ee0d5

github mathlib4 bot (Feb 03 2025 at 10:23):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-03 branch from nightly-testing (specifically a94c6d1c3e86987f507443d7464a2c802c2e39ac), and then PR that to "bump/v4.17.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.17.0" --nightlydate=2025-02-03 --nightlysha=a94c6d1c3e86987f507443d7464a2c802c2e39ac

github mathlib4 bot (Feb 04 2025 at 10:55):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-04 branch from nightly-testing (specifically 9bdd95bdc7906447e1aea509cf21c8d39633183f), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-02-04 --nightlysha=9bdd95bdc7906447e1aea509cf21c8d39633183f

github mathlib4 bot (Feb 06 2025 at 01:34):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-05 branch from nightly-testing (specifically 8a2d338ba77347504a3a5a57fe4401d9ddf05d01), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-02-05 --nightlysha=8a2d338ba77347504a3a5a57fe4401d9ddf05d01

github mathlib4 bot (Feb 06 2025 at 10:24):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-06 branch from nightly-testing (specifically fdd759714b98d9c371a832e842643255a385e9e9), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-02-06 --nightlysha=fdd759714b98d9c371a832e842643255a385e9e9

github mathlib4 bot (Feb 10 2025 at 03:31):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-09 branch from nightly-testing (specifically 370e197c3682b1b952160e58965fbb734bc23c26), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-02-09 --nightlysha=370e197c3682b1b952160e58965fbb734bc23c26

github mathlib4 bot (Feb 10 2025 at 10:27):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-10 branch from nightly-testing (specifically e2649ed629bd663355c3cb6ac5535151fa7e47b3), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-02-10 --nightlysha=e2649ed629bd663355c3cb6ac5535151fa7e47b3

github mathlib4 bot (Feb 11 2025 at 11:09):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-11 branch from nightly-testing (specifically 619a1ebba2f05fe0d3c1147e9628ec361175bea6), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-02-11 --nightlysha=619a1ebba2f05fe0d3c1147e9628ec361175bea6

github mathlib4 bot (Feb 13 2025 at 00:29):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-12 branch from nightly-testing (specifically 5eae4dcb283ac0db0f41f06df2ae8bb0761add4b), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-02-12 --nightlysha=5eae4dcb283ac0db0f41f06df2ae8bb0761add4b

github mathlib4 bot (Feb 13 2025 at 13:29):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-13 branch from nightly-testing (specifically 5c7de27570615977f1d1a584a0f695487198d86e), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-02-13 --nightlysha=5c7de27570615977f1d1a584a0f695487198d86e

github mathlib4 bot (Feb 16 2025 at 23:51):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-16 branch from nightly-testing (specifically ca6d4da0ff6cfe9c3e200119dca942a302da5521), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-02-16 --nightlysha=ca6d4da0ff6cfe9c3e200119dca942a302da5521

github mathlib4 bot (Feb 17 2025 at 13:36):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-17 branch from nightly-testing (specifically 1027a18fb029a2d22e0ca36800e9da75d75fd883), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-02-17 --nightlysha=1027a18fb029a2d22e0ca36800e9da75d75fd883

github mathlib4 bot (Feb 18 2025 at 13:34):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-18 branch from nightly-testing (specifically c5db03bc3823a4bb1c5982e179bf6bcd51cb8d33), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-02-18 --nightlysha=c5db03bc3823a4bb1c5982e179bf6bcd51cb8d33

github mathlib4 bot (Feb 19 2025 at 12:06):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-19 branch from nightly-testing (specifically 7c50f8ced4c4698d6b5fff06a9a3bbad0918687e), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-02-19 --nightlysha=7c50f8ced4c4698d6b5fff06a9a3bbad0918687e

github mathlib4 bot (Feb 20 2025 at 11:25):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-20 branch from nightly-testing (specifically 11dafdf912525bd451817754e52808e9d905b629), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-02-20 --nightlysha=11dafdf912525bd451817754e52808e9d905b629

github mathlib4 bot (Feb 25 2025 at 04:13):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-24 branch from nightly-testing (specifically 2bfa3eb705b0fe9d6cdc11f91f728f66b1720dd5), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-02-24 --nightlysha=2bfa3eb705b0fe9d6cdc11f91f728f66b1720dd5

github mathlib4 bot (Feb 25 2025 at 22:30):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-25 branch from nightly-testing (specifically a429f616174b54dc85e0154c84bb2d46879e70ab), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-02-25 --nightlysha=a429f616174b54dc85e0154c84bb2d46879e70ab

github mathlib4 bot (Feb 26 2025 at 22:41):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-26 branch from nightly-testing (specifically aaaee1505b7ad5fa5afb79aeb30a7d71d4f9c7f5), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-02-26 --nightlysha=aaaee1505b7ad5fa5afb79aeb30a7d71d4f9c7f5

github mathlib4 bot (Feb 27 2025 at 09:37):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-27 branch from nightly-testing (specifically 945c66e068c4e874261a90232fe9e5e35975c258), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-02-27 --nightlysha=945c66e068c4e874261a90232fe9e5e35975c258

github mathlib4 bot (Mar 01 2025 at 00:40):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-02-28 branch from nightly-testing (specifically 5aee0a154d404a5a1aa14f3687c1a1d0d7cb9a46), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-02-28 --nightlysha=5aee0a154d404a5a1aa14f3687c1a1d0d7cb9a46

github mathlib4 bot (Mar 02 2025 at 10:38):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-02 branch from nightly-testing (specifically f77cdc2ac5bc49894441dc437e08ae4d40f3271a), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-03-02 --nightlysha=f77cdc2ac5bc49894441dc437e08ae4d40f3271a

github mathlib4 bot (Mar 03 2025 at 10:20):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-03 branch from nightly-testing (specifically 25e831ed30f19e534c0e14ca2ba8c5a785e7711f), and then PR that to "bump/v4.18.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.18.0" --nightlydate=2025-03-03 --nightlysha=25e831ed30f19e534c0e14ca2ba8c5a785e7711f

Johan Commelin (Mar 05 2025 at 06:06):

It's been a bit silent here. I wonder why.

Johan Commelin (Mar 05 2025 at 06:09):

https://github.com/leanprover-community/mathlib4/actions/workflows/nightly_detect_failure.yml :shrug:

Johan Commelin (Mar 05 2025 at 20:10):

I pushed a fix to nightly-testing.

github mathlib4 bot (Mar 05 2025 at 20:40):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-05 branch from nightly-testing (specifically dc26fc02df4023439f1359ce63a1b7c2ed6cc79d), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-05 --nightlysha=dc26fc02df4023439f1359ce63a1b7c2ed6cc79d

github mathlib4 bot (Mar 06 2025 at 10:33):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-06 branch from nightly-testing (specifically 769e5739ce63a2ec8970b115f09c02cdf8255cda), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-06 --nightlysha=769e5739ce63a2ec8970b115f09c02cdf8255cda

github mathlib4 bot (Mar 10 2025 at 07:40):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-09 branch from nightly-testing (specifically 21ebdb2ad2d0096a136ba23ec43ffa98f68f0962), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-09 --nightlysha=21ebdb2ad2d0096a136ba23ec43ffa98f68f0962

github mathlib4 bot (Mar 10 2025 at 10:28):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-10 branch from nightly-testing (specifically f946d24de494227fcbef6ed1a73b5f4a8bde1bb1), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-10 --nightlysha=f946d24de494227fcbef6ed1a73b5f4a8bde1bb1

github mathlib4 bot (Mar 11 2025 at 10:30):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-11 branch from nightly-testing (specifically a75783f538090ee16c118d9583f3e5576a17cd7d), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-11 --nightlysha=a75783f538090ee16c118d9583f3e5576a17cd7d

github mathlib4 bot (Mar 13 2025 at 12:34):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-12 branch from nightly-testing (specifically 759a343fcbe32736f2daf14cabc24daebc9f5a25), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-12 --nightlysha=759a343fcbe32736f2daf14cabc24daebc9f5a25

github mathlib4 bot (Mar 14 2025 at 13:34):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-14 branch from nightly-testing (specifically 9cb2a54e1ffd8914b9e0e46de954703a37827f9e), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-14 --nightlysha=9cb2a54e1ffd8914b9e0e46de954703a37827f9e

github mathlib4 bot (Mar 15 2025 at 11:05):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-15 branch from nightly-testing (specifically 950e64cf316acd5865d007144850dcc4d230381c), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-15 --nightlysha=950e64cf316acd5865d007144850dcc4d230381c

github mathlib4 bot (Mar 17 2025 at 09:00):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-16 branch from nightly-testing (specifically 69eb24d5020265f3fc2048e69137faa1b368ee67), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-16 --nightlysha=69eb24d5020265f3fc2048e69137faa1b368ee67

github mathlib4 bot (Mar 17 2025 at 14:58):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-17 branch from nightly-testing (specifically 0b0ab2589bbb44452061502e9cb849837c9c25d2), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-17 --nightlysha=0b0ab2589bbb44452061502e9cb849837c9c25d2

github mathlib4 bot (Mar 19 2025 at 04:11):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-18 branch from nightly-testing (specifically b266c88eaaff9448445982628b6814ef2f94a7df), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-18 --nightlysha=b266c88eaaff9448445982628b6814ef2f94a7df

github mathlib4 bot (Mar 19 2025 at 13:46):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-19 branch from nightly-testing (specifically bfb212af9d68914d3bcc24b863982969d89d861b), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-19 --nightlysha=bfb212af9d68914d3bcc24b863982969d89d861b

github mathlib4 bot (Mar 20 2025 at 23:30):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-20 branch from nightly-testing (specifically 390f4edd30d68d493e6b38527f2a73646aa30293), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-20 --nightlysha=390f4edd30d68d493e6b38527f2a73646aa30293

github mathlib4 bot (Mar 21 2025 at 15:38):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-21 branch from nightly-testing (specifically 7c56b4c877c1b368d8b76a9bafa5ecbcaf0a43b2), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-21 --nightlysha=7c56b4c877c1b368d8b76a9bafa5ecbcaf0a43b2

github mathlib4 bot (Mar 23 2025 at 19:56):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-22 branch from nightly-testing (specifically 0336b0207f74597b520457c4de723c3bad571a2c), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-22 --nightlysha=0336b0207f74597b520457c4de723c3bad571a2c

github mathlib4 bot (Mar 24 2025 at 20:01):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-24 branch from nightly-testing (specifically e7f18a305a91a997d0b68d407e433b78ea51d60a), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-24 --nightlysha=e7f18a305a91a997d0b68d407e433b78ea51d60a

github mathlib4 bot (Mar 25 2025 at 23:42):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-25 branch from nightly-testing (specifically ed4fcfffeca0d59158ff44e2aa842d4709ff446b), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-25 --nightlysha=ed4fcfffeca0d59158ff44e2aa842d4709ff446b

github mathlib4 bot (Mar 28 2025 at 11:13):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-28 branch from nightly-testing (specifically 07234560b588005c159bd00a0e81e7546f924ce4), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-28 --nightlysha=07234560b588005c159bd00a0e81e7546f924ce4

github mathlib4 bot (Mar 29 2025 at 13:35):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-29 branch from nightly-testing (specifically a1b8d7845467111b2d9206691d54947917deaac9), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-29 --nightlysha=a1b8d7845467111b2d9206691d54947917deaac9

github mathlib4 bot (Mar 30 2025 at 10:33):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-30 branch from nightly-testing (specifically ab98a3ffaa98586009f793bbdd18d80d6ecc5d79), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-30 --nightlysha=ab98a3ffaa98586009f793bbdd18d80d6ecc5d79

github mathlib4 bot (Mar 31 2025 at 12:00):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-03-31 branch from nightly-testing (specifically 44a2fd5edc38e4760b008956991d62cb65917977), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-03-31 --nightlysha=44a2fd5edc38e4760b008956991d62cb65917977

github mathlib4 bot (Apr 01 2025 at 22:21):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-04-01 branch from nightly-testing (specifically aed9d747c0fa0a811af70c98c323f2d54a4e74ac), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-04-01 --nightlysha=aed9d747c0fa0a811af70c98c323f2d54a4e74ac

github mathlib4 bot (Apr 02 2025 at 23:08):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-04-02 branch from nightly-testing (specifically d66f383244a70111a71e348e40aff03745c4ac02), and then PR that to "bump/v4.19.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.19.0" --nightlydate=2025-04-02 --nightlysha=d66f383244a70111a71e348e40aff03745c4ac02

github mathlib4 bot (Apr 04 2025 at 03:40):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-04-03 branch from nightly-testing (specifically b4d11241f700b09f70f513e2f5ebec8863113059), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-03 --nightlysha=b4d11241f700b09f70f513e2f5ebec8863113059

github mathlib4 bot (Apr 04 2025 at 10:45):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-04-04 branch from nightly-testing (specifically 7e3ec380a557ceb5c51f157aea6f72c3f14bc317), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-04 --nightlysha=7e3ec380a557ceb5c51f157aea6f72c3f14bc317

Kim Morrison (Apr 05 2025 at 01:23):

I think this reminder is sufficiently reliable, and uncomplicated, that the bot should just do it as well as posting about it.

github mathlib4 bot (Apr 05 2025 at 01:37):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-04-04 branch from nightly-testing (specifically 7e3ec380a557ceb5c51f157aea6f72c3f14bc317), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-04 --nightlysha=7e3ec380a557ceb5c51f157aea6f72c3f14bc317

Johan Commelin (Apr 07 2025 at 16:24):

Kim Morrison said:

I think this reminder is sufficiently reliable, and uncomplicated, that the bot should just do it as well as posting about it.

I hope that #23793 does that

github mathlib4 bot (Apr 08 2025 at 02:28):

:working_on_it:: it looks like it's time to create a new bump/nightly-2025-04-07 branch from nightly-testing (specifically b7aab63cacec62673c58dccf1a1e167ecc495f0f), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-07 --nightlysha=b7aab63cacec62673c58dccf1a1e167ecc495f0f

Johan Commelin (Apr 09 2025 at 04:13):

Johan Commelin said:

Kim Morrison said:

I think this reminder is sufficiently reliable, and uncomplicated, that the bot should just do it as well as posting about it.

I hope that #23793 does that

That didn't work :sad:
https://github.com/leanprover-community/mathlib4/actions/runs/14347039415/job/40218701624#step:14:26

Johan Commelin (Apr 09 2025 at 04:18):

I hope #23856 fixes it

Johan Commelin (Apr 10 2025 at 04:03):

Another attempt to fix things: #23899

github mathlib4 bot (Apr 10 2025 at 08:34):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-04-09 branch from nightly-testing (specifically 157a68078c492a194022e1d97461507e6ce59c71), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-09 --nightlysha=157a68078c492a194022e1d97461507e6ce59c71

Johan Commelin (Apr 10 2025 at 08:35):

Thank you bot!

Kim Morrison (Apr 10 2025 at 08:40):

@Johan Commelin, you added a :working_on_it: emoji, but there's no PR or zulip post.

Johan Commelin (Apr 10 2025 at 08:41):

I'm working on it. As the emoji says.

Johan Commelin (Apr 10 2025 at 08:41):

@Kim Morrison What is the spelling these days? zipWith or merge?

Johan Commelin (Apr 10 2025 at 08:41):

There's a bunch of conflicts about that.

Johan Commelin (Apr 10 2025 at 08:42):

If you would rather fix them yourselves, I'm happy to abort my :working_on_it:

Markus Himmel (Apr 10 2025 at 08:44):

Assuming you're talking about Option, merge is the correct name now (lean4#7851).

github mathlib4 bot (Apr 10 2025 at 12:35):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-04-10 branch from nightly-testing (specifically b4367811d208c50064e5d6cbfe20b601e72e675a), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-10 --nightlysha=b4367811d208c50064e5d6cbfe20b601e72e675a

Johan Commelin (Apr 14 2025 at 09:04):

This thread has been annoyingly silent since I've tried to automate the running of this script...

Johan Commelin (Apr 14 2025 at 09:05):

Ooh, maybe that's just because branch#nightly-testing is broken?

Markus Himmel (Apr 14 2025 at 09:07):

Could it be because we skipped several nightlies? Before the 2025-04-14 nightly which released a few minutes ago, the most recent nightly is 2025-04-10.

Johan Commelin (Apr 14 2025 at 09:20):

Aah, I didn't realise that!

github mathlib4 bot (Apr 15 2025 at 09:10):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-04-14 branch from nightly-testing (specifically 502763ce50606727068031da926036ac415b9944), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-14 --nightlysha=502763ce50606727068031da926036ac415b9944

github mathlib4 bot (Apr 16 2025 at 10:23):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-04-16 branch from nightly-testing (specifically 908d1720cb6a97f2f9118da71465af28855a3eea), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-16 --nightlysha=908d1720cb6a97f2f9118da71465af28855a3eea

github mathlib4 bot (Apr 19 2025 at 20:32):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-04-19 branch from nightly-testing (specifically 7e1178d897c64fca384e902ea5298d99491f4e16), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-19 --nightlysha=7e1178d897c64fca384e902ea5298d99491f4e16

github mathlib4 bot (Apr 20 2025 at 09:33):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-04-20 branch from nightly-testing (specifically 04cea2442cb64efe013904b87cae551507694c23), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-20 --nightlysha=04cea2442cb64efe013904b87cae551507694c23

Kim Morrison (Apr 20 2025 at 09:42):

I know other things are going on this week, but we do need to diagnose this script at some point. It is succeeding fine locally, so hopefully it should work for the bot too.

github mathlib4 bot (Apr 20 2025 at 10:12):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-04-20 branch from nightly-testing (specifically 04cea2442cb64efe013904b87cae551507694c23), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-20 --nightlysha=04cea2442cb64efe013904b87cae551507694c23

Kim Morrison (Apr 20 2025 at 12:08):

Hmm, and this one shouldn't even have been attempted!

github mathlib4 bot (Apr 20 2025 at 13:36):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-04-20 branch from nightly-testing (specifically 04cea2442cb64efe013904b87cae551507694c23), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-20 --nightlysha=04cea2442cb64efe013904b87cae551507694c23

github mathlib4 bot (Apr 21 2025 at 23:26):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-04-21 branch from nightly-testing (specifically baf884f022743fe2d457d778610456a718bc471f), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-21 --nightlysha=baf884f022743fe2d457d778610456a718bc471f

github mathlib4 bot (Apr 25 2025 at 13:21):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-04-25 branch from nightly-testing (specifically b7a687535bfa626b79c5554e6f7e2a6dfd15339a), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-25 --nightlysha=b7a687535bfa626b79c5554e6f7e2a6dfd15339a

github mathlib4 bot (Apr 26 2025 at 16:54):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-04-26 branch from nightly-testing (specifically 637398a215a1ec7aadc4de0138c5bd4527296279), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-26 --nightlysha=637398a215a1ec7aadc4de0138c5bd4527296279

github mathlib4 bot (Apr 27 2025 at 21:39):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-04-27 branch from nightly-testing (specifically 26e8de2dfae04438c9cd6da1fa9df74d89f70e6b), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-27 --nightlysha=26e8de2dfae04438c9cd6da1fa9df74d89f70e6b

github mathlib4 bot (Apr 28 2025 at 09:49):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-04-28 branch from nightly-testing (specifically 91ba50b9ac2717983d780a776d2a36d7eb989509), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-28 --nightlysha=91ba50b9ac2717983d780a776d2a36d7eb989509

github mathlib4 bot (Apr 29 2025 at 15:16):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-04-29 branch from nightly-testing (specifically 5afdea540abf6226b130896e2c1ae3e06de1c3bb), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-29 --nightlysha=5afdea540abf6226b130896e2c1ae3e06de1c3bb

github mathlib4 bot (Apr 30 2025 at 13:44):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-04-30 branch from nightly-testing (specifically 4dd235e6045ca31c51dace4dcff464a16170359c), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-04-30 --nightlysha=4dd235e6045ca31c51dace4dcff464a16170359c

github mathlib4 bot (May 01 2025 at 16:40):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-05-01 branch from nightly-testing (specifically 701d7503190076933232fbffd40efc333cae8490), and then PR that to "bump/v4.20.0". To do so semi-automatically, run the following script from mathlib root:

./scripts/create-adaptation-pr.sh --bumpversion="v4.20.0" --nightlydate=2025-05-01 --nightlysha=701d7503190076933232fbffd40efc333cae8490

Last updated: May 02 2025 at 03:31 UTC