Revert "publish released mirrors' oleans to the Lake cache"

PLAN/Releases.md

@@ -258,26 +258,18 @@ that can disagree with the build.
 
 ### The Lake cache
 
-Every mirror publishes its compiled oleans to a Cloudflare R2 bucket, so a
-consumer of the released set fetches them with `lake cache get` instead of
-compiling the library graph. Without it, depending on `leanprover/hex` costs
-about 10k Lake jobs and half an hour, none of it Mathlib. hex-dev publishes its
-own build the same way, from `.github/workflows/ci.yml`.
+hex-dev publishes its own compiled oleans to a Cloudflare R2 bucket from
+`.github/workflows/ci.yml`, and a consumer can fetch them with `lake cache get`.
+The released mirrors briefly did the same. They no longer do, because measuring
+it showed the fetch cost more than the reuse saved.
 
 The bucket is `hex-cache`. Uploads are signed against R2's S3 API; downloads are
 plain unauthenticated GETs, because Lake's fetcher sends no credentials, so they
-go through the bucket's public host instead. That is why there are two endpoint
-pairs rather than one, and why the bucket must stay publicly readable.
+go through the bucket's public host instead. Hence two endpoint pairs, and hence
+the bucket must stay publicly readable.
 
-Publishing happens only from `main`, after every verification gate, and
-immediately before the terminal cache save. `lake cache put` re-uploads every
-artifact in the mappings file with no check for what is already there, so
-running it per pull request would burn R2's write allowance. The job sets
-`LAKE_ARTIFACT_CACHE`: artifact-cache writes default to off while reads default
-to on, and without it the mappings `-o` records would name artifacts that were
-never put in the cache to upload.
-
-Each mirror needs one secret and four variables:
+Each mirror still carries the credentials, so re-enabling publishing is a change
+to `released-ci.yml` alone rather than a re-provisioning exercise:
 
 | name | kind | purpose |
 | --- | --- | --- |
@@ -287,33 +279,43 @@ Each mirror needs one secret and four variables:
 | `HEX_LAKE_CACHE_ARTIFACT_ENDPOINT_PUBLIC` | variable | public host, downloads |
 | `HEX_LAKE_CACHE_REVISION_ENDPOINT_PUBLIC` | variable | public host, downloads |
 
-The names are Hex-specific because these could otherwise collide with any other
-Lean project in the organization.
-
-`scripts/release/provision_cache_secrets.sh` sets all five on every repository
-in `released-ci.yml`, plus hex-dev. It is idempotent, so adding a mirror and
-re-running it is the whole ceremony; `--check` takes no token and reports what
-is unprovisioned, which is the cheap way to catch a mirror that was added but
-never given credentials. It is run by hand rather than by the sync, because
-writing a secret from CI would mean widening `RELEASED_SYNC_PAT` with Secrets
-permission and another organization-owner approval.
-
-The token lives at `~/.config/hex/lake-cache-key`, mode 600, and is read from
-there or from `$HEX_LAKE_CACHE_KEY`. R2 shows a secret key once, so a lost file
-is not recoverable and means minting a new token; run the script with no token
-and it prints that procedure in full, including how to verify the new token
-before provisioning 57 repositories with it. A bucket may hold several tokens,
-so the old one need not be revoked first.
-
-If a mirror ever stops publishing, look for `upload not configured` in its CI
-log: that is the step reporting a missing secret or variable rather than
-failing, so an unprovisioned repository is quiet rather than red.
-
-Changing the publish step means changing `released-ci.yml`, which the sync can
-only deliver while the publishing tokens carry the Workflows permission (see
-"Publishing a new library: widen a token first"). A sync whose workflow text is
-unchanged pushes no workflow file and so never exercises that permission, which
-is worth remembering when diagnosing the first sync after a workflow change.
+The names are Hex-specific because a bare `LAKE_CACHE_KEY` would collide with
+any other Lean project in the organization.
+`scripts/release/provision_cache_secrets.sh` sets all five on every repository in
+`released-ci.yml`, plus hex-dev; it is idempotent, and `--check` takes no token
+and reports what is unprovisioned. The token lives at
+`~/.config/hex/lake-cache-key`, mode 600. R2 shows a secret key once, so a lost
+file means minting a replacement: run the script with no token and it prints
+that procedure, including how to verify the new token first.
+
+#### Why the mirrors stopped publishing
+
+Publishing worked. All 56 mirrors uploaded, the objects were publicly readable,
+and a consumer fetched every map and all 1128 artifacts they referenced. The
+problem was on the consuming side, and it was quantitative rather than a
+failure. Against a downloads-only cache with every Hex build directory wiped:
+
+| package | modules recompiled | time |
+| --- | ---: | ---: |
+| HexMatrix | 0 | 2s |
+| HexModArith | 2 of 96 | 43s |
+| HexGF2 | 10 | 171s |
+| HexGraphIso | 64 of 91 | 367s |
+
+Restoration is real, but the modules that fail to restore are consistently the
+expensive ones, so the wall clock barely moves while the fetch adds two to three
+minutes. End to end in the blog's CI, measured twice with identical results: 41
+minutes with the cache against about 31 without.
+
+What distinguishes the modules that never restore is still unknown. It is not
+`native_decide` (one module in the whole graph uses it), not a Mathlib revision
+difference (identical), not the upstream pins, and not `precompileModules`. Nor
+is it a root-versus-dependency effect: a minimal two-package reproducer, one
+published as root and consumed as a dependency, restores perfectly, with and
+without `precompileModules`, so cross-workspace reuse is supported.
+
+Anyone picking this up again should start by identifying what those expensive
+modules have in common, not by re-checking the transport, which is sound.
 
 ### Publishing a new library: widen a token first