# KeYmaera X API Server - Z3 Only
# Provides a REST API for agents to submit models and proofs to KeYmaera X

FROM eclipse-temurin:17-jdk-jammy

# Install Python, Z3, and dependencies
# Z3 must be installed from system packages because the bundled Z3 in KeYmaera X
# is architecture-specific (x86_64) and won't work on ARM
RUN apt-get update && apt-get install -y --no-install-recommends \
    python3 \
    python3-pip \
    python3-venv \
    curl \
    z3 \
    && rm -rf /var/lib/apt/lists/*

# Make system Z3 available to KeYmaera X
# KeYmaera X looks for z3 in ~/.keymaerax/ and reads Z3_PATH from config
RUN mkdir -p /root/.keymaerax && \
    ln -s /usr/bin/z3 /root/.keymaerax/z3 && \
    echo 'Z3_PATH = /root/.keymaerax' > /root/.keymaerax/keymaerax.conf && \
    echo 'QE_TOOL = z3' >> /root/.keymaerax/keymaerax.conf && \
    echo 'USE_DEFAULT_USER = true' >> /root/.keymaerax/keymaerax.conf && \
    echo 'DEFAULT_USER = local' >> /root/.keymaerax/keymaerax.conf

# Set up Python virtual environment
RUN python3 -m venv /opt/venv
ENV PATH="/opt/venv/bin:$PATH"

# Install Python packages
RUN pip install --no-cache-dir \
    flask==3.0.0 \
    gunicorn==21.2.0

# Create app directory
WORKDIR /app

# Download KeYmaera X
ARG KEYMAERAX_VERSION=5.1.2
RUN curl -L -o /app/keymaerax.jar \
    "https://github.com/LS-Lab/KeYmaeraX-release/releases/download/${KEYMAERAX_VERSION}/keymaerax.jar"

# Pre-warm KeYmaera X to derive lemmas at build time (takes ~3-5 minutes)
# This avoids the slow first-run penalty at container startup
RUN echo 'ArchiveEntry "Warmup"\nProgramVariables Real x; End.\nProblem x>=0 -> x>=0 End.\nTactic "T" id End.\nEnd.' > /tmp/warmup.kyx && \
    timeout 600 java -Xss20M -jar /app/keymaerax.jar -launch -prove /tmp/warmup.kyx -tool z3 || true && \
    rm /tmp/warmup.kyx

# Copy application code
COPY server.py /app/
COPY entrypoint.sh /app/

RUN chmod +x /app/entrypoint.sh

# Create directories for work files
RUN mkdir -p /app/workdir /app/proofs

# Expose API port
EXPOSE 8080

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

ENTRYPOINT ["/app/entrypoint.sh"]
