feat(CI): add upload & download via lake cache

[tydeu]

This PR adds upload and download support for Mathlib's CI build artifacts via lake cache, Lake's native artifact cache system. It runs alongside the existing lake exe cache tooling during a transition/validation period.

Changes

lakefile.lean:

• enableArtifactCache := true — opt into Lake's artifact cache
• restoreAllArtifacts := true — restore all artifacts (not just the minimal set) from cache, as various tooling expects Mathlib artifacts to be in the build directory.
• platformIndependent := true — .olean files built in CI are used cross-platform
• fixedToolchain := true — Mathlib is tied to the toolchain it was built with

.github/workflows/build_template.yml:

• Set LAKE_CACHE_DIR: .lake/cache so Lake stores its artifact cache inside .lake/, which is already within the rw mount permitted by landrun.
• Pass LAKE_CACHE_DIR through landrun's --env flag so it is visible to sandboxed steps.
• In the build job, after the build, run lake build --no-build -o .lake/outputs.jsonl + lake cache stage to collect artifacts into a staging directory, then upload that as a GitHub Actions artifact.
• In the new upload_lake_cache job, download the staging directory and upload it to the Cloudflare cache via lake cache put-staged.
• In the new verify_lake_cache job, build Mathlib's dependencies, fetch the Mathlib Lake cache with lake cache get, and verify completeness with lake build --no-build --rehash -v.

🤖 Prepared with Claude Code

---

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[tydeu]

@marcelolynch This PR deploys the new Lake cache to Mathlib. It is still a work-in-progress, but it seems reasonable to alert you now, just in case you might already have thoughts about the PR's design.

[marcelolynch]

On a general note: I understand that this PR is open against nightly-testing because it depends on some lake changes that will hit nightly-testing first, so to iterate / fix things it's a suitable arena, but I think we should try to make the actual deployments using intentional PRs to mathlib4. In other words: let's not deploy this change bundled with an adaptation PR from nightly-testing / as part of a toolchain bump, and rather let's create specific PRs (that we can revert, review separately, etc.) to deploy this change. Let me know what you think of this!

[tydeu]

@marcelolynch The plan was to merge the finished version of this PR into nightly-testing to build up the cache and help debug any issues. That is also why the verification job is not currently continue-on-error. If necessary, we can revert before the next toolchain release.