Skip to content

chore: debug mismatch w/ CI lake cache#13292

Closed
tydeu wants to merge 1 commit intomasterfrom
debug-lake-cache-ci
Closed

chore: debug mismatch w/ CI lake cache#13292
tydeu wants to merge 1 commit intomasterfrom
debug-lake-cache-ci

Conversation

@tydeu
Copy link
Copy Markdown
Member

@tydeu tydeu commented Apr 6, 2026

No description provided.

@tydeu tydeu mentioned this pull request Apr 6, 2026
Closed
@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 Apr 6, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 6, 2026
Update lean-toolchain for testing leanprover/lean4#13292
1a02949
@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 6, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 6, 2026
Update lean-toolchain for testing leanprover/lean4#13292
e542a14
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Apr 6, 2026
@leanprover-bot
Update lean-toolchain for testing leanprover/lean4#13292
cfcd7e8
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Apr 6, 2026
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Apr 6, 2026 •
edited
Loading

Reference manual CI status:

  • ✅ Reference manual branch lean-pr-testing-13292 has successfully built against this PR. (2026-04-06 18:53:16) View Log
  • 🟡 Reference manual branch lean-pr-testing-13292 build against this PR didn't complete normally. (2026-04-06 18:55:40) View Log
  • ✅ Reference manual branch lean-pr-testing-13292 has successfully built against this PR. (2026-04-07 01:11:26) View Log
  • 🟡 Reference manual branch lean-pr-testing-13292 build against this PR didn't complete normally. (2026-04-07 01:13:59) View Log
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-08 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-08 16:56:40)

@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Apr 6, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 6, 2026 •
edited
Loading

Mathlib CI status (docs):

  • ✅ Mathlib branch lean-pr-testing-13292 has successfully built against this PR. (2026-04-06 19:42:39) View Log
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-04-08 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-04-08 16:56:38)

@tydeu tydeu force-pushed the debug-lake-cache-ci branch from 76db53a to ad4e0d0 Compare April 7, 2026 00:15
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 7, 2026
Update lean-toolchain for leanprover/lean4#13292
d1bca42
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 7, 2026
Update lean-toolchain for leanprover/lean4#13292
0d43b6e
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Apr 7, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#13292
ad8f5aa
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 7, 2026

Mathlib CI status (docs):

@tydeu tydeu force-pushed the debug-lake-cache-ci branch from ad4e0d0 to cb333ff Compare April 8, 2026 16:08
@tydeu
Copy link
Copy Markdown
Member Author

tydeu commented Apr 11, 2026

Debugging has been completed and the trace mismatches have been sufficiently fixed (#13294, #13335), so I am closing this issue. There is still the Leanc mismatch, but it requires a significant refactor (the file could not be templated) for minimal benefit (caching one file), and thus it is not planned to be fixed at the moment.

@tydeu tydeu closed this Apr 11, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em will be requested when the pull request is marked ready for review kim-em is a code owner

Assignees

No one assigned

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR builds-mathlib CI has verified that Mathlib builds against this 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

@tydeu @leanprover-bot