Skip to content

Conversation

@tydeu
Copy link
Member

@tydeu tydeu commented Sep 27, 2025

This PR makes Lake no longer error if build outputs found in a trace file (or in the artifact cache) are ill-formed.

This is caused a problem with the CI cache and is just generally too strict.

@tydeu tydeu added changelog-no Do not include this PR in the release changelog changelog-lake Lake labels Sep 27, 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 Sep 27, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Sep 27, 2025

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-09-26 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. (2025-09-27 01:29:44)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5b8d4d72104e66de541339027b41b7e434c1ab7e --onto ac0b82933f6eac9914011ca2caf38d0e4e991160. You can force Mathlib CI using the force-mathlib-ci label. (2025-09-27 03:02:44)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Sep 27, 2025

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-09-26 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. (2025-09-27 01:29:45)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5b8d4d72104e66de541339027b41b7e434c1ab7e --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-09-27 03:02:46)

github-merge-queue bot pushed a commit that referenced this pull request Sep 27, 2025
This PR invalidates the CI cache for the Linux Lake build job by bumping
the version of the CI cache key.

The CI cache is broken due to a change in the output format in build
traces. This will be fixed in #10586, but this should prevent further
breakages of PRs in the meantime.
@tydeu tydeu force-pushed the lake/fix-output-errors branch from eed0013 to 40a0c9e Compare September 27, 2025 01:51
@tydeu tydeu force-pushed the lake/fix-output-errors branch from 40a0c9e to 78958d9 Compare September 27, 2025 01:52
@tydeu tydeu removed the changelog-lake Lake label Sep 27, 2025
@tydeu tydeu enabled auto-merge September 27, 2025 03:30
@tydeu tydeu added this pull request to the merge queue Sep 27, 2025
Merged via the queue into leanprover:master with commit 18832eb Sep 27, 2025
14 checks passed
@tydeu tydeu deleted the lake/fix-output-errors branch September 27, 2025 03:57
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 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.

3 participants