batteris bump job

Stream: nightly-testing

[Joachim Breitner]

It seems that https://github.com/leanprover-community/batteries/actions/workflows/nightly_bump_toolchain.yml didn’t run as per schedule? Any idea why?

(Bumped manually for now)

[Joachim Breitner]

And can we please stop merging master into nightly-testing so often? Shouldn’t it be enough to do it once per day (maybe opposite the bump, i.e. 12h later)? It’s annoying when one is trying to shepherd the build and then it gets cancelled because of a commit to master.

(Or am I the only one who runs into this?)

[Joachim Breitner]

Hmm, and would it be possible to get mathilb CI running even if batteries doesn’t have the tag?
(I was hoping my PRs would now get tested, with everything in place, but then if failed due to that.)

[Kim Morrison]

Joachim Breitner said:

And can we please stop merging master into nightly-testing so often? Shouldn’t it be enough to do it once per day (maybe opposite the bump, i.e. 12h later)? It’s annoying when one is trying to shepherd the build and then it gets cancelled because of a commit to master.

(Or am I the only one who runs into this?)

@Joachim Breitner, just to clarify, is this about Batteries (which merges every commit to main into nightly-testing), or about Mathlib (which merges master into nightly-testing every 3 hours).

I'd be happy to make either less frequent!

[Kim Morrison]

Joachim Breitner said:

Hmm, and would it be possible to get mathilb CI running even if batteries doesn’t have the tag?
(I was hoping my PRs would now get tested, with everything in place, but then if failed due to that.)

Sorry, which tag?

[Yaël Dillies]

Joachim Breitner said:

It’s annoying when one is trying to shepherd the build and then it gets cancelled because of a commit to master.

Stupid question: Would disabling cancellation of previous commits solve your annoyance?

[Joachim Breitner]

Kim Morrison schrieb:

Joachim Breitner said:

Joachim Breitner, just to clarify, is this about Batteries (which merges every commit to main into nightly-testing), or about Mathlib (which merges master into nightly-testing every 3 hours).

I'd be happy to make either less frequent!

That was mathlib. I didn't know it's already time based, so maybe I was just unlucky. Every 3h is also reasonable, so if others prefer that then no worries

[Joachim Breitner]

Kim Morrison schrieb:

Joachim Breitner said:

Hmm, and would it be possible to get mathilb CI running even if batteries doesn’t have the tag?
(I was hoping my PRs would now get tested, with everything in place, but then if failed due to that.)

Sorry, which tag?

The nightly-2025-08-02 tag (or branch?) on batteries. It seems that there PR release action checks that the current nightly-with-mathlib release has such a tag in batteries and in mathlib before proceeding to create an adaption branch. This adds friction if mathlib builds (and nightly-with-mathlib advances) but batteries failed (e.g. in tests).

Again, not super important, I was mostly just ranting in the moment.