Skip to content

chore: test adaptation PR CI#14170

Draft
Garmelon wants to merge 2 commits into
masterfrom
joscha/test-adaptations
Draft

chore: test adaptation PR CI#14170
Garmelon wants to merge 2 commits into
masterfrom
joscha/test-adaptations

Conversation

@Garmelon

@Garmelon Garmelon commented Jun 24, 2026

Copy link
Copy Markdown
Contributor

No description provided.

@Garmelon Garmelon added the downstream Request a downstream-lean4 adaptation PR. label Jun 24, 2026
@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 Jun 24, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Jun 24, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c50c2ba69d4d12a9b6ef8f2d451627c63d326409 --onto 0a8abcb19f7daf70ac75e5899ee3fd42f54adb33. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-24 16:05:41)
  • ✅ Mathlib branch lean-pr-testing-14170 has successfully built against this PR. (2026-06-24 18:53:39) View Log
  • ✅ Mathlib branch lean-pr-testing-14170 has successfully built against this PR. (2026-06-24 20:25:54) View Log

@leanprover-bot

leanprover-bot commented Jun 24, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c50c2ba69d4d12a9b6ef8f2d451627c63d326409 --onto 2e72131c7f007ab9d2538b676106c5141b24ba22. You can force reference manual CI using the force-manual-ci label. (2026-06-24 16:05:42)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-06-24 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-06-24 17:56:33)

@downstream-lean4

downstream-lean4 Bot commented Jun 24, 2026 •
edited
Loading

Copy link
Copy Markdown

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

@Garmelon Garmelon force-pushed the joscha/test-adaptations branch from d0903bd to b9be87b Compare June 24, 2026 17:20
@github-actions github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Jun 24, 2026
@downstream-lean4 downstream-lean4 Bot mentioned this pull request Jun 24, 2026
Open
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Jun 24, 2026
@Garmelon
Revert "foo"
6a5fe63 
This reverts commit b9be87b.
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Jun 24, 2026
Update lean-toolchain for leanprover/lean4#14170
7091f77
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jun 24, 2026
Update lean-toolchain for leanprover/lean4#14170
5e372a9
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

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