Skip to content

test: lake: mock remote cache artifact transfers - #14700

Draft
tydeu wants to merge 3 commits into
leanprover:masterfrom
tydeu:lake/cache-transfer-test
Draft

test: lake: mock remote cache artifact transfers#14700
tydeu wants to merge 3 commits into
leanprover:masterfrom
tydeu:lake/cache-transfer-test

Conversation

@tydeu

@tydeu tydeu commented Aug 6, 2026

Copy link
Copy Markdown
Member

This PR adds a Lake test which performs mock artifact transfers to/from a remote cache service using a mock Python HTTP server. This serves as an alternative to the existing online cache test which covers full integration with Reservoir but also requires secrets and network access and is thus ill-suited for CI.

This PR also fixes test_err in the Lake test harness, which did not fail when an Lake invocation unexpectedly succeeded. All tests still pass, so no failures were obscured by this issue.

Test Cases

  • cache put, put-staged, and stage, plus rejected artifact and outputs uploads
  • cache get by --scope and by --repo, --force-download, --mappings-only, revision search and --max-revs, and platform- and toolchain-partitioned revision paths
  • download failures: a missing artifact, a content hash mismatch, a body cut short of its declared Content-Length, a connection closed with no response, a response carrying no body at all, and an error response whose body is not an artifact
  • misreported transfers: a curl that reports no transfer while claiming success, one that reports failure for artifacts that arrived complete, and one that reports success for artifacts it never wrote
  • on-demand artifact fetches during a build, over both bucket and Reservoir URLs
  • the Reservoir batch URL lookup, including a short result list and an API error object
  • artifacts that share a content hash across extensions, which download once and are copied, not hard linked, into place
  • Lake: one unreadable artifact aborts the whole lake cache get #14698: a batch in which one artifact yields no output file must report "failed to download some artifacts" and retain the artifacts that did transfer, rather than abort on the missing file.

Failure case also assert exactly which artifacts remain in the local cache, and those that could poison it assert that a subsequent good fetch still succeeds.

🤖 Prepared with Claude Code

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@tydeu tydeu added the changelog-no Do not include this PR in the release changelog label Aug 6, 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 Aug 6, 2026
@leanprover-bot

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-05 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-08-06 04:43:41)

@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 Aug 6, 2026
tydeu and others added 2 commits August 6, 2026 04:55
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Aug 6, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Aug 6, 2026

Copy link
Copy Markdown

Mathlib CI status (docs):

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Aug 6, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Aug 6, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-no Do not include this PR in the release changelog 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

Development

Successfully merging this pull request may close these issues.

2 participants