FROM debian:bookworm-slim

WORKDIR /app

RUN apt-get update && apt-get install -y --no-install-recommends \
    bash ca-certificates clang curl git libgmp-dev nodejs npm \
    && rm -rf /var/lib/apt/lists/*

RUN npm install -g tsx typescript

RUN curl -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal \
    && /root/.cargo/bin/rustup default stable \
    && /root/.cargo/bin/cargo --version

RUN curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
    | sh -s -- -y --default-toolchain none

COPY --from=ghcr.io/astral-sh/uv:latest /uv /uvx /bin/

ENV PATH="/root/.cargo/bin:/root/.elan/bin:$PATH" \
    LEAN_BIN=/root/.elan/bin/lean \
    LEAN_CWD=/app/env/lean \
    LEAN_PATH=/app/env/lean/.lake/build/lib \
    PYTHONPATH=/app/env \
    UV_LINK_MODE=copy \
    UV_COMPILE_BYTECODE=1

COPY lean/lean-toolchain /app/env/lean/lean-toolchain

RUN elan default "$(cat /app/env/lean/lean-toolchain)" \
    && lean --version

COPY . /app/env

WORKDIR /app/env/lean

RUN lake build AuthSpec PricingSpec SagaSpec

WORKDIR /app/env
RUN uv sync --locked

ENV PATH="/app/env/.venv/bin:/root/.cargo/bin:/root/.elan/bin:$PATH" \
    VIRTUAL_ENV=/app/env/.venv

EXPOSE 8000

HEALTHCHECK --interval=30s --timeout=3s --start-period=5s --retries=3 \
    CMD curl -f http://localhost:8000/health || exit 1

ENV ENABLE_WEB_INTERFACE=true
CMD ["sh", "-c", "cd /app/env && uv run uvicorn lean_migrate.server.app:app --host 0.0.0.0 --port 8000"]