ship: SZLHOLDINGS/lean-kernel — live Lean v4.13.0 + Mathlib kernel, 7 API endpoints, honest build status

Dockerfile

@@ -26,11 +26,13 @@ RUN git clone --depth 1 https://github.com/szl-holdings/lutar-lean.git ${LUTAR_R
     && cat lean-toolchain \
     && lake --version
 
-# --- resolve deps + warm Mathlib cache (best-effort; build still works without) ---
-# `lake update -R` generates lake-manifest.json; `lake exe cache get` pulls
-# prebuilt Mathlib oleans so the on-demand `lake build` is fast & green.
+# --- warm Mathlib cache (best-effort; build still works without) ---
+# The repo ships a pinned lake-manifest.json, so we DO NOT run `lake update`
+# (which could move deps off the pinned revs). `lake exe cache get` pulls the
+# prebuilt Mathlib oleans for the pinned revs so the on-demand `lake build` is
+# fast. If the cache is unavailable the kernel still serves; the build endpoint
+# reports the honest failure rather than faking green.
 RUN cd ${LUTAR_REPO} \
-    && lake update -R \
     && (lake exe cache get || echo "WARN: mathlib cache fetch incomplete; build will compile from source on demand")
 
 # --- python service deps ---

README.md

@@ -34,4 +34,4 @@ This Space pins **Lean v4.13.0 + Mathlib v4.13.0** (from the repo's `lean-toolch
 
 Numbers are **never hardcoded** — every figure is recomputed live from the deployed commit. If `lake build` fails (e.g. Mathlib cache or disk is unavailable on the box), `healthz` and the UI report **BUILD FAIL** with the verbatim error tail. Nothing is faked green.
 
-Doctrine v10. Author: Stephen P. Lutar Jr. (ORCID 0009-0001-0110-4173), SZL Holdings.
+Doctrine v10/v11. Author: Stephen P. Lutar Jr. (ORCID 0009-0001-0110-4173), SZL Holdings.