claude-bot
3e0782c62a
Mathlib's post-update hook fetched the cache inside 'lake update', where a few dropped transfers failed the build before the retries could run. Disable the hook, retry up to six times, and keep the archives in a BuildKit cache mount so a retried image build resumes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01FYqwNMyPUHeTbFWg83GQq6
103 lines
4.7 KiB
Docker
103 lines
4.7 KiB
Docker
# 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"]
|