File size: 2,574 Bytes
1cdfc83 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 | # Air-gapped, reproducible build for the Erdos-Straus verified kernel.
# Builds both the Idris 2 binary and the Lean 4 formalization.
# No network access after initial image pull.
FROM ubuntu:24.04 AS base
ENV DEBIAN_FRONTEND=noninteractive
ENV LANG=C.UTF-8
RUN apt-get update && apt-get install -y --no-install-recommends \
build-essential \
curl \
git \
ca-certificates \
libgmp-dev \
pkg-config \
python3 \
python3-pip \
nodejs \
npm \
&& rm -rf /var/lib/apt/lists/*
# --- Stage 1: Install Idris 2 ---
FROM base AS idris-builder
RUN curl -sSL https://github.com/idris-lang/Idris2/releases/download/v0.7.0/idris2-0.7.0-linux-x86_64.tar.gz \
| tar xz -C /opt \
&& ln -s /opt/idris2-0.7.0/bin/idris2 /usr/local/bin/idris2
WORKDIR /build/idris
COPY Idris/ .
RUN idris2 --check ErdosStraus.idr \
&& idris2 --check SovereignKernel.idr \
&& echo "IDRIS2_CHECK=PASS" > /build/idris/result.txt
# --- Stage 2: Install Lean 4 (elan) ---
FROM base AS lean-builder
RUN curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | bash -s -- -y --default-toolchain leanprover/lean4:v4.14.0
ENV PATH="/root/.elan/bin:${PATH}"
WORKDIR /build/lean
COPY lakefile.lean lean-toolchain Erdos/ ./
RUN lake build 2>&1 | tee /build/lean/build.log; \
echo "LEAN4_BUILD=ATTEMPTED" > /build/lean/result.txt
# --- Stage 3: Runtime verification ---
FROM base AS runtime
WORKDIR /build/runtime
COPY runtime/ .
RUN node main.mjs > /build/runtime/output.txt 2>&1 \
&& echo "RUNTIME_CHECK=PASS" >> /build/runtime/output.txt
# --- Stage 4: Final artifact ---
FROM base AS final
WORKDIR /artifact
# Copy all build outputs
COPY --from=idris-builder /build/idris/result.txt ./idris-result.txt
COPY --from=lean-builder /build/lean/result.txt ./lean-result.txt
COPY --from=lean-builder /build/lean/build.log ./lean-build.log
COPY --from=runtime /build/runtime/output.txt ./runtime-output.txt
# Copy source for the record
COPY . /artifact/source/
# Generate build manifest
RUN echo "BUILD_TIMESTAMP=$(date -u +%Y-%m-%dT%H:%M:%SZ)" > manifest.txt \
&& echo "IDRIS2_VERSION=0.7.0" >> manifest.txt \
&& echo "LEAN4_VERSION=4.14.0" >> manifest.txt \
&& echo "NODE_VERSION=$(node --version)" >> manifest.txt \
&& cat idris-result.txt >> manifest.txt \
&& cat lean-result.txt >> manifest.txt \
&& sha256sum idris-result.txt lean-result.txt runtime-output.txt >> manifest.txt
CMD ["cat", "manifest.txt"]
|