Skip to content

fix: lake: small cache issues#12037

Merged
tydeu merged 4 commits intoleanprover:masterfrom
tydeu:lake/remote-cache-fixes
Jan 22, 2026
Merged

fix: lake: small cache issues#12037
tydeu merged 4 commits intoleanprover:masterfrom
tydeu:lake/remote-cache-fixes

Conversation

@tydeu
Copy link
Copy Markdown
Member

@tydeu tydeu commented Jan 18, 2026 •
edited
Loading

This PR fixes two Lake cache issues: a bug where a failed upload would not produce an error and a mistake in the --wfail checks of the cache commands.

@tydeu tydeu added the changelog-lake Lake label Jan 18, 2026
@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 Jan 18, 2026
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Jan 18, 2026 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-01-14 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-01-18 19:39:34)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-01-21 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-01-22 01:01:19)

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Jan 18, 2026
Update lean-toolchain for testing leanprover/lean4#12037
90c3a85
@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 Jan 18, 2026
ghost pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jan 18, 2026
Update lean-toolchain for testing leanprover/lean4#12037
ce74ea4
@ghost ghost added the builds-mathlib CI has verified that Mathlib builds against this PR label Jan 18, 2026
@ghost
Copy link
Copy Markdown

ghost commented Jan 18, 2026 •
edited by ghost
Loading

Mathlib CI status (docs):

@tydeu tydeu changed the title fix: lake: cache blockers for CI integration fix: lake: small cache issues Jan 21, 2026
@tydeu tydeu force-pushed the lake/remote-cache-fixes branch from 2ff2b68 to 8c1ab55 Compare January 22, 2026 00:03
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Jan 22, 2026
Update lean-toolchain for leanprover/lean4#12037
ff5c6b4
ghost pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jan 22, 2026
Update lean-toolchain for leanprover/lean4#12037
365be59
@tydeu tydeu marked this pull request as ready for review January 22, 2026 03:11
@tydeu tydeu enabled auto-merge January 22, 2026 03:11
@tydeu tydeu added this pull request to the merge queue Jan 22, 2026
Merged via the queue into leanprover:master with commit 3bc63ae Jan 22, 2026
16 checks passed
@tydeu tydeu deleted the lake/remote-cache-fixes branch January 22, 2026 17:52
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

builds-mathlib CI has verified that Mathlib builds against this PR changelog-lake Lake 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