Skip to content

chore: tweak adaptation PR "waiting for CI" message - #14999

Merged
Garmelon merged 1 commit into
masterfrom
joscha/ci-green-msg
Sep 3, 2026
Merged

chore: tweak adaptation PR "waiting for CI" message#14999
Garmelon merged 1 commit into
masterfrom
joscha/ci-green-msg

Conversation

@Garmelon

@Garmelon Garmelon commented Sep 2, 2026

Copy link
Copy Markdown
Contributor

Instead of saying that it's waiting for CI to be green, it's now mentioning the toolchain, which is what it's actually waiting for.

@Garmelon
Garmelon requested a review from kim-em as a code owner September 2, 2026 15:44
@Garmelon Garmelon added the downstream Request a downstream-lean4 adaptation PR. label Sep 2, 2026
@github-actions github-actions Bot added toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN labels Sep 2, 2026
@downstream-lean4 downstream-lean4 Bot mentioned this pull request Sep 2, 2026
Merged
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Sep 2, 2026
@leanprover-bot

leanprover-bot commented Sep 2, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ✅ Reference manual branch lean-pr-testing-14999 has successfully built against this PR. (2026-09-02 16:16:57) View Log
  • 🟡 Reference manual branch lean-pr-testing-14999 build against this PR didn't complete normally. (2026-09-02 16:19:12) View Log
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 137a88d9d363d6f0c60de75d4cef02a26f38962e --onto 19c79593c47bb8dd3371327c08fc80775d8488af. You can force reference manual CI using the force-manual-ci label. (2026-09-03 14:56:17)

@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Sep 2, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Sep 2, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ✅ Mathlib branch lean-pr-testing-14999 has successfully built against this PR. (2026-09-02 17:25:44) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 137a88d9d363d6f0c60de75d4cef02a26f38962e --onto c632a0a0e434a951cdcf61bb4da3344abadd5587. You can force Mathlib CI using the force-mathlib-ci label. (2026-09-03 14:56:15)

@Garmelon
Garmelon added this pull request to the merge queue Sep 2, 2026
@Garmelon Garmelon added downstream Request a downstream-lean4 adaptation PR. and removed downstream Request a downstream-lean4 adaptation PR. labels Sep 2, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Sep 2, 2026
@Garmelon
Garmelon force-pushed the joscha/ci-green-msg branch from 0cfa05e to 24a1ea7 Compare September 3, 2026 13:55
@Garmelon
Garmelon enabled auto-merge September 3, 2026 13:55
@Garmelon
Garmelon added this pull request to the merge queue Sep 3, 2026
@downstream-lean4

downstream-lean4 Bot commented Sep 3, 2026

Copy link
Copy Markdown

The adaptation PR for this PR is leanprover/downstream-lean4#34.

Merged via the queue into master with commit 5877442 Sep 3, 2026
20 checks passed
@Garmelon
Garmelon deleted the joscha/ci-green-msg branch September 4, 2026 00:01
downstream-lean4 Bot added a commit to leanprover/downstream-lean4 that referenced this pull request Sep 4, 2026
@downstream-lean4
[#14999] chore: tweak adaptation PR "waiting for CI" message (#34)
ad30876 
This is the adaptation PR for leanprover/lean4#14999.

---------

Co-authored-by: downstream-lean4[bot] <downstream-lean4[bot]@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR builds-mathlib CI has verified that Mathlib builds against this PR downstream Request a downstream-lean4 adaptation PR. mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@Garmelon @leanprover-bot