Skip to content

Conversation

@tydeu
Copy link
Member

@tydeu tydeu commented Sep 26, 2025

This PR sets restoreAllArtifacts = true in the core build Lake configuration file.

@tydeu tydeu added the changelog-no Do not include this PR in the release changelog label Sep 26, 2025
@tydeu tydeu changed the title chore: `restoreAllArtifacts = true for core chore: restoreAllArtifacts = true for core Sep 26, 2025
@tydeu tydeu force-pushed the lakefile-restoreAllArtifacts branch from 213e206 to 8964b3e Compare September 27, 2025 01:52
@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

Mathlib CI status (docs):

  • ❗ 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:05:10)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ 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:05:11)

@tydeu tydeu added this pull request to the merge queue Sep 27, 2025
Merged via the queue into leanprover:master with commit 05300f7 Sep 27, 2025
16 checks passed
@tydeu tydeu deleted the lakefile-restoreAllArtifacts 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