mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-30 17:16:16 +00:00
allaun
1b5d57bed3
- Containerfile: COPY prove.py, verify_lean.py, frozen_template/ into image - Systemd service: targets ComplexProjectiveSpace.lean (2 sorries) - verify_lean.py: scoped banned keyword check (target module only, not entire formal/)
26 lines
953 B
Docker
26 lines
953 B
Docker
FROM docker.io/runpod/autoresearch:1.0.7-cuda1281-ubuntu2204
|
|
|
|
# Install Lean 4 toolchain
|
|
RUN curl -sSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -o /tmp/elan-init.sh && \
|
|
sh /tmp/elan-init.sh -y --default-toolchain none && \
|
|
rm /tmp/elan-init.sh
|
|
|
|
ENV ELAN_HOME=/root/.elan
|
|
ENV PATH=$ELAN_HOME/bin:$PATH
|
|
|
|
# Install SilverSight toolchain
|
|
COPY SilverSight/lean-toolchain /tmp/lean-toolchain
|
|
RUN elan toolchain install $(cat /tmp/lean-toolchain) && \
|
|
elan default $(cat /tmp/lean-toolchain) && \
|
|
rm /tmp/lean-toolchain
|
|
|
|
# Copy autoresearch scripts (prove.py with 5-check pipeline, verify_lean.py)
|
|
COPY autoresearch/prove.py /opt/autoresearch/prove.py
|
|
COPY autoresearch/verify_lean.py /opt/autoresearch/verify_lean.py
|
|
COPY autoresearch/frozen_template/ /opt/autoresearch/frozen_template/
|
|
|
|
# Install Python deps
|
|
RUN pip install requests 2>/dev/null || true
|
|
|
|
WORKDIR /root/SilverSight
|
|
ENTRYPOINT ["/bin/bash", "-c"]
|