Dockerfile

# 使用轻量级 Debian 基础镜像
FROM debian:bookworm-slim

# 安装系统依赖
RUN apt-get update && apt-get install -y \
    ca-certificates curl git zstd \
    python3 python3-venv \
    && rm -rf /var/lib/apt/lists/*

# 安装 elan (Lean 版本管理器)
RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y
ENV PATH="/root/.elan/bin:${PATH}"

# 设置工作目录
WORKDIR /app

# 初始化 Lean 项目并配置 mathlib4
RUN lake new eval_project math
WORKDIR /app/eval_project

# 下载 mathlib 的预编译缓存并预构建（这里才有 `lake exe cache`）
RUN lake exe cache get && lake build

# 构建 repl（单独仓库）。运行时用 `lake env` 提供 mathlib 环境。
WORKDIR /app
RUN git clone --depth 1 https://github.com/leanprover-community/repl.git /app/repl
WORKDIR /app/repl
RUN lake build

# 回到 app 目录准备 Python 环境
WORKDIR /app
COPY requirements.txt .
RUN python3 -m venv /opt/venv
ENV PATH="/opt/venv/bin:${PATH}"
RUN pip install --no-cache-dir -r requirements.txt

# 拷贝应用代码
COPY . .

# 暴露端口（HF Space 默认使用 7860）
CMD ["streamlit", "run", "app.py", "--server.port=7860", "--server.address=0.0.0.0"]