# lean-bench: Lean 4 + Mathlib + the ingestion pipeline, in one image.
#
# Build from the repository root:
#   docker build -f docker/Dockerfile -t lean-bench:latest .
#
# The Mathlib revision and the Lean toolchain are resolved against each other at
# build time (see docker/resolve-mathlib.sh); override with --build-arg MATHLIB_REV=v4.33.0.
FROM ubuntu:24.04

LABEL org.opencontainers.image.title="lean-bench" \
      org.opencontainers.image.description="Detect formalizable mathematics in books and turn it into verified, indexed Lean 4" \
      org.opencontainers.image.source="https://gitea.entroia.com/Zayden-Jung/lean-bench"

ENV DEBIAN_FRONTEND=noninteractive \
    ELAN_HOME=/opt/elan \
    PATH=/opt/elan/bin:$PATH \
    PYTHONUNBUFFERED=1

RUN apt-get update && apt-get install -y --no-install-recommends \
        build-essential ca-certificates curl git jq sqlite3 \
        libgmp-dev python3 python3-pip \
    && rm -rf /var/lib/apt/lists/*

# -- elan (the Lean toolchain manager) --------------------------------------
RUN curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o /tmp/elan-init.sh \
    && sh /tmp/elan-init.sh -y --no-modify-path --default-toolchain none \
    && rm /tmp/elan-init.sh \
    && elan --version

WORKDIR /opt/lean-bench

# -- Lean project: toolchain, Mathlib, and its prebuilt cache ---------------
# One layer per step on purpose. The cache fetch is the expensive one (gigabytes),
# so it gets a layer of its own: a failure in any later step re-runs that step, never
# the download. Every long step is wrapped in `timeout` so a stall fails loudly with
# a diagnosable message instead of hanging until the CI job's own limit.
ARG MATHLIB_REV=auto
COPY lean/ lean/
COPY docker/resolve-mathlib.sh docker/resolve-mathlib.sh
RUN chmod +x docker/resolve-mathlib.sh && docker/resolve-mathlib.sh lean "$MATHLIB_REV"

RUN elan toolchain install "$(cat lean/lean-toolchain)" \
    && elan default "$(cat lean/lean-toolchain)"

# Resolve dependencies: clones Mathlib and writes the manifest.
# Mathlib's post-update hook would fetch the cache here, outside the retry loop below.
RUN cd lean && MATHLIB_NO_CACHE_ON_UPDATE=1 timeout 1800 lake update

# Mathlib's prebuilt artifacts. Slow, large, and cached as its own layer.
# A handful of the ~9,000 transfers failing is normal; a re-run fetches only what is missing.
# The downloaded archives live in a BuildKit cache mount on the build host, so a
# retried build resumes instead of starting over; only the unpacked oleans enter the image.
RUN --mount=type=cache,target=/root/.cache/mathlib \
    cd lean && for attempt in 1 2 3 4 5 6; do \
      timeout 5400 lake exe cache get && break; \
      [ "$attempt" -eq 6 ] && exit 1; \
      echo "cache get attempt $attempt failed; retrying" >&2; sleep $((attempt * 15)); \
    done

# The honest check that this image can do its job, and it is exactly what
# verification does at runtime: elaborate a file against Mathlib with `lake env lean`.
# There is deliberately no `lake build` here -- compiling our own library is something
# nothing in the pipeline ever uses.
#
# Loading Mathlib's environment needs several GB of RAM. On a host that does not have
# it, this does not fail: it thrashes, and the only symptom is silence. So it runs
# under `timeout`, and exit 124 is reported for what it almost always is.
RUN cd lean && timeout 1200 lake env lean LeanBench.lean; status=$?; \
    if [ "$status" -eq 124 ]; then \
      echo "ERROR: elaborating 'import Mathlib' timed out after 20 minutes." >&2; \
      echo "Every olean it needs is already on local disk, so this is not the network." >&2; \
      echo "Loading Mathlib wants ~4-8 GB of RAM. This machine has:" >&2; \
      { free -h || head -3 /proc/meminfo; } >&2 2>/dev/null; \
      echo "Give the build host more memory, or build this image elsewhere." >&2; \
    fi; \
    [ "$status" -eq 0 ] || exit "$status"; \
    lake env lean --version

# -- the pipeline -----------------------------------------------------------
COPY pyproject.toml README.md ./
COPY leanbench/ leanbench/
RUN pip install --break-system-packages --no-cache-dir . \
    && lean-bench --help > /dev/null

COPY docker/entrypoint.sh /usr/local/bin/leanbench-entrypoint
RUN chmod +x /usr/local/bin/leanbench-entrypoint

ENV LEANBENCH_LEAN_PROJECT=/opt/lean-bench/lean \
    LEANBENCH_LEAN_COMMAND='["lake","env","lean"]' \
    LEANBENCH_DATABASE=/data/leanbench.sqlite \
    LEANBENCH_LLM_MODEL=qwen-max \
    LEANBENCH_LLM_BASE_URL=https://dashscope.aliyuncs.com/compatible-mode/v1 \
    LEANBENCH_LLM_API_KEY_ENV=DASHSCOPE_API_KEY

# /books is where you put the source you are submitting; /data holds the database.
VOLUME ["/data", "/books"]
WORKDIR /work

RUN mkdir -p /work

ENTRYPOINT ["leanbench-entrypoint"]
CMD ["doctor"]