Skip to content

fix: lake: test flakiness#8580

Draft
tydeu wants to merge 1 commit into
leanprover:masterfrom
tydeu:lake/fix-test-flakiness
Draft

fix: lake: test flakiness#8580
tydeu wants to merge 1 commit into
leanprover:masterfrom
tydeu:lake/fix-test-flakiness

Conversation

@tydeu
Copy link
Copy Markdown
Member

@tydeu tydeu commented Jun 1, 2025

This PR aims to fix the flakiness of some Lake tests in CI.

Currently, this PR serves as a testbed for reproducing and debugging the errors; the fix is still a work-in-progress.

@tydeu tydeu added the merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. label Jun 1, 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 Jun 1, 2025
@ghost

This comment was marked as outdated.

Sign in to view
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Jun 7, 2025
Update lean-toolchain for testing leanprover/lean4#8580
cbfd16d
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jun 7, 2025
Update lean-toolchain for testing leanprover/lean4#8580
2cf3c30
@ghost ghost added the builds-mathlib CI has verified that Mathlib builds against this PR label Jun 7, 2025
@tydeu tydeu force-pushed the lake/fix-test-flakiness branch 2 times, most recently from e8b38fa to cca2632 Compare April 23, 2026 20:56
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing Bot commented Apr 23, 2026 •
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 2e48cd293ae3d8743949baefe6788bd3089dbe13 --onto 30a3fde8aa2968acce441fa37436e51acf55f376. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-23 22:03:50)
  • ✅ Mathlib branch lean-pr-testing-8580 has successfully built against this PR. (2026-04-28 21:06:35) View Log
  • 💥 Mathlib branch lean-pr-testing-8580 build failed against this PR. (2026-05-01 05:10:10) View Log
  • 💥 Mathlib branch lean-pr-testing-8580 build failed against this PR. (2026-05-01 21:41:27) View Log
  • 💥 Mathlib branch lean-pr-testing-8580 build failed against this PR. (2026-05-02 19:54:11) View Log
  • 💥 Mathlib branch lean-pr-testing-8580 build failed against this PR. (2026-05-03 19:30:40) View Log

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Apr 23, 2026 •
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 2e48cd293ae3d8743949baefe6788bd3089dbe13 --onto 3fc99eef102549c743c6c63547983319bfae6f01. You can force reference manual CI using the force-manual-ci label. (2026-04-23 22:03:51)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-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-04-28 20:08:34)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-29 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-05-01 04:20:23)

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 28, 2026
Update lean-toolchain for leanprover/lean4#8580
6ed6629
@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 Apr 28, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 28, 2026
Update lean-toolchain for leanprover/lean4#8580
31d8772
@tydeu tydeu force-pushed the lake/fix-test-flakiness branch from cca2632 to 6f0fda9 Compare May 1, 2026 03:11
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 1, 2026
Update lean-toolchain for leanprover/lean4#8580
6d59896
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request May 1, 2026
Update lean-toolchain for leanprover/lean4#8580
83f1367
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels May 1, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 1, 2026
Update lean-toolchain for leanprover/lean4#8580
b2aaf0a
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request May 1, 2026
Update lean-toolchain for leanprover/lean4#8580
859cc85
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 2, 2026
Update lean-toolchain for leanprover/lean4#8580
4359d70
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request May 2, 2026
Update lean-toolchain for leanprover/lean4#8580
bc00c7d
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 3, 2026
Update lean-toolchain for leanprover/lean4#8580
2086152
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request May 3, 2026
Update lean-toolchain for leanprover/lean4#8580
563a82d
@tydeu tydeu mentioned this pull request May 8, 2026
Merged
pull Bot pushed a commit to VitalyAnkh/lean4 that referenced this pull request May 11, 2026
@tydeu
chore: re-enable Lake tests (leanprover#13692)
f52a18a 
This PR re-enables all of the Lake tests by default. The previous
flakiness appears to have been fixed by leanprover#13559, as multiple runs of
leanprover#8580 demonstrate. The `LAKE_CI` CMake setting and the `lake-ci` label
is kept to potentially enable expensive Lake tests in the future (e.g.,
the online tests that are not currently run in CI).
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

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. 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

@tydeu @leanprover-bot