File size: 1,879 Bytes
ab54eb4 e6aa1c8 ab54eb4 | 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 | # Container image for the AProver chat demo.
#
# Designed for Hugging Face Spaces (sdk: docker, app_port: 7860). Installs
# CBMC + uv + the project, then launches uvicorn against web.server:app.
#
# Required runtime secrets (set in the Space settings):
# ANTHROPIC_API_KEY — Claude key for both chat agent and AProver pipeline
# Optional:
# BMC_AGENT_LLM_MODEL — defaults to claude-sonnet-4-6
FROM python:3.12-slim
ENV PYTHONUNBUFFERED=1 \
PYTHONDONTWRITEBYTECODE=1 \
PIP_DISABLE_PIP_VERSION_CHECK=1 \
UV_SYSTEM_PYTHON=1 \
HOME=/home/user \
BMC_AGENT_LOG_DIR=/tmp/aprover-logs
# CBMC + a C compiler (needed by the parser preprocessor and any future
# dynamic-validator path). gcc is pulled in by build-essential.
RUN apt-get update \
&& apt-get install -y --no-install-recommends \
cbmc \
build-essential \
ca-certificates \
git \
&& rm -rf /var/lib/apt/lists/*
# uv for fast, reproducible installs of the project deps.
RUN pip install --no-cache-dir uv
# HF Spaces runs containers as a non-root user (uid 1000). Match that so
# the workdir + temp dirs stay writable.
RUN useradd -m -u 1000 user
WORKDIR /home/user/app
# Install Python deps first for better layer caching.
COPY --chown=user:user pyproject.toml uv.lock* /home/user/app/
RUN uv pip install --system \
"fastapi>=0.110" \
"uvicorn[standard]>=0.27" \
"anthropic>=0.40.0" \
"tree-sitter>=0.21.0" \
"tree-sitter-c>=0.21.0" \
"rich>=13.0.0" \
"pydantic>=2.0.0"
# Project source.
COPY --chown=user:user bmc_agent /home/user/app/bmc_agent
COPY --chown=user:user aprover /home/user/app/aprover
COPY --chown=user:user assets /home/user/app/assets
COPY --chown=user:user web /home/user/app/web
USER user
EXPOSE 7860
CMD ["uvicorn", "web.server:app", "--host", "0.0.0.0", "--port", "7860"]
|