Skip to content

fix: lake-ci test glob#12876

Merged
tydeu merged 1 commit intoleanprover:masterfrom
tydeu:fix-lake-ci
Mar 11, 2026
Merged

fix: lake-ci test glob#12876
tydeu merged 1 commit intoleanprover:masterfrom
tydeu:fix-lake-ci

Conversation

@tydeu
Copy link
Member

@tydeu tydeu commented Mar 11, 2026

This PR fixes an error in the test globs for lake-ci. With lake-ci, the shake test was created twice, which CMake does not accept.

@tydeu tydeu added the changelog-no Do not include this PR in the release changelog label Mar 11, 2026
@tydeu
Copy link
Member Author

tydeu commented Mar 11, 2026

FYI, @kim-em, this glob issue appears to be why #12540 is currently failing.

@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 Mar 11, 2026
@mathlib-lean-pr-testing
Copy link

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-03-10 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-11 02:05:39)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-10 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-03-11 02:05:40)

@tydeu tydeu added the lake-ci Run all Lake tests label Mar 11, 2026
@tydeu tydeu added this pull request to the merge queue Mar 11, 2026
Merged via the queue into leanprover:master with commit cd85b93 Mar 11, 2026
38 checks passed
@tydeu tydeu deleted the fix-lake-ci branch March 11, 2026 04:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-no Do not include this PR in the release changelog lake-ci Run all Lake tests 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