# 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"]