Zulip Chat Archive

Stream: nightly-testing

Topic: Cslib bump branch reminders

github mathlib4 bot (Nov 21 2025 at 13:19):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-11-21 branch from nightly-testing (specifically 81ad2f2dab4b4d54e9791b8eaa195db261cc4276), and then PR that to bump/v4.27.0. To do so semi-automatically, run the following script from Cslib root:

./scripts/create-adaptation-pr.sh --bumpversion=v4.27.0 --nightlydate=2025-11-21 --nightlysha=81ad2f2dab4b4d54e9791b8eaa195db261cc4276

github mathlib4 bot (Nov 22 2025 at 00:56):

./scripts/create-adaptation-pr.sh --bumpversion=v4.27.0 --nightlydate=2025-11-21 --nightlysha=81ad2f2dab4b4d54e9791b8eaa195db261cc4276

github mathlib4 bot (Nov 23 2025 at 19:25):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-11-23 branch from nightly-testing (specifically 668b7d3a3617a2500130ad21d7f18d0ce948dd61), and then PR that to bump/v4.27.0. To do so semi-automatically, run the following script from Cslib root:

./scripts/create-adaptation-pr.sh --bumpversion=v4.27.0 --nightlydate=2025-11-23 --nightlysha=668b7d3a3617a2500130ad21d7f18d0ce948dd61

Chris Henson (Nov 23 2025 at 19:38):

@Kim Morrison It seems like the lakefile.toml is consistently a merge conflict for these. I saw yesterday in cslib#179 you made it use the current nightly, is that what we should be doing? If so, can create-adaptation-pr.sh just be made to use the lakefile from nightly-testing?

Kim Morrison (Nov 23 2025 at 21:33):

Yes, we need to diverge from the Mathlib behaviour here because we automatically modify the lakefile.toml each night (unlike Mathlib). There's existing code in this script to prefer changes to lean-toolchain and lake-manifest.json frmo the nightly-testing side, we should just also add lakefile.toml to that.

Kim Morrison (Nov 23 2025 at 21:40):

cslib#180 addresses the persistent lakefile.toml merge conflicts by automatically preferring the nightly-testing version (like lean-toolchain and lake-manifest.json).

github mathlib4 bot (Dec 14 2025 at 13:17):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2025-12-14 branch from nightly-testing (specifically 3d5395665a10bf7b61e53e7fd049f9358ca11e1f), and then PR that to bump/v4.27.0. To do so semi-automatically, run the following script from Cslib root:

./scripts/create-adaptation-pr.sh --bumpversion=v4.27.0 --nightlydate=2025-12-14 --nightlysha=3d5395665a10bf7b61e53e7fd049f9358ca11e1f

github mathlib4 bot (Jan 24 2026 at 10:10):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2026-01-24 branch from nightly-testing (specifically d8869e6f73ad42cb7252c00e608b0a3c64b28769), and then PR that to bump/v4.28.0. To do so semi-automatically, run the following script from Cslib root:

./scripts/create-adaptation-pr.sh --bumpversion=v4.28.0 --nightlydate=2026-01-24 --nightlysha=d8869e6f73ad42cb7252c00e608b0a3c64b28769

github mathlib4 bot (Jan 24 2026 at 18:50):

./scripts/create-adaptation-pr.sh --bumpversion=v4.28.0 --nightlydate=2026-01-24 --nightlysha=d8869e6f73ad42cb7252c00e608b0a3c64b28769

Chris Henson (Jan 24 2026 at 19:00):

I manually followed the above instructions, though I don't know why the bot posted twice for the same nightly commit/date.

Kim Morrison (Jan 25 2026 at 07:47):

Yes, it's been doing this recently for Mathlib too, and I haven't had time to investigate.

Kim Morrison (Jan 25 2026 at 08:19):

I investigated this and found the root cause. The deduplication logic compares the first 160 characters of the message, but the GitHub Actions run ID is embedded within those characters:

🛠️: Automatic PR creation [failed](https://github.com/leanprover/cslib/actions/runs/XXXXXXXXXXX)...

The run ID differs between workflow runs, so even when everything else (nightly date, SHA, bump version) is identical, the comparison fails and a duplicate is posted.

PRs to fix this (using regex to extract and compare the nightly date and bump branch specifically):

Mathlib: https://github.com/leanprover-community/mathlib4/pull/34398
Batteries: https://github.com/leanprover-community/batteries/pull/1630
Cslib: https://github.com/leanprover/cslib/pull/290

github mathlib4 bot (Jan 25 2026 at 15:44):

./scripts/create-adaptation-pr.sh --bumpversion=v4.28.0 --nightlydate=2026-01-24 --nightlysha=d8869e6f73ad42cb7252c00e608b0a3c64b28769

Chris Henson (Jan 25 2026 at 16:56):

Note that for instance in the above case, any messages in-between by humans will also confuse the workflow. Could we easily change the request to grab a reasonable window of messages (as opposed to the current 'num_before': 1) and use the last one posted by the bot?

Kim Morrison (Jan 25 2026 at 22:24):

Done! PRs to fetch the last 20 messages and look for the most recent bot message:

github mathlib4 bot (Jan 26 2026 at 04:14):

./scripts/create-adaptation-pr.sh --bumpversion=v4.28.0 --nightlydate=2026-01-24 --nightlysha=d8869e6f73ad42cb7252c00e608b0a3c64b28769

Chris Henson (Jan 26 2026 at 04:38):

Hmm, is there still a bug? I notice that in the run linked directly above, it says

###### Last bot message:
🛠️: Automatic PR creation [failed](https://github.com/leanprover/cslib/actions/runs/19571772376). Please create a new bump/nightly-2025-11-21 branch from nightly-testing (specifically 81ad2f2dab4b4d54e9791b8eaa195db261cc4276), and then PR that to bump/v4.27.0. To do so semi-automatically, run the following script from Cslib root:

```bash
./scripts/create-adaptation-pr.sh --bumpversion=v4.27.0 --nightlydate=2025-11-21 --nightlysha=81ad2f2dab4b4d54e9791b8eaa195db261cc4276
```

and this appears to be the very first message in this channel. I don't use Python or the Zulip API much, so the problem isn't jumping out at me. Is it as simple as the order being in reverse of what you expected?

github mathlib4 bot (Jan 26 2026 at 21:46):

./scripts/create-adaptation-pr.sh --bumpversion=v4.28.0 --nightlydate=2026-01-24 --nightlysha=d8869e6f73ad42cb7252c00e608b0a3c64b28769

Kim Morrison (Jan 27 2026 at 00:01):

@Chris Henson You were right — the messages were in reverse order of what I expected. The Zulip API returns messages oldest→newest with anchor: 'newest', so next() was finding the oldest bot message, not the newest.

Fixed by using Bryan's suggestion to add a sender narrow filter, so the API only returns bot messages. This is simpler and also handles the case where there are >20 human messages between bot posts.

PRs:

#34398 (updated)
batteries#1632 (updated)
cslib#295 (new, since cslib#291 was already merged)

github mathlib4 bot (Jan 27 2026 at 00:56):

./scripts/create-adaptation-pr.sh --bumpversion=v4.28.0 --nightlydate=2026-01-24 --nightlysha=d8869e6f73ad42cb7252c00e608b0a3c64b28769

github mathlib4 bot (Jan 29 2026 at 02:13):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2026-01-28 branch from nightly-testing (specifically 62ef5297712f3f15f59441cc215b7c2b68cfa246), and then PR that to bump/v4.29.0. To do so semi-automatically, run the following script from Cslib root:

./scripts/create-adaptation-pr.sh --bumpversion=v4.29.0 --nightlydate=2026-01-28 --nightlysha=62ef5297712f3f15f59441cc215b7c2b68cfa246

github mathlib4 bot (Jan 29 2026 at 12:54):

./scripts/create-adaptation-pr.sh --bumpversion=v4.29.0 --nightlydate=2026-01-28 --nightlysha=62ef5297712f3f15f59441cc215b7c2b68cfa246

github mathlib4 bot (Jan 29 2026 at 15:52):

./scripts/create-adaptation-pr.sh --bumpversion=v4.29.0 --nightlydate=2026-01-28 --nightlysha=62ef5297712f3f15f59441cc215b7c2b68cfa246

github mathlib4 bot (Jan 30 2026 at 13:31):

:working_on_it:: Automatic PR creation failed. Please create a new bump/nightly-2026-01-30 branch from nightly-testing (specifically 1f95e11986f04f916b4655cf3e0ce0105851523e), and then PR that to bump/v4.29.0. To do so semi-automatically, run the following script from Cslib root:

./scripts/create-adaptation-pr.sh --bumpversion=v4.29.0 --nightlydate=2026-01-30 --nightlysha=1f95e11986f04f916b4655cf3e0ce0105851523e

Last updated: Feb 28 2026 at 14:05 UTC