Кэш сборки Lean / Lake

Обзор

Сборщик Lean, Lake, умеет забирать готовые .olean/.ilean артефакты из удалённого кэша вместо повторной компиляции. Больше всего это нужно для mathlib, где артефакты привязаны к конкретному тулчейну: кэш, в котором смешались версии тулчейна, — это тот самый случай, когда сборка падает с “object file does not exist”.

У NORA нет формата Lean, и для чтения кэша он не нужен. Lake скачивает обычными GET по пути — ровно то, что делает raw-реестр.

Что Lake ждёт от кэш-сервиса и что из этого закрывает NORA:

Операция	Что делает Lake	NORA raw
Маппинги ревизии	`GET {revisionEndpoint}/{scope}/{git-rev}.jsonl`	работает
Артефакт	`GET {artifactEndpoint}/{scope}/{hash}.art`	работает
Загрузка	`PUT`, подписанный AWS SigV4	работает с NORA 1.3.3 при выключенной аутентификации — см. ограничения

Проверено на Lean 4.34.1 и Lake 5.0.0; путь загрузки — на NORA 1.3.3.

Настройка кэш-сервиса

Lake берёт кэш-сервис из файла конфигурации. Направьте оба эндпоинта на один префикс в raw-репозитории — Lake держит маппинги ревизий и артефакты раздельно, поэтому достаточно двух подпрефиксов:

# services.toml, выбирается через 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"

Старые переменные окружения LAKE_CACHE_ARTIFACT_ENDPOINT и LAKE_CACHE_REVISION_ENDPOINT ещё работают и должны быть заданы вместе, но Lake предупреждает, что они устарели в пользу настроенного сервиса.

Пакет должен включить кэш явно, иначе сборка запишет маппинги на артефакты, которых в кэше нет:

name = "mypkg"
enableArtifactCache = true

Ключ обязан стоять на уровне пакета, как выше. TOML привязывает одиночный ключ к предшествующей таблице, поэтому та же строка, дописанная в конец файла, попадёт внутрь последнего [[lean_exe]]: Lake предупредит, что кэш артефактов для пакета не включён, а маппинги всё равно запишет.

Восстановить сборку из NORA

# забрать маппинги и артефакты, которые в них перечислены
lake cache get --scope=mypkg --service=nora

# переиграть сборку из кэша: компилироваться ничего не должно
lake build MyPkg --no-build

При успешном восстановлении Lake печатает для каждого объекта локальный путь и удалённый URL, а сборка затем сообщает про цели Unpacked, а не Built.

Наполнить кэш

Lake подписывает загрузки по AWS SigV4, которого NORA не проверяет, поэтому на NORA с включённой аутентификацией lake cache put получает отказ (см. ограничения). В таком случае публикуйте объекты в NORA самостоятельно и дайте Lake их читать. Маппинги получаются при сборке; дальше выкладываются и они, и перечисленные в них артефакты:

# задать расположение кэша явно, чтобы CI-джоба и этот скрипт сходились
export LAKE_CACHE_DIR=$PWD/.lake-cache

# собрать и записать маппинги вход -> выход
lake build MyPkg -o outputs.jsonl

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

# файл маппингов, названный по ревизии, которую он описывает
curl -fsS -H "Authorization: Bearer $NORA_TOKEN" \
  -X PUT --data-binary @outputs.jsonl \
  "$BASE/r0/$SCOPE/$REV.jsonl"

# каждый артефакт из маппингов: `<hash>.ltar` в кэше, `<hash>.art` в 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

Файл маппингов — это JSON Lines: в первой строке версия схемы, далее по паре ["<hash-входа>", "<hash-артефакта>.ltar"] на артефакт. scope выбираете вы: Lake подставляет его как есть, поэтому один raw-префикс может держать рядом несколько проектов, тулчейнов или платформ.

Эта же схема удобна для закрытого контура: один раз засеять объекты с машины, у которой есть доступ в сеть, отзеркалить префикс — и все сборщики за воздушным зазором читают из NORA.

Ограничения

lake cache put требует NORA 1.3.3 или новее. До 1.3.2 raw отвечал 201 Created там, где клиент требует 200 — Lake прерывается на error: failed to upload artifact, error 201, хотя объект уже сохранён, — и 409 на повторную загрузку, которую Lake делает после частичного сбоя. И то, и другое исправлено (#1039, #1036). На более старой NORA публикуйте через curl, как выше.
Запись Lake подписывает только SigV4, которого NORA не проверяет, а запрос с учётными данными NORA проверяет всегда. Поэтому lake cache put проходит только на NORA с выключенной аутентификацией либо через прокси перед реестром, который заменяет заголовок Authorization от Lake на токен NORA. С включённой аутентификацией каждый put получает 401, с анонимным чтением или без. Чтение — отдельная история, см. следующий пункт.
На скачивании Lake не посылает никаких учётных данных, поэтому при включённой аутентификации кэшу нужен анонимный доступ на чтение (NORA_AUTH_ANONYMOUS_READ=true) либо прокси, который подставляет токен для этого префикса. С анонимным чтением скачивание проходит, а запись по-прежнему требует токена — неаутентифицированный PUT даёт 401. Без него Lake останавливается на failed to GET URL, error 401 и сообщает output lookup failed.
Хеши артефактов не криптографические. Lake говорит об этом сам — именно поэтому он префиксует загрузки областью (scope). Держите области раздельно по проектам и считайте общую область общей границей доверия.