Skip to content

chore: fix awaiting-mathlib.yml #8480

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
kim-em merged 3 commits into from
May 26, 2025
Merged

chore: fix awaiting-mathlib.yml #8480

kim-em merged 3 commits into from
May 26, 2025

Conversation

@kim-em
Copy link
Collaborator

@kim-em kim-em commented May 26, 2025

This PR hopefully fixes a problem from #8471, which even the most cursory testing (by me!) should have detected.

@kim-em kim-em added the awaiting-mathlib We should not merge this until we have a successful Mathlib build label May 26, 2025
@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 May 26, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented May 26, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 383f68f8063d4eec7d0c4ebe9258705af9fedcc3 --onto 2a1354b3cc1eb05e1b67c656d2172ada8f54a937. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-26 01:25:29)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bdbb6597657869edcb458337cd8ee6b25566df09 --onto 2a1354b3cc1eb05e1b67c656d2172ada8f54a937. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-26 01:55:33)

@kim-em kim-em force-pushed the fix_awaiting_mathlib branch from 440aa88 to dce8f9f Compare May 26, 2025 01:27
@kim-em kim-em added force-mathlib-ci and removed awaiting-mathlib We should not merge this until we have a successful Mathlib build force-mathlib-ci labels May 26, 2025
@kim-em kim-em added this pull request to the merge queue May 26, 2025
Merged via the queue into master with commit c1866a7 May 26, 2025
21 of 23 checks passed
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

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.

3 participants

@kim-em @leanprover-community-bot