Skip to content

chore: fix ci for new test suite#12704

Merged
Garmelon merged 12 commits intomasterfrom
joscha/fix-ci-for-new-test-suite
Feb 27, 2026
Merged

chore: fix ci for new test suite#12704
Garmelon merged 12 commits intomasterfrom
joscha/fix-ci-for-new-test-suite

Conversation

@Garmelon
Copy link
Contributor

No description provided.

@Garmelon Garmelon requested a review from kim-em as a code owner February 26, 2026 13:40
@Garmelon Garmelon added the release-ci Enable all CI checks for a PR, like is done for releases label Feb 26, 2026
@Garmelon Garmelon force-pushed the joscha/fix-ci-for-new-test-suite branch 4 times, most recently from 5f16d2f to 441c72e Compare February 26, 2026 15:45
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 26, 2026
@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Feb 26, 2026

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 846420dabab15cec6d4c095069dc34d7a9ba4b59 --onto c595413fccaa47ebdc399d9b817c17425687fc26. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-26 17:12:26)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase adf3e5e6612e709c65e8edabae6b54590ca46c4d --onto c595413fccaa47ebdc399d9b817c17425687fc26. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-27 01:33:18)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b4f768b67f4d9a1573055a8a7d1d4bee5773326d --onto 87ec768a509c45987a7d73258da0cc1ef047925c. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-27 13:39:50)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 81a5eb55d54f2be749f1e419f250787497a6eb10 --onto 87ec768a509c45987a7d73258da0cc1ef047925c. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-27 21:58:22)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 54df5173d2eaa34326a38d664746c51d4ac79b93 --onto 87ec768a509c45987a7d73258da0cc1ef047925c. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-27 23:37:41)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Feb 26, 2026

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 846420dabab15cec6d4c095069dc34d7a9ba4b59 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-26 17:12:28)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase adf3e5e6612e709c65e8edabae6b54590ca46c4d --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-27 01:33:20)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase b4f768b67f4d9a1573055a8a7d1d4bee5773326d --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-27 13:39:52)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 81a5eb55d54f2be749f1e419f250787497a6eb10 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-27 21:58:24)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 54df5173d2eaa34326a38d664746c51d4ac79b93 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-27 23:37:42)

@Garmelon Garmelon force-pushed the joscha/fix-ci-for-new-test-suite branch 9 times, most recently from d6b9837 to 0d97516 Compare February 27, 2026 20:39
@Garmelon
Copy link
Contributor Author

elab_bench/big_do.lean seems to crash in the reldebug CI. Before the new test suite, it was only a benchmark and thus it was only executed in the linux lake CI occasionally (where it doesn't crash). Ignoring it doesn't make things worse than pre-new-suite.

@Garmelon Garmelon force-pushed the joscha/fix-ci-for-new-test-suite branch from 0d97516 to d20dba1 Compare February 27, 2026 22:01
@Garmelon Garmelon enabled auto-merge February 27, 2026 22:01
@Garmelon Garmelon added this pull request to the merge queue Feb 27, 2026
Merged via the queue into master with commit 08ab8bf Feb 27, 2026
23 of 24 checks passed
@Garmelon Garmelon deleted the joscha/fix-ci-for-new-test-suite branch February 28, 2026 00:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants