Skip to content

chore: [match_pattern] should enforce [expose] #9534

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
Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

chore: [match_pattern] should enforce [expose] #9534

wants to merge 1 commit into from

Conversation

Kha
Copy link
Member

@Kha Kha commented Jul 25, 2025

No description provided.

@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 Jul 25, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jul 25, 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 3f19182afc70bfefadd41588b1329136f11d04a7 --onto 73422d52fd61c3d5bce6f5edb53c6bd698b1b7ba. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-25 15:16:54)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b437232ab6d4ac4f1a63855001d8279dc7803a4f --onto 73422d52fd61c3d5bce6f5edb53c6bd698b1b7ba. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-25 17:04:24)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 98569c7cf02c236b6d25cb46b5c990aea3431c27 --onto 73422d52fd61c3d5bce6f5edb53c6bd698b1b7ba. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-25 21:47:56)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Jul 25, 2025 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 3f19182afc70bfefadd41588b1329136f11d04a7 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-25 15:16:55)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase b437232ab6d4ac4f1a63855001d8279dc7803a4f --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-25 17:04:25)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 98569c7cf02c236b6d25cb46b5c990aea3431c27 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-25 21:47:58)

@Kha Kha force-pushed the push-zxlrzxxssoxk branch 2 times, most recently from 1d090d4 to f1474de Compare July 25, 2025 20:10
@Kha Kha force-pushed the push-zxlrzxxssoxk branch from f1474de to ad97418 Compare July 25, 2025 20:40
@Kha Kha added this pull request to the merge queue Jul 27, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Jul 27, 2025
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
@Kha @leanprover-community-bot @leanprover-bot