RFC: Configurable / default `lake cache` scopes

Proposal

A custom S3 cache service can only be used by passing --scope/--repo on every cache get. This RFC proposes a per-service Boolean config field, scoped. A service with scoped = false uses no scope: lake cache get --service <name> then works without a scope flag.

Background

Scope is the path prefix under which a service stores artifacts ({endpoint}/{scope}/{hash}.art) and mappings ({endpoint}/{scope}/{rev}.jsonl). The scope kind also selects the revision layout. A repository scope (--repo) inserts platform and toolchain segments into the revision path: …/{scope}/pt/{platform}/tc/{toolchain}/{rev}.jsonl (Cache.lean:1004-1016). These segments are empty when the package sets platformIndependent := true and fixedToolchain := true (Main.lean:455-459). A string scope (--scope) is a pure prefix.

Today the scope comes only from the CLI for S3 services, or is derived from package fields for Reservoir (reservoirScope). A flat content-addressed bucket has no meaningful scope, yet the CLI still demands one. The flat layout is in fact not expressible today: an empty --scope argument is accepted but produces a double slash in the URL (Main.lean:299; compare --toolchain, which maps an empty argument to "none", Main.lean:311).

Current state

For a custom (non-Reservoir) service, cache get requires --scope or --repo; with neither it errors (Main.lean:565-566). The service config carries endpoints and kind, but no scope (LakeConfig.lean:30-42).

The change

Add scoped to CacheServiceConfig, default true:

• scoped = true: the current behavior. cache get and cache put require --scope or --repo.
• scoped = false: the service uses no scope. Artifacts live at {endpoint}/{hash}.art and mappings at {endpoint}/{rev}.jsonl, for get and put alike. A fixed prefix, if wanted, is written into the endpoint URLs.

Three rules keep this safe:

• A --scope/--repo flag directed at a scoped = false service is an error. The flag is not ignored, and it is never appended after a prefix inside the endpoint.
• An empty argument to --scope or --repo becomes an error. Today it is accepted and produces a malformed URL.
• scoped on a Reservoir service is a configuration error: Reservoir derives its scope per package and has no flat form.

Configuration sketch

[[cache.service]]
name = "forks"
kind = "s3"
artifactEndpoint = "https://cache.example.org/forks/artifacts"
revisionEndpoint = "https://cache.example.org/forks/revisions"
scoped = false    # flat: no prefix, no scope flag

[[cache.service]]
name = "master"
kind = "s3"
artifactEndpoint = "https://cache.example.org/artifacts/leanprover-community/mathlib4"
revisionEndpoint = "https://cache.example.org/revisions/leanprover-community/mathlib4"
scoped = false    # fixed prefix, written into the endpoints

lake cache get --service forks then needs no scope flag.

Security

Scope is the operator describing where to read, which is already their responsibility; reads remain verified by hash

Limitation and future work

scoped = false always produces plain paths. A service with the platform/toolchain revision layout therefore still needs --repo on every call: Lake computes those segments per call, so they cannot be written into an endpoint URL. This matters only for packages outside the platformIndependent/fixedToolchain regime, and no current consumer needs it. When one does, the extension is per-service value fields (scope = "prefix", repo = "owner/name") that join scoped = false as mutually exclusive alternatives, with at most one of the three set, and a package-to-scope derivation for custom services.

Backwards compatibility

Flows that pass --scope/--repo are unaffected, and scoped defaults to true, which is changes are visible: an empty --scope/--repo argument becomes an error instead of amalformed URL, and a scope flag directed at a scoped = false service is an error.

User Experience

A service declares once, in config, that it takes no scope; lake cache get --service <name> works with no scope flag. Fixed prefixes live in the endpoint URLs.

Beneficiaries

Anyone running an S3-backed Lake cache who would rather configure the layout once than pass --scope on every call. Flat content-addressed buckets that have no scope to pass. Chain members in the companion read
chain RFC (#14152), which need services that resolve without flags.

Maintainability

Small: one Boolean config field, one CLI check relaxed, two error checks added.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, pleaseask them to add 👍 to it.

Start with Lake/Config/LakeConfig.lean for CacheServiceConfig, then read the scope handling and validation in Lake/CLI/Main.lean and the layout logic in Lake/Config/Cache.lean. Done means the proposed scoped configuration, flag validation, empty-argument errors, and Reservoir restriction are implemented while preserving the default behavior.