Lean / Lake build cache

Overview

Lean’s build tool, Lake, can fetch prebuilt .olean/.ilean artifacts from a remote cache instead of recompiling them. That matters most for mathlib, where artifacts are tied to the exact toolchain: a cache mixed across toolchain versions is how a build ends up failing with “object file does not exist”.

NORA has no Lean format, and does not need one to serve the cache for reading. Lake downloads with plain GETs by path, which is exactly what the raw registry does.

What Lake expects from a cache service, and what NORA covers:

Operation	What Lake does	NORA raw
Fetch a revision’s mappings	GET {revisionEndpoint}/{scope}/{git-rev}.jsonl	works
Fetch an artifact	GET {artifactEndpoint}/{scope}/{hash}.art	works
Upload	PUT signed with AWS SigV4	works from NORA 1.3.3 when authentication is off — see limits

Verified against Lean 4.34.1 and Lake 5.0.0; the upload path on NORA 1.3.3.

Configure the cache service

Lake takes the cache service from a configuration file. Point both endpoints at one prefix in your raw repository — Lake keeps revision mappings and artifacts apart, so two sub-prefixes under it are enough:

# services.toml, selected with LAKE_CONFIG=/path/to/services.toml
[[cache.service]]
name = "nora"
type = "s3"
artifactEndpoint = "https://nora.example.com/raw/lean/a0"
revisionEndpoint = "https://nora.example.com/raw/lean/r0"

The older LAKE_CACHE_ARTIFACT_ENDPOINT / LAKE_CACHE_REVISION_ENDPOINT environment variables still work, and must be set together, but Lake now warns that they are deprecated in favour of a configured service.

The package has to opt in, or a build will record mappings for artifacts it never cached:

lakefile.toml

name = "mypkg"
enableArtifactCache = true

The key has to sit at package level, as above. TOML attaches a bare key to the table that precedes it, so the same line appended at the end of the file lands inside the last [[lean_exe]] and Lake warns that the artifact cache is not enabled for the package — while still writing the mappings.

Restore a build from NORA

# fetch the mappings and the artifacts they name
lake cache get --scope=mypkg --service=nora

# replay the build from the cache; nothing should compile
lake build MyPkg --no-build

A successful restore prints the local path and the remote URL for each object, and the build then reports targets as Unpacked rather than Built.

Fill the cache

Lake signs uploads with AWS SigV4, which NORA does not validate, so on a NORA with authentication enabled lake cache put is refused (see limits). There, publish the objects to NORA yourself and let Lake read them. Produce the mappings during a build, then upload both the mappings and the artifacts they name:

# set the cache location explicitly, so a CI job and this script agree on it
export LAKE_CACHE_DIR=$PWD/.lake-cache

# build and record the input-to-output mappings
lake build MyPkg -o outputs.jsonl

REV=$(git rev-parse HEAD)
SCOPE=mypkg
BASE=https://nora.example.com/raw/lean

# the mappings file, named after the revision it describes
curl -fsS -H "Authorization: Bearer $NORA_TOKEN" \
  -X PUT --data-binary @outputs.jsonl \
  "$BASE/r0/$SCOPE/$REV.jsonl"

# every artifact the mappings name: `<hash>.ltar` in the cache, `<hash>.art` on NORA
awk -F'"' 'NR>1 {print $4}' outputs.jsonl | while read -r art; do
  curl -fsS -H "Authorization: Bearer $NORA_TOKEN" \
    -X PUT --data-binary @"$LAKE_CACHE_DIR/artifacts/$art" \
    "$BASE/a0/$SCOPE/${art%.ltar}.art"
done

The mappings file is JSON Lines: a schema version on the first line, then one ["<input-hash>", "<artifact-hash>.ltar"] pair per artifact. The scope is yours to choose — Lake prefixes everything with it and uses it verbatim, so one raw prefix can hold several projects, toolchains or platforms side by side.

This is also the shape that suits an air-gapped contour: seed the objects once from a connected machine, mirror the prefix, and every builder behind the air gap reads from NORA.

Limits

• lake cache put needs NORA 1.3.3 or newer. Up to 1.3.2 raw answered 201 Created where the client requires 200 — Lake aborts with error: failed to upload artifact, error 201 although the object is already stored — and 409 on the retry Lake makes after a partial transfer. Both are fixed (#1039, #1036). On an older NORA, publish with curl as above.
• Lake authenticates uploads only with SigV4, which NORA does not validate, and NORA checks every request that carries credentials. So lake cache put succeeds only on a NORA with authentication disabled, or through a proxy in front that replaces Lake’s Authorization header with a NORA token. With authentication enabled every put gets 401, anonymous read or not. Reads are separate — see the next point.
• Lake sends no credentials when downloading, so with authentication enabled the cache needs anonymous read (NORA_AUTH_ANONYMOUS_READ=true) or a proxy in front that injects a token for the prefix. With anonymous read on, downloads succeed and writes still require a token — an unauthenticated PUT is 401. With it off, Lake stops at failed to GET URL, error 401 and reports output lookup failed.
• Artifact hashes are not cryptographic. Lake says so itself, which is why it prefixes uploads with a scope — keep scopes distinct per project, and treat a shared scope as a shared trust boundary.