# Lean 4 v4.34.1, which checks proofs/SB3.lean. The proof uses Lean's core library only (no
# Mathlib), so checking needs no network: `lean proofs/SB3.lean` from the bundle's root.
FROM debian:bookworm-slim
RUN apt-get update \
 && apt-get install -y --no-install-recommends ca-certificates curl \
 && rm -rf /var/lib/apt/lists/*
ENV ELAN_HOME=/opt/elan
RUN curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
      | sh -s -- -y --no-modify-path --default-toolchain leanprover/lean4:v4.34.1 \
 && chmod -R a+rX /opt/elan
# The toolchain's own binaries come first, so checking runs Lean directly, not elan's proxy.
ENV PATH=/opt/elan/toolchains/leanprover--lean4---v4.34.1/bin:/opt/elan/bin:$PATH
RUN lean --version