Forked from soil-moisture-image, then restructured so the heavy Mathlib/TorchLean
tree is NO LONGER baked into the image (it was "too large"). Instead a shared Lean
package store is populated once, at container time, into the persistent home dir --
EBS-backed on hub.maap-project.org, host-mounted locally by run-image.sh -- so the
one-time sync survives container restarts and the image stays small (elan + a
C/CUDA toolchain + tooling on a pangeo PyTorch base).

Mechanism:
  * scripts/lean-store-sync.sh -- reads ~/.lean-store/repos.txt (a manifest of git
    repos), clones + builds each into ~/.lean-store, pulls Mathlib oleans via
    `lake exe cache get`, applies the glibc-2.38 CUDA link shim for the 'cuda'
    flavor, and writes ~/.lean-store/package-overrides.json.
  * scripts/gen-package-overrides.py -- now MERGES multiple store projects into one
    Lake override (first-wins by name, collision-warned).
  * scripts/smi-env.sh -- LEAN_PACKAGES + lean-build/lean-clean/lean-wire, sourced
    system-wide (/etc/zsh/zshenv + /etc/profile.d) so it survives the home-volume
    shadow on the hub. Shipped under /opt/smi (outside $HOME).
  * Dockerfile -- drops the /opt/lean clone/cache/build layers; keeps elan, the
    CUDA toolkit (for runtime GPU builds), and zsh; ships /opt/smi + wires smi-env.
  * run-image.sh -- mounts a persistent host store at ~/.lean-store, adds
    --store/--sync, handles an unsynced store, repoints all /opt/lean paths.
  * verify-dedup.sh -- inspects a synced store dir instead of a baked image.

On Lake's native cache: v4.31.0 ships `lake cache get` / `--try-cache`
(Reservoir-backed) but it does not yet serve Mathlib, so the store uses Mathlib's
own `lake exe cache get`; the swap point is marked in lean-store-sync.sh for when a
cache service (Reservoir or a MAAP-hosted S3 scope) covers our packages.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>