#!/bin/sh
# Mathew — lean server entrypoint.
#
# In the usual image this does nothing: the built Mathlib already sits under
# the project and the server starts straight away.
#
# With the image built as `--build-arg BAKE_MATHLIB=false` (see README's
# "Keeping Mathlib out of the image"), the project's .lake is meant to be a
# volume: a fresh one gets filled once, at first start, so Mathlib's ~7GB of
# compiled cache never travels through the registry.
#
# The manifest pairing matters: `lake update` advances the packages in .lake
# AND rewrites lake-manifest.json — but the manifest sits in the (ephemeral)
# image while the packages sit in the (permanent) volume. Without help, a new
# container would find manifest ≠ volume and try to re-sync Mathlib from
# GitHub at every session. So the first start saves the manifest it resolved
# into the volume, and every later start puts that saved copy over the
# image's — manifest and packages always tell the same story.
set -eu

PROJECT=/opt/lean4web/Projects/MathlibDemo
MANIFEST="$PROJECT/lake-manifest.json"
SAVED_MANIFEST="$PROJECT/.lake/mathew-lake-manifest.json"

if [ -f "$SAVED_MANIFEST" ]; then
  cp "$SAVED_MANIFEST" "$MANIFEST"
fi

if [ ! -f "$PROJECT/.lake/build/lib/lean/MathlibDemo.olean" ]; then
  echo "[mathew-lean] $PROJECT/.lake holds no built Mathlib — fetching it once (expect ~10 minutes)"
  # lake update pulls the sources pinned in lake-manifest.json, and Mathlib's
  # post-update hook fetches the matching precompiled cache; lake build then
  # only writes the project's own module. The image's pinned toolchain
  # (elan) stays as it is — no lean-toolchain re-curl, no surprise downloads.
  # (subshell: its cd must not leak into the server's working directory)
  ( cd "$PROJECT" && lake update -R && lake build )
  cp "$MANIFEST" "$SAVED_MANIFEST"
  echo "[mathew-lean] Mathlib ready"
fi

exec "$@"