diff --git a/.github/workflows/checks.yml b/.github/workflows/checks.yml index b8ad96d0..d9eb47a7 100644 --- a/.github/workflows/checks.yml +++ b/.github/workflows/checks.yml @@ -66,6 +66,7 @@ jobs: --ignore=tests/test_lean_vuln_e2e.py --ignore=tests/test_comparator_security.py --ignore=tests/test_comparator_primitives.py + --ignore=tests/test_agent_image.py - suite: comparator-tests args: >- tests/test_singlefile_proof.py @@ -80,6 +81,10 @@ jobs: tests/test_fc100_isolation.py - suite: gold-proofs args: tests/test_gold_proofs.py + # Contract test for the agent image's declared compute stack (builds + # the agent image in-test, like the other container suites). + - suite: agent-image + args: tests/test_agent_image.py steps: - uses: actions/checkout@v4 - uses: astral-sh/setup-uv@v5 diff --git a/apn/__init__.py b/apn/__init__.py index dd2e1e7d..27f6d21e 100644 --- a/apn/__init__.py +++ b/apn/__init__.py @@ -1,4 +1,4 @@ __all__ = ["__version__"] -__version__ = "0.1.9" +__version__ = "0.1.10rc3" diff --git a/apn/lean/Dockerfile b/apn/lean/Dockerfile index e1361620..14f937b6 100644 --- a/apn/lean/Dockerfile +++ b/apn/lean/Dockerfile @@ -9,9 +9,17 @@ # rename -- the builder detects which from the checkout) # compiles. Shared by the two service images; not a service # itself. -# - agent -- the agent's workspace: base + PyPantograph + numerical -# Python libs. Deliberately contains NO verifier tooling (no -# comparator, no lean4export, no landrun). +# - agent -- the agent's workspace: base + a declared compute stack. +# One locked conda-forge env at /opt/env (python + Sage + +# the python stack + solver binaries; spec in +# compute-env.yaml, built in `compute_build`), apt tools +# conda-forge lacks, source-built and release-pinned solvers +# (`solvers_build`), Walnut (`walnut_build`), Julia with +# OSCAR/Hecke (`julia_build`), the Loogle Mathlib-search CLI +# (`loogle_build`), and per-tool docs downloaded from pinned +# upstream sources (`docs_fetch`) at /opt/docs. Deliberately +# contains NO verifier tooling (no comparator, no +# lean4export, no landrun). # - comparator -- the trusted verifier: base + the Comparator binary + the # lean4export binary + landrun + the pristine workspace tree. # Replaces the former `compile` + `scorer` pair: the @@ -25,8 +33,9 @@ # # - The FC project (statements, Mathlib, oleans) is pinned by the dataset's # FC_COMMIT and builds with its own lean-toolchain (v4.27.0 today). This is -# dataset identity; PyPantograph's repl must match it (oleans load only -# under the toolchain that built them). +# dataset identity; anything that importModules-loads oleans (lean4export, +# Loogle) must be built at this toolchain (oleans load only under the +# toolchain that built them). # - The lean4export *binary* (the runtime exporter) `importModules`-loads the # project's oleans in-process, so it MUST be built at the project # toolchain. Upstream's rev at that toolchain emits an export format the @@ -42,11 +51,21 @@ # comparator tip only, so its pin tracks the newest tag, not the project # toolchain (plan §2.1). # -# On an FC-pin bump: PyPantograph and the exporter's toolchain move with it. +# On an FC-pin bump: the exporter's and Loogle's builds move with it (Loogle +# is dependency-free and merely rebuilt at the pin's toolchain, with its +# Mathlib search index rebaked; see `loogle_build`). # On a comparator bump: move LEAN4EXPORT_COMMIT to the rev in comparator's # lake-manifest.json, re-verify the toolchain-override build, and re-run the # primitive-constants check (plan §2.3; the gold-proof suite exercises it). # +# The agent's compute stack is DECLARED, not accreted: the conda-forge env +# spec (compute-env.yaml) plus the explicit install lines in `compute_build`, +# `solvers_build`, and the `agent` stage are the source of truth for what the +# agent can run; tests/test_agent_image.py contract-tests the roster and +# apn/prompts.py advertises it. Loogle is the one deliberately pin-tied +# addition outside the base layer; everything else in the compute stack is +# Lean-agnostic. +# # The builder stage clones the whole formal-conjectures repo and builds the # library; base copies in ONLY the toolchain, the lake build artifacts # (oleans), and the proving-library source. The conjecture corpus (other OEIS @@ -54,6 +73,22 @@ # axioms), the library test suite, and repo tooling/docs/.git never reach the # agent's sandbox, so there is no contamination to strip after the fact. +# Shared pins: tools whose install AND whose /opt/docs documentation (the +# `docs_fetch` stage) must come from the SAME revision. Declared once here; +# stages redeclare `ARG ` (no value) to inherit these defaults, so a +# bump moves the tool and its docs together. Docs for tools pinned elsewhere +# (compute-env.yaml, bookworm's package table, the pip layer) hardcode the +# matching revision in docs_fetch with a comment naming the pin they mirror. +ARG MSOLVE_VERSION=0.10.1 +ARG PLANTRI_VERSION=55 +ARG DRATTRIM_VERSION=v05.22.2023 +ARG BREAKID_VERSION=3.1.3 +ARG SMS_VERSION=v2.1.1 +ARG CAKE_LPR_COMMIT=a36874a8b750b43fe4b385b8ddbf5b033e46a3fa +ARG KAMIS_VERSION=v3.2 +ARG GCLC_VERSION=v2026.1 +ARG MSIEVE_VERSION=1.53 + # --------------------------------------------------------------------------- # # Builder: clone + build the FC library (everything here is discarded). # # --------------------------------------------------------------------------- # @@ -180,18 +215,19 @@ ENV DEBIAN_FRONTEND=noninteractive \ APN_LEAN_PROJECT=/workspace/leanproject # Runtime libs for the Lean toolchain, plus the build tools the derived images -# need (the agent builds PyPantograph; the comparator image builds lean4export) -# and python3 (the agent uses it to drive PyPantograph and as a numerical -# scratchpad). +# need (the loogle_build and lean4export_build stages compile Lean projects) +# and python3 (loogle_build reads the baked manifest with it; the `generate` +# stage drives repo scripts with it). The agent's own python is NOT this one: +# the agent image puts its /opt/env python first on PATH. RUN apt-get update && apt-get install -y --no-install-recommends \ curl git ca-certificates build-essential libgmp-dev \ python3 python3-pip \ && rm -rf /var/lib/apt/lists/* # The Lean/lake toolchain (binaries + the project toolchain). The image ENV PATH -# above covers non-login execs (how ``sandbox().exec`` and the agent's PyPantograph -# subprocess run); add a profile snippet so *login* shells (e.g. ``bash -lc``) -# also find lake/lean. +# above covers non-login execs (plain ``sandbox().exec`` calls); add a profile +# snippet so *login* shells (``bash --login -c``, how the agent's bash tool +# execs) also find lake/lean. COPY --from=builder /root/.elan /root/.elan RUN echo 'export PATH=/root/.elan/bin:$PATH' > /etc/profile.d/elan.sh @@ -218,54 +254,490 @@ COPY --from=builder /staged ./ CMD ["sleep", "infinity"] # --------------------------------------------------------------------------- # -# agent: the agent's workspace. # +# compute_build: the agent's conda-forge compute env at /opt/env (python + # +# Sage + the python stack + solver binaries; spec: compute-env.yaml). Built # +# in its own stage so the multi-GB env is one cached layer COPY'd into agent, # +# re-run only when the spec or the pip pins change. The pip layer installs # +# into the SAME env (no second python): PyPI-only packages, pinned here. # # --------------------------------------------------------------------------- # -FROM base AS agent +FROM debian:bookworm-slim AS compute_build + +ENV DEBIAN_FRONTEND=noninteractive + +# build-essential: graphillion has no cp313 wheel, so its pip install below +# compiles the sdist (stage-local; the compiler does not ship). +RUN apt-get update && apt-get install -y --no-install-recommends \ + curl ca-certificates bzip2 build-essential \ + && rm -rf /var/lib/apt/lists/* + +ARG MICROMAMBA_VERSION=2.9.0 +RUN arch="$(uname -m)" \ + && case "$arch" in x86_64) plat=linux-64 ;; aarch64) plat=linux-aarch64 ;; *) echo "unsupported arch $arch" >&2; exit 1 ;; esac \ + && curl -sSfL "https://micro.mamba.pm/api/micromamba/${plat}/${MICROMAMBA_VERSION}" \ + | tar -xj -C /usr/local bin/micromamba + +COPY compute-env.yaml /tmp/compute-env.yaml +RUN micromamba create -y -p /opt/env -f /tmp/compute-env.yaml \ + && micromamba clean -afy + +# PyPI-only packages, into the same env. snappy is SnapPy (3-manifold +# topology), not the compression lib. pyscipopt's wheel bundles libscip +# (SCIP via conda is impossible: every scip/soplex build wants a boost newer +# than the sage stack's pin). graphillion compiles from sdist (no cp313 +# wheel; verified clean on py3.13, both arches). +RUN /opt/env/bin/pip install --no-cache-dir \ + python-sat==1.9.dev15 \ + cvc5==1.3.4 \ + ortools==9.15.6755 \ + snappy==3.3.2 \ + pysindy==2.1.0 \ + hypothesis==6.165.10 \ + libsemigroups_pybind11==1.4.4 \ + pymanopt==2.2.1 \ + graphillion==2.1 \ + pyscipopt==6.2.1 \ + && find /opt/env -name '__pycache__' -type d -prune -exec rm -rf {} + + +# --------------------------------------------------------------------------- # +# solvers_build: tools with no conda-forge or bookworm packaging, built from # +# pinned sources (plus pinned official release binaries: cvc5 static, whose # +# PyPI wheel in compute_build carries only the python API; vampire; cake_lpr; # +# and the x86-only LLR/PFGW primality provers). Everything lands in /out/bin # +# and links only the libc family, libstdc++, and zlib from the shared # +# bookworm userland (flint/gmp/mpfr are linked statically), so the binaries # +# drop straight into agent. # +# --------------------------------------------------------------------------- # +FROM debian:bookworm-slim AS solvers_build + +ENV DEBIAN_FRONTEND=noninteractive + +RUN apt-get update && apt-get install -y --no-install-recommends \ + curl ca-certificates build-essential unzip m4 \ + cmake git subversion p7zip perl zlib1g-dev \ + libboost-graph-dev libboost-program-options-dev \ + libgmp-dev libmpfr-dev \ + && rm -rf /var/lib/apt/lists/* \ + && mkdir -p /out/bin + +# kissat: state-of-the-art CDCL SAT solver (DIMACS in/out). +ARG KISSAT_VERSION=rel-4.0.4 +RUN curl -sSfL "https://github.com/arminbiere/kissat/archive/refs/tags/${KISSAT_VERSION}.tar.gz" \ + | tar xz -C /tmp \ + && cd /tmp/kissat-* \ + && ./configure && make -j"$(nproc)" \ + && install -m 755 build/kissat /out/bin/kissat \ + && rm -rf /tmp/kissat-* + +# plantri: planar-graph generator (Brinkmann & McKay). +ARG PLANTRI_VERSION +RUN curl -sSfL "https://users.cecs.anu.edu.au/~bdm/plantri/plantri${PLANTRI_VERSION}.tar.gz" \ + | tar xz -C /tmp \ + && cd /tmp/plantri* \ + && make plantri \ + && install -m 755 plantri /out/bin/plantri \ + && rm -rf /tmp/plantri* + +# prover9/mace4: first-order theorem prover + finite-model finder. Upstream +# (cs.unm.edu LADR-2009-11A) has no releases and Debian dropped the package; +# built from a pinned commit of the ai4reason mirror of that final release. +ARG PROVER9_COMMIT=cdca95a51d3c3459b8fd2ebbb5ac1504be2172e3 +RUN curl -sSfL "https://github.com/ai4reason/Prover9/archive/${PROVER9_COMMIT}.tar.gz" \ + | tar xz -C /tmp \ + && cd /tmp/Prover9-* \ + && make all \ + && install -m 755 bin/prover9 bin/mace4 bin/interpformat bin/prooftrans /out/bin/ \ + && rm -rf /tmp/Prover9-* + +# msolve: multivariate polynomial system solver (Groebner bases). Needs +# FLINT >= 3, which bookworm lacks -- both are built here, FLINT static so +# nothing but the msolve binaries ship. +ARG FLINT_VERSION=3.6.0 +ARG MSOLVE_VERSION +RUN curl -sSfL "https://github.com/flintlib/flint/releases/download/v${FLINT_VERSION}/flint-${FLINT_VERSION}.tar.gz" \ + | tar xz -C /tmp \ + && cd /tmp/flint-* \ + && ./configure --disable-shared --prefix=/usr/local \ + && make -j"$(nproc)" && make install \ + && rm -rf /tmp/flint-* +RUN curl -sSfL "https://github.com/algebraic-solving/msolve/releases/download/v${MSOLVE_VERSION}/msolve-${MSOLVE_VERSION}.tar.gz" \ + | tar xz -C /tmp \ + && cd /tmp/msolve-* \ + && ./configure --disable-shared \ + && make -j"$(nproc)" \ + && install -m 755 msolve /out/bin/msolve \ + && rm -rf /tmp/msolve-* + +# cvc5: SMT solver, official pinned static release binary (matches the pip +# bindings' version in compute_build). +ARG CVC5_VERSION=1.3.4 +RUN arch="$(uname -m)" \ + && case "$arch" in x86_64) a=x86_64 ;; aarch64) a=arm64 ;; *) echo "unsupported arch $arch" >&2; exit 1 ;; esac \ + && curl -sSfL -o /tmp/cvc5.zip \ + "https://github.com/cvc5/cvc5/releases/download/cvc5-${CVC5_VERSION}/cvc5-Linux-${a}-static.zip" \ + && unzip -q /tmp/cvc5.zip -d /tmp/cvc5 \ + && install -m 755 /tmp/cvc5/*/bin/cvc5 /out/bin/cvc5 \ + && rm -rf /tmp/cvc5 /tmp/cvc5.zip + +# vampire: superposition first-order prover + finite-model builder (--mode +# fmb), official pinned release binaries (link only libc/libstdc++). +ARG VAMPIRE_VERSION=v5.1.0 +RUN arch="$(uname -m)" \ + && case "$arch" in \ + x86_64) z=vampire-Linux-X64.zip; sha=495828dc76cb17a27080d62dedce755e46de96f47f06f5f0ad4be9cdaf6f968f ;; \ + aarch64) z=vampire-Linux-ARM64.zip; sha=7abc39224fdf41bdb2c241f8b180a80b7c1a4bce1e46dc79df02cfea2798ad5c ;; \ + *) echo "unsupported arch $arch" >&2; exit 1 ;; \ + esac \ + && curl -sSfL -o /tmp/vampire.zip \ + "https://github.com/vprover/vampire/releases/download/${VAMPIRE_VERSION}/${z}" \ + && echo "${sha} /tmp/vampire.zip" | sha256sum -c - \ + && unzip -q /tmp/vampire.zip -d /tmp/vampire \ + && install -m 755 "$(find /tmp/vampire -type f -name vampire)" /out/bin/vampire \ + && rm -rf /tmp/vampire /tmp/vampire.zip + +# drat-trim + lrat-check: proof checkers for SAT solvers' UNSAT certificates +# (DRAT from kissat/cryptominisat; DRAT->LRAT conversion). +ARG DRATTRIM_VERSION +RUN curl -sSfL "https://github.com/marijnheule/drat-trim/archive/refs/tags/${DRATTRIM_VERSION}.tar.gz" \ + | tar xz -C /tmp \ + && cd /tmp/drat-trim-* \ + && make \ + && install -m 755 drat-trim lrat-check /out/bin/ \ + && rm -rf /tmp/drat-trim-* + +# cake_lpr: formally verified LRAT proof checker (CakeML); built from the +# repo's pre-generated per-arch assembly with one gcc call. +ARG CAKE_LPR_COMMIT +RUN curl -sSfL "https://github.com/tanyongkiam/cake_lpr/archive/${CAKE_LPR_COMMIT}.tar.gz" \ + | tar xz -C /tmp \ + && cd /tmp/cake_lpr-* \ + && case "$(uname -m)" in x86_64) s=cake_lpr.S ;; aarch64) s=cake_lpr_arm8.S ;; esac \ + && gcc -O2 -std=c99 basis_ffi.c "$s" -o /out/bin/cake_lpr \ + && rm -rf /tmp/cake_lpr-* + +# BreakID: static CNF symmetry breaking (preprocessor for SAT searches). +ARG BREAKID_VERSION +RUN git clone --depth 1 --branch "release/${BREAKID_VERSION}" \ + https://github.com/meelgroup/breakid /tmp/breakid \ + && cmake -S /tmp/breakid -B /tmp/breakid/build -DCMAKE_BUILD_TYPE=Release \ + && cmake --build /tmp/breakid/build -j"$(nproc)" \ + && install -m 755 /tmp/breakid/build/breakid /out/bin/breakid \ + && rm -rf /tmp/breakid + +# SMS (smsg): SAT-modulo-symmetries graph search -- find/enumerate graphs with +# a property, modulo isomorphism. CaDiCaL is bundled as a pinned submodule. +ARG SMS_VERSION +RUN git clone --depth 1 --branch "${SMS_VERSION}" --recurse-submodules \ + https://github.com/markirch/sat-modulo-symmetries /tmp/sms \ + && cd /tmp/sms/cadical_sms && ./configure -fPIC && make -j"$(nproc)" \ + && cd /tmp/sms \ + # static boost so the binary keeps to the shared bookworm userland + && cmake -B build -S . -DCMAKE_BUILD_TYPE=Release -DBoost_USE_STATIC_LIBS=ON \ + && cmake --build build -j"$(nproc)" \ + && install -m 755 build/src/smsg /out/bin/smsg \ + && rm -rf /tmp/sms + +# march_cu: cube-and-conquer splitter for hard SAT instances (Heule's CnC; +# no tags upstream, commit-pinned). -fcommon: pre-C99 tentative definitions. +ARG MARCH_CU_COMMIT=705b60c6491ef2b61988b3ce6ac674be1b90571d +RUN curl -sSfL "https://github.com/marijnheule/CnC/archive/${MARCH_CU_COMMIT}.tar.gz" \ + | tar xz -C /tmp \ + && cd /tmp/CnC-*/march_cu \ + && make CFLAGS='-O3 -fno-strict-aliasing -Wall -DNDEBUG -fcommon' \ + && install -m 755 march_cu /out/bin/march_cu \ + && rm -rf /tmp/CnC-* + +# msieve: SIQS/NFS integer factorization past gmp-ecm's reach. OPT_FLAGS +# overrides the Makefile's -march=native so the binary is portable. +ARG MSIEVE_VERSION +RUN curl -sSfL "https://downloads.sourceforge.net/project/msieve/msieve/Msieve%20v${MSIEVE_VERSION}/msieve$(echo "${MSIEVE_VERSION}" | tr -d .)_src.tar.gz" \ + | tar xz -C /tmp \ + && cd /tmp/msieve-* \ + && make all -j"$(nproc)" OPT_FLAGS='-O3 -fomit-frame-pointer -D_FILE_OFFSET_BITS=64 -DNDEBUG' \ + && install -m 755 msieve /out/bin/msieve \ + && rm -rf /tmp/msieve-* + +# redumis (KaMIS): near-optimal maximum independent sets at scales exact +# solvers can't reach (KaHIP is vendored in the release tarball). +ARG KAMIS_VERSION +RUN curl -sSfL "https://github.com/KarlsruheMIS/KaMIS/archive/refs/tags/${KAMIS_VERSION}.tar.gz" \ + | tar xz -C /tmp \ + && cmake -S /tmp/KaMIS-* -B /tmp/kamis-build -DCMAKE_BUILD_TYPE=Release \ + && cmake --build /tmp/kamis-build -j"$(nproc)" --target redumis \ + && install -m 755 /tmp/kamis-build/redumis /out/bin/redumis \ + && rm -rf /tmp/KaMIS-* /tmp/kamis-build + +# gclc: automated Euclidean geometry proving (area/Wu methods; CLI only). +ARG GCLC_VERSION +RUN git clone --depth 1 --branch "${GCLC_VERSION}" https://github.com/janicicpredrag/gclc /tmp/gclc \ + && cmake -S /tmp/gclc -B /tmp/gclc/build -DCMAKE_BUILD_TYPE=Release -Dgui=OFF \ + && cmake --build /tmp/gclc/build -j"$(nproc)" \ + && install -m 755 /tmp/gclc/build/gclc /out/bin/gclc \ + && rm -rf /tmp/gclc + +# The special-form primality toolchain, amd64 images only (CI/production): +# srsieve2 sieves k*b^n+-c candidate grids (mtsieve suite; SourceForge SVN, +# revision-pinned; its makefile only knows x86 and 32-bit ARM), then sllr64 +# (LLR) and pfgw64 (OpenPFGW) prove primality at 10^5..10^7 digits (gwnum is +# x86-64 assembly -- no arm route exists). +ARG MTSIEVE_SVN_REV=469 +ARG LLR_VERSION=407 +ARG PFGW_VERSION=4.1.8 +RUN if [ "$(uname -m)" = x86_64 ]; then \ + svn checkout -q -r "${MTSIEVE_SVN_REV}" https://svn.code.sf.net/p/mtsieve/svn/ /tmp/mtsieve \ + && cd /tmp/mtsieve \ + && make -j"$(nproc)" srsieve2 \ + && install -m 755 srsieve2 /out/bin/srsieve2 \ + && rm -rf /tmp/mtsieve; \ + fi +RUN if [ "$(uname -m)" = x86_64 ]; then \ + # jpenne.free.fr is HTTP-only; integrity comes from the sha256 pin. + curl -sSfL -o /tmp/llr.zip "http://jpenne.free.fr/llr4/llr${LLR_VERSION}slinux64.zip" \ + && echo "b92424d85d0d37788bb33613ec1af2b6d5cb1f5ce37be5ed062b0aad604a6ab3 /tmp/llr.zip" | sha256sum -c - \ + && unzip -q /tmp/llr.zip -d /tmp/llr \ + && install -m 755 "$(find /tmp/llr -type f -name sllr64)" /out/bin/sllr64 \ + && curl -sSfL -o /tmp/pfgw.7z "https://downloads.sourceforge.net/project/openpfgw/pfgw_linux_${PFGW_VERSION}.7z" \ + && echo "aadf885e2d6489866bb7eeea2ba3f75a3fa02e679f1d6a86fd2632e042a99c99 /tmp/pfgw.7z" | sha256sum -c - \ + && 7zr x -o/tmp/pfgw /tmp/pfgw.7z >/dev/null \ + && install -m 755 /tmp/pfgw/pfgw64 /out/bin/pfgw64 \ + && rm -rf /tmp/llr /tmp/llr.zip /tmp/pfgw /tmp/pfgw.7z; \ + fi + +# --------------------------------------------------------------------------- # +# walnut_build: Walnut, the decision procedure for automatic sequences / # +# base-k digit statements (Buechi arithmetic). Java; built once with the # +# repo's own gradle wrapper, shipped as the /opt/walnut tree and run via # +# upstream's launcher: /opt/walnut/walnut.sh (JRE comes from the agent # +# stage's default-jre-headless). # +# --------------------------------------------------------------------------- # +FROM debian:bookworm-slim AS walnut_build + +ENV DEBIAN_FRONTEND=noninteractive -# PyPantograph commit b8608f3 pins Pantograph v0.3.13, whose repl targets Lean -# v4.27.0 -- matching this track's Mathlib + FormalConjectures oleans. (The repl -# must be built with the same toolchain that produced the oleans it loads.) -# The clone is removed after install so the only importable `pantograph` is the -# installed package (a lingering source tree would shadow it for any python -# started inside /opt/PyPantograph, and the source tree lacks the built repl). -ARG PYPANTOGRAPH_COMMIT=b8608f3 -RUN git clone https://github.com/lenianiva/PyPantograph.git /opt/PyPantograph \ - && cd /opt/PyPantograph \ - && git checkout "${PYPANTOGRAPH_COMMIT}" \ - && git submodule update --init --recursive \ - && pip3 install --break-system-packages --no-cache-dir . \ - && cd / && rm -rf /opt/PyPantograph - -# In-sandbox references for the agent (the sandbox has no network), vendored -# version-matched to the installed package: PyPantograph docs + examples at the -# pinned commit, and Pantograph's repl protocol reference at the submodule -# commit that pin builds. -COPY pypantograph-docs /opt/pypantograph-docs -COPY pantograph-docs /opt/pantograph-docs - -# Numerical/symbolic scratchpad for the agent (the `bash` tool runs python3 in -# this image). The sandbox has no network, so everything is baked in here. -# - sagemath: a full computer algebra system on the `sage` command, bundling -# PARI/GP, FLINT, Maxima, GAP and Singular -- far stronger than sympy for -# number theory (factoring, modular arithmetic, elliptic curves, continued -# fractions) and the dialect much of OEIS's own reference code is written in. -# - python3-{numpy,sympy,mpmath}: importable directly from `python3` (sympy = -# exact symbolic, mpmath = arbitrary precision with pslq/identify). Pulled -# from apt alongside sagemath so all versions resolve mutually consistent -# (a pip --break-system-packages upgrade could outrun what Sage expects). -# This ~1.5 GB install is its own cached layer. RUN apt-get update && apt-get install -y --no-install-recommends \ - sagemath python3-numpy python3-sympy python3-mpmath \ + curl ca-certificates openjdk-17-jdk-headless git \ && rm -rf /var/lib/apt/lists/* -# CLI tools for the agent's `bash` tool (git is already in `base`): jq for JSON, -# ripgrep for fast search (`rg`). In `agent` so both run conditions get them and -# the agent can be prompted to use `rg` consistently whether or not /corpus is -# present. A cheap layer kept after the sagemath layer so editing it never busts -# that cache. -RUN apt-get update && apt-get install -y --no-install-recommends jq ripgrep \ +# Upstream's build.sh is its gradle invocation + chmod, followed by an +# interactive "Press enter" prompt that exits 1 in a non-interactive build -- +# so run those two commands directly. +ARG WALNUT_VERSION=v7.1.0 +RUN curl -sSfL "https://github.com/Walnut-Theorem-Prover/Walnut/archive/refs/tags/${WALNUT_VERSION}.tar.gz" \ + | tar xz -C /opt \ + && mv /opt/Walnut-* /opt/walnut \ + && cd /opt/walnut \ + && ./gradlew clean customFatJar \ + && chmod +x walnut.sh \ + && rm -rf /root/.gradle + +# --------------------------------------------------------------------------- # +# julia_build: Julia + OSCAR/Hecke (computer algebra: Galois groups, number # +# fields, group theory) as a fully precompiled, offline-usable depot. The # +# multi-target JULIA_CPU_TARGET (the same lists the official binaries use) # +# makes the baked pkgimages load on any deploy CPU. NEVER build this stage # +# under qemu emulation: precompilation crashes there (native-only, both # +# arches verified for artifact coverage). # +# --------------------------------------------------------------------------- # +FROM debian:bookworm-slim AS julia_build + +RUN apt-get update && apt-get install -y --no-install-recommends \ + curl ca-certificates \ && rm -rf /var/lib/apt/lists/* +# sha256s from https://julialang-s3.julialang.org/bin/checksums/julia-1.12.7.sha256 +ARG JULIA_VERSION=1.12.7 +RUN arch="$(uname -m)" \ + && case "$arch" in \ + x86_64) a=x64/1.12/julia-${JULIA_VERSION}-linux-x86_64.tar.gz; \ + sha=4e7e9e776634d24835250de67cde39b0d4af15bc432eb20697e6be6c28ea69e8 ;; \ + aarch64) a=aarch64/1.12/julia-${JULIA_VERSION}-linux-aarch64.tar.gz; \ + sha=9243c0b524c7f300883240a1ee5ea3916a30e070bff718acf8ccaee31a731ef2 ;; \ + *) echo "unsupported arch $arch" >&2; exit 1 ;; \ + esac \ + && curl -fsSL "https://julialang-s3.julialang.org/bin/linux/${a}" -o /tmp/julia.tar.gz \ + && echo "${sha} /tmp/julia.tar.gz" | sha256sum -c - \ + && mkdir -p /opt/julia \ + && tar -xzf /tmp/julia.tar.gz -C /opt/julia --strip-components=1 \ + && rm /tmp/julia.tar.gz + +ENV JULIA_DEPOT_PATH=/opt/julia-depot +ARG OSCAR_VERSION=1.8.1 +ARG HECKE_VERSION=0.39.22 +RUN case "$(uname -m)" in \ + x86_64) export JULIA_CPU_TARGET='generic;sandybridge,-xsaveopt,clone_all;haswell,-rdrnd,base(1);x86-64-v4,-rdrnd,base(1)' ;; \ + aarch64) export JULIA_CPU_TARGET='generic;cortex-a57;thunderx2t99;carmel,clone_all;apple-m1,base(3);neoverse-512tvb,-rand,-fpac,base(3)' ;; \ + esac \ + && /opt/julia/bin/julia -e "using Pkg; Pkg.add([ \ + PackageSpec(name=\"Oscar\", version=\"${OSCAR_VERSION}\"), \ + PackageSpec(name=\"Hecke\", version=\"${HECKE_VERSION}\")]); \ + Pkg.precompile(); Pkg.gc()" \ + # The depot must be complete: loading may not touch the network. + && JULIA_PKG_OFFLINE=true /opt/julia/bin/julia -e \ + 'using Oscar; using Hecke; println("Oscar ", Oscar.VERSION_NUMBER)' + +# --------------------------------------------------------------------------- # +# loogle_build: the Loogle type-pattern Mathlib search CLI. Upstream's # +# "Running locally" contract: the binary is dependency-free, must merely be # +# built with the TARGET project's toolchain, and then searches any Lake # +# project via `lake env loogle --module ""` (it reads LEAN_PATH). # +# The first query builds a search index cached next to the module's .olean # +# and auto-invalidated when the oleans change; running one here bakes that # +# index (and smoke-tests the build), so agents get fast queries. # +# --------------------------------------------------------------------------- # +FROM base AS loogle_build + +ARG LOOGLE_COMMIT=9f11169aaebf1ed1e7dcc4077f2aafe0fcf66fd0 +RUN git clone https://github.com/nomeata/loogle.git /opt/loogle \ + && git -C /opt/loogle checkout --detach "${LOOGLE_COMMIT}" \ + && cp /workspace/leanproject/lean-toolchain /opt/loogle/lean-toolchain \ + && cd /opt/loogle \ + && lake build \ + && cd /workspace/leanproject \ + && lake env /opt/loogle/.lake/build/bin/loogle --module Mathlib "Nat.Prime" > /dev/null + +# --------------------------------------------------------------------------- # +# docs_fetch: in-sandbox references at /opt/docs/, DOWNLOADED at build # +# from pinned sources (never vendored in the repo, never PDFs, always the # +# upstream files verbatim). Each fetch is pinned to the revision the image # +# actually installs: shared ARGs (top of file) where the install is ARG- # +# pinned, hardcoded matching revisions (with the mirrored pin named in a # +# comment) where the install pin lives in compute-env.yaml / bookworm / the # +# pip layer. Tools whose only docs are PDFs or mutable webpages ship # +# undocumented (their --help still works). # +# --------------------------------------------------------------------------- # +FROM debian:bookworm-slim AS docs_fetch + +ENV DEBIAN_FRONTEND=noninteractive + +RUN apt-get update && apt-get install -y --no-install-recommends \ + curl ca-certificates git \ + && rm -rf /var/lib/apt/lists/* + +# Single-file fetches from pinned raw URLs. +ARG DRATTRIM_VERSION +ARG BREAKID_VERSION +ARG CAKE_LPR_COMMIT +ARG KAMIS_VERSION +ARG GCLC_VERSION +ARG MSOLVE_VERSION +# Must equal loogle_build's LOOGLE_COMMIT. +ARG LOOGLE_DOCS_COMMIT=9f11169aaebf1ed1e7dcc4077f2aafe0fcf66fd0 +RUN set -e; \ + fetch() { mkdir -p "/opt/docs/$1" && curl -sSfL -o "/opt/docs/$1/$2" "$3"; }; \ + fetch loogle README.md "https://raw.githubusercontent.com/nomeata/loogle/${LOOGLE_DOCS_COMMIT}/README.md"; \ + fetch loogle blurb.md "https://raw.githubusercontent.com/nomeata/loogle/${LOOGLE_DOCS_COMMIT}/blurb.md"; \ + fetch msolve msolve-tutorial.tex "https://raw.githubusercontent.com/algebraic-solving/msolve/v${MSOLVE_VERSION}/doc/msolve-tutorial.tex"; \ + fetch drat-trim README.md "https://raw.githubusercontent.com/marijnheule/drat-trim/${DRATTRIM_VERSION}/README.md"; \ + fetch breakid README.md "https://raw.githubusercontent.com/meelgroup/breakid/release/${BREAKID_VERSION}/README.md"; \ + fetch cake_lpr README.md "https://raw.githubusercontent.com/tanyongkiam/cake_lpr/${CAKE_LPR_COMMIT}/README.md"; \ + fetch kamis README.md "https://raw.githubusercontent.com/KarlsruheMIS/KaMIS/${KAMIS_VERSION}/README.md"; \ + fetch gclc gclc_man.tex "https://raw.githubusercontent.com/janicicpredrag/gclc/${GCLC_VERSION}/manual/gclc_man.tex"; \ + # matches bookworm coinor-csdp 6.2.0-4 + fetch csdp csdpuser.tex "https://raw.githubusercontent.com/coin-or/Csdp/releases/6.2.0/doc/csdpuser.tex"; \ + # matches the pip layer's graphillion==2.1 + fetch graphillion README.md "https://raw.githubusercontent.com/takemaru/graphillion/v2.1/README.md"; \ + # matches compute-env.yaml 4ti2=1.6.15 + for f in 4ti2_manual 4ti2_manual_beginner 4ti2_manual_advanced 4ti2_manual_ref 4ti2_manual_api; do \ + fetch 4ti2 "$f.tex" "https://raw.githubusercontent.com/4ti2/4ti2/Release_1_6_15/doc/$f.tex"; \ + done + +# Tag-pinned clones where the docs are a file set. +ARG SMS_VERSION +RUN set -e; \ + clonedocs() { git clone -q --depth 1 --branch "$2" "$1" /tmp/d && mkdir -p "/opt/docs/$3"; }; \ + # matches solvers_build's SMS_VERSION + clonedocs https://github.com/markirch/sat-modulo-symmetries "${SMS_VERSION}" sms \ + && cp /tmp/d/docs/*.md /opt/docs/sms/ && rm -rf /tmp/d; \ + # matches compute-env.yaml normaliz=3.11.0 + clonedocs https://github.com/Normaliz/Normaliz v3.11.0 normaliz \ + && cp /tmp/d/doc/*.tex /tmp/d/README.md /opt/docs/normaliz/ && rm -rf /tmp/d; \ + # matches the pip layer's snappy==3.3.2 (SnapPy) + clonedocs https://github.com/3-manifolds/SnapPy 3.3.2_as_released snappy \ + && cp /tmp/d/doc_src/*.rst /opt/docs/snappy/ && rm -rf /tmp/d; \ + # matches compute-env.yaml python-flint=0.8.0 + clonedocs https://github.com/flintlib/python-flint 0.8.0 python-flint \ + && cp /tmp/d/doc/source/*.rst /opt/docs/python-flint/ && rm -rf /tmp/d; \ + # matches bookworm regina-normal 7.3 (handbook source; DocBook is text) + clonedocs https://github.com/regina-normal/regina regina-7.3 regina \ + && cp /tmp/d/qtui/doc/regina/*.docbook /opt/docs/regina/ && rm -rf /tmp/d + +# Tarball-shipped docs (same tarballs the installs use). +ARG PLANTRI_VERSION +RUN set -e; \ + mkdir -p /opt/docs/plantri /opt/docs/lrslib /opt/docs/msieve; \ + curl -sSfL "https://users.cecs.anu.edu.au/~bdm/plantri/plantri${PLANTRI_VERSION}.tar.gz" | tar xz -C /tmp \ + && cp /tmp/plantri*/plantri-guide.txt /opt/docs/plantri/ && rm -rf /tmp/plantri*; \ + # matches compute-env.yaml lrslib=73.a + curl -sSfL "https://cgm.cs.mcgill.ca/~avis/C/lrslib/archive/lrslib-073a.tar.gz" | tar xz -C /tmp \ + && cp -r /tmp/lrslib-073a/man/html /opt/docs/lrslib/man-html \ + && cp /tmp/lrslib-073a/README /opt/docs/lrslib/ && rm -rf /tmp/lrslib-073a; \ + curl -sSfL "https://downloads.sourceforge.net/project/msieve/msieve/Msieve%20v1.53/msieve153_src.tar.gz" | tar xz -C /tmp \ + && cp /tmp/msieve-*/Readme* /opt/docs/msieve/ && rm -rf /tmp/msieve-* + +# Walnut's per-command help ships inside the same build the image runs. +COPY --from=walnut_build /opt/walnut/README.md /opt/docs/walnut/README.md +COPY --from=walnut_build ["/opt/walnut/Help Documentation/Commands", "/opt/docs/walnut/commands"] + +# --------------------------------------------------------------------------- # +# agent: the agent's workspace. Layer order is big/stable first (the conda # +# env), then apt, then the small solver binaries, then Loogle, then docs # +# (which churn most). # +# --------------------------------------------------------------------------- # +FROM base AS agent + +# The compute env (see compute-env.yaml). /opt/env/bin goes FIRST on PATH so +# the env's python IS the agent's `python3` (and sage, gp, gap, z3, ... all +# resolve there); the profile.d snippet covers login shells (`bash --login +# -c`, how apn.tools execs), the ENV covers plain execs. +COPY --from=compute_build /opt/env /opt/env +ENV PATH=/opt/env/bin:$PATH +RUN echo 'export PATH=/opt/env/bin:$PATH' > /etc/profile.d/compute-env.sh + +# Julia with the precompiled OSCAR/Hecke depot (see julia_build). The depot +# path must match the build-time one or every load re-precompiles. +COPY --from=julia_build /opt/julia /opt/julia +COPY --from=julia_build /opt/julia-depot /opt/julia-depot +ENV JULIA_DEPOT_PATH=/opt/julia-depot +RUN ln -s /opt/julia/bin/julia /usr/local/bin/julia \ + && echo 'export JULIA_DEPOT_PATH=/opt/julia-depot' > /etc/profile.d/julia.sh + +# Tools conda-forge lacks, from bookworm: polymake (polyhedral geometry), +# Macaulay2 (commutative algebra), regina-normal (low-dimensional topology; +# `regina-python`), cryptominisat (SAT, newer here than conda-forge's), +# coinor-csdp (semidefinite programming, `csdp`), topcom (triangulations), +# cadabra2 (tensor algebra), minizinc (CP modeling), berkeley-abc (Boolean +# networks), eprover (first-order ATP), mpsolve (certified polynomial roots), +# default-jre-headless (runs Walnut), jq + ripgrep for the bash tool (git is +# already in `base`), libmpfr6 (msolve's one non-static runtime link besides +# gmp, which base's libgmp-dev already provides). +RUN apt-get update && apt-get install -y --no-install-recommends \ + polymake macaulay2 regina-normal cryptominisat coinor-csdp \ + topcom cadabra2 minizinc berkeley-abc eprover mpsolve \ + default-jre-headless jq ripgrep libmpfr6 \ + && rm -rf /var/lib/apt/lists/* + +# Source-built and release-pinned solver binaries (see solvers_build). +COPY --from=solvers_build /out/bin/ /usr/local/bin/ + +# Walnut (automatic-sequence decision procedure): upstream's own tree and +# launcher, run as /opt/walnut/walnut.sh (java from apt above). +COPY --from=walnut_build /opt/walnut /opt/walnut + +# Loogle: the dependency-free binary, plus the Mathlib search index it baked +# next to Mathlib.olean (COPY preserves mtimes, and this stage shares base's +# layers with loogle_build, so the index stays valid; were it ever judged +# stale, loogle transparently rebuilds it). Invocation, per upstream's docs +# (vendored at /opt/docs/loogle): from the project, +# lake env loogle --module Mathlib "" +COPY --from=loogle_build /opt/loogle/.lake/build/bin/loogle /usr/local/bin/loogle +COPY --from=loogle_build \ + /workspace/leanproject/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib.loogle-index \ + /workspace/leanproject/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib.loogle-index + +# In-sandbox references (the sandbox has no network): version-matched upstream +# docs, downloaded at build (see docs_fetch). Last: docs churn more than any +# layer above. +COPY --from=docs_fetch /opt/docs /opt/docs + CMD ["sleep", "infinity"] # --------------------------------------------------------------------------- # diff --git a/apn/lean/compute-env.yaml b/apn/lean/compute-env.yaml new file mode 100644 index 00000000..f9728872 --- /dev/null +++ b/apn/lean/compute-env.yaml @@ -0,0 +1,54 @@ +# The agent's compute environment: one locked conda-forge env at /opt/env +# (created by the Dockerfile's `compute_build` stage; /opt/env/bin is first on +# the agent's PATH, so this env's python IS the agent's `python3`). +# +# Every tool the agent is promised is listed here EXPLICITLY with an exact +# pin, even where it would arrive anyway as a sage dependency (pari, gap, +# maxima, singular, ecm, nauty, ...): the roster must not depend on what sage +# happens to pull. Transitive dependencies not listed here resolve at image +# build time. Version bumps are deliberate edits to this file. The solve is +# verified for linux-64 and linux-aarch64 (local dev on Apple silicon); when +# bumping a pin, keep versions that exist for both platforms. +# +# pip-layer packages (python-sat, cvc5 bindings, ortools, snappy) are +# installed into this same env by the Dockerfile, pinned there. +name: compute +channels: + - conda-forge +dependencies: + - python=3.13.15 + - pip=26.2.1 + # computer algebra systems and their engines + - sage=10.9 + - pari=2.17.3 # PARI/GP: the `gp` binary + libpari + - gap-defaults=4.15.1 # GAP: computational group theory + - maxima=5.49.0 + - singular=4.4.1.p5 + # python stack + - numpy=2.5.2 + - scipy=1.18.0 + - sympy=1.14.0 + - mpmath=1.4.1 + - pandas=3.0.5 + - networkx=3.6.1 + - python-igraph=0.11.9 + - python-flint=0.8.0 + - highspy=1.15.1 + # solvers (binary + python bindings) + - z3-solver=5.1.0.0 + - glpk=5.0 + - clingo=5.8.2 # ASP: clingo binary + python module + - cvxpy=1.9.2 # convex-optimization modeling front end + - clarabel=0.11.1 + # lattice reduction + - fpylll=0.6.4 + # number theory CLI tools + - primesieve=12.13 + - primecount=8.2 + - ecm=7.0.6 # GMP-ECM factorization + # graph / discrete geometry / algebra CLI tools + - nauty=2.9.3 + - cliquer=1.23 + - normaliz=3.11.0 + - 4ti2=1.6.15 + - lrslib=73.a diff --git a/apn/lean/pantograph-docs/LICENSE b/apn/lean/pantograph-docs/LICENSE deleted file mode 100644 index 34f63a39..00000000 --- a/apn/lean/pantograph-docs/LICENSE +++ /dev/null @@ -1,190 +0,0 @@ - Apache License - Version 2.0, January 2004 - http://www.apache.org/licenses/ - - TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION - - 1. Definitions. - - "License" shall mean the terms and conditions for use, reproduction, - and distribution as defined by Sections 1 through 9 of this document. - - "Licensor" shall mean the copyright owner or entity authorized by - the copyright owner that is granting the License. - - "Legal Entity" shall mean the union of the acting entity and all - other entities that control, are controlled by, or are under common - control with that entity. For the purposes of this definition, - "control" means (i) the power, direct or indirect, to cause the - direction or management of such entity, whether by contract or - otherwise, or (ii) ownership of fifty percent (50%) or more of the - outstanding shares, or (iii) beneficial ownership of such entity. - - "You" (or "Your") shall mean an individual or Legal Entity - exercising permissions granted by this License. - - "Source" form shall mean the preferred form for making modifications, - including but not limited to software source code, documentation - source, and configuration files. - - "Object" form shall mean any form resulting from mechanical - transformation or translation of a Source form, including but - not limited to compiled object code, generated documentation, - and conversions to other media types. - - "Work" shall mean the work of authorship, whether in Source or - Object form, made available under the License, as indicated by a - copyright notice that is included in or attached to the work - (an example is provided in the Appendix below). - - "Derivative Works" shall mean any work, whether in Source or Object - form, that is based on (or derived from) the Work and for which the - editorial revisions, annotations, elaborations, or other modifications - represent, as a whole, an original work of authorship. For the purposes - of this License, Derivative Works shall not include works that remain - separable from, or merely link (or bind by name) to the interfaces of, - the Work and Derivative Works thereof. - - "Contribution" shall mean any work of authorship, including - the original version of the Work and any modifications or additions - to that Work or Derivative Works thereof, that is intentionally - submitted to Licensor for inclusion in the Work by the copyright owner - or by an individual or Legal Entity authorized to submit on behalf of - the copyright owner. For the purposes of this definition, "submitted" - means any form of electronic, verbal, or written communication sent - to the Licensor or its representatives, including but not limited to - communication on electronic mailing lists, source code control systems, - and issue tracking systems that are managed by, or on behalf of, the - Licensor for the purpose of discussing and improving the Work, but - excluding communication that is conspicuously marked or otherwise - designated in writing by the copyright owner as "Not a Contribution." - - "Contributor" shall mean Licensor and any individual or Legal Entity - on behalf of whom a Contribution has been received by Licensor and - subsequently incorporated within the Work. - - 2. Grant of Copyright License. Subject to the terms and conditions of - this License, each Contributor hereby grants to You a perpetual, - worldwide, non-exclusive, no-charge, royalty-free, irrevocable - copyright license to reproduce, prepare Derivative Works of, - publicly display, publicly perform, sublicense, and distribute the - Work and such Derivative Works in Source or Object form. - - 3. Grant of Patent License. Subject to the terms and conditions of - this License, each Contributor hereby grants to You a perpetual, - worldwide, non-exclusive, no-charge, royalty-free, irrevocable - (except as stated in this section) patent license to make, have made, - use, offer to sell, sell, import, and otherwise transfer the Work, - where such license applies only to those patent claims licensable - by such Contributor that are necessarily infringed by their - Contribution(s) alone or by combination of their Contribution(s) - with the Work to which such Contribution(s) was submitted. If You - institute patent litigation against any entity (including a - cross-claim or counterclaim in a lawsuit) alleging that the Work - or a Contribution incorporated within the Work constitutes direct - or contributory patent infringement, then any patent licenses - granted to You under this License for that Work shall terminate - as of the date such litigation is filed. - - 4. Redistribution. You may reproduce and distribute copies of the - Work or Derivative Works thereof in any medium, with or without - modifications, and in Source or Object form, provided that You - meet the following conditions: - - (a) You must give any other recipients of the Work or - Derivative Works a copy of this License; and - - (b) You must cause any modified files to carry prominent notices - stating that You changed the files; and - - (c) You must retain, in the Source form of any Derivative Works - that You distribute, all copyright, patent, trademark, and - attribution notices from the Source form of the Work, - excluding those notices that do not pertain to any part of - the Derivative Works; and - - (d) If the Work includes a "NOTICE" text file as part of its - distribution, then any Derivative Works that You distribute must - include a readable copy of the attribution notices contained - within such NOTICE file, excluding those notices that do not - pertain to any part of the Derivative Works, in at least one - of the following places: within a NOTICE text file distributed - as part of the Derivative Works; within the Source form or - documentation, if provided along with the Derivative Works; or, - within a display generated by the Derivative Works, if and - wherever such third-party notices normally appear. The contents - of the NOTICE file are for informational purposes only and - do not modify the License. You may add Your own attribution - notices within Derivative Works that You distribute, alongside - or as an addendum to the NOTICE text from the Work, provided - that such additional attribution notices cannot be construed - as modifying the License. - - You may add Your own copyright statement to Your modifications and - may provide additional or different license terms and conditions - for use, reproduction, or distribution of Your modifications, or - for any such Derivative Works as a whole, provided Your use, - reproduction, and distribution of the Work otherwise complies with - the conditions stated in this License. - - 5. Submission of Contributions. Unless You explicitly state otherwise, - any Contribution intentionally submitted for inclusion in the Work - by You to the Licensor shall be under the terms and conditions of - this License, without any additional terms or conditions. - Notwithstanding the above, nothing herein shall supersede or modify - the terms of any separate license agreement you may have executed - with Licensor regarding such Contributions. - - 6. Trademarks. This License does not grant permission to use the trade - names, trademarks, service marks, or product names of the Licensor, - except as required for reasonable and customary use in describing the - origin of the Work and reproducing the content of the NOTICE file. - - 7. Disclaimer of Warranty. Unless required by applicable law or - agreed to in writing, Licensor provides the Work (and each - Contributor provides its Contributions) on an "AS IS" BASIS, - WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or - implied, including, without limitation, any warranties or conditions - of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A - PARTICULAR PURPOSE. You are solely responsible for determining the - appropriateness of using or redistributing the Work and assume any - risks associated with Your exercise of permissions under this License. - - 8. Limitation of Liability. In no event and under no legal theory, - whether in tort (including negligence), contract, or otherwise, - unless required by applicable law (such as deliberate and grossly - negligent acts) or agreed to in writing, shall any Contributor be - liable to You for damages, including any direct, indirect, special, - incidental, or consequential damages of any character arising as a - result of this License or out of the use or inability to use the - Work (including but not limited to damages for loss of goodwill, - work stoppage, computer failure or malfunction, or any and all - other commercial damages or losses), even if such Contributor - has been advised of the possibility of such damages. - - 9. Accepting Warranty or Additional Liability. While redistributing - the Work or Derivative Works thereof, You may choose to offer, - and charge a fee for, acceptance of support, warranty, indemnity, - or other liability obligations and/or rights consistent with this - License. However, in accepting such obligations, You may act only - on Your own behalf and on Your sole responsibility, not on behalf - of any other Contributor, and only if You agree to indemnify, - defend, and hold each Contributor harmless for any liability - incurred by, or claims asserted against, such Contributor by reason - of your accepting any such warranty or additional liability. - - END OF TERMS AND CONDITIONS - - Copyright 2024 Leni Aniva - - Licensed under the Apache License, Version 2.0 (the "License"); - you may not use this file except in compliance with the License. - You may obtain a copy of the License at - - http://www.apache.org/licenses/LICENSE-2.0 - - Unless required by applicable law or agreed to in writing, software - distributed under the License is distributed on an "AS IS" BASIS, - WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - See the License for the specific language governing permissions and - limitations under the License. diff --git a/apn/lean/pantograph-docs/contributing.md b/apn/lean/pantograph-docs/contributing.md deleted file mode 100644 index 6d61d944..00000000 --- a/apn/lean/pantograph-docs/contributing.md +++ /dev/null @@ -1,42 +0,0 @@ -# Contributing - -A Lean development shell is provided in the Nix flake. Nix usage is optional. -Any contribution has to pass the pre-commit hooks, installable using either `prek` or `pre-commit`: -```sh -prek install -pre-commit install --install-hooks -``` - -All commit messages must conform to the Conventional Commits specification. - -## Testing - -The tests are based on `LSpec`. To run tests, use either - -``` sh -nix flake check -``` -or -``` sh -lake test -``` - -You can run an individual test by specifying a prefix - -``` sh -lake test -- Frontend/Collect -``` - -## Formatting - -When writing Lean code, follow the guidelines - -- Functions should be in `camelCase` -- Theorems and tests should be in `snake_case` -- Write the `|` in a pattern-matching `let` on the next line. This is for visual - distinction with long function arguments. -```lean -let .some result := function - | fail "incorrect" -``` -- Each test should be pinpointed and as devolatilized as possible. diff --git a/apn/lean/pantograph-docs/rationale.md b/apn/lean/pantograph-docs/rationale.md deleted file mode 100644 index d44b02a9..00000000 --- a/apn/lean/pantograph-docs/rationale.md +++ /dev/null @@ -1,60 +0,0 @@ -# Design Rationale - -A great problem in machine learning is to use ML agents to automatically prove -mathematical theorems. This sort of proof necessarily involves *search*. -Compatibility for search is the main reason for creating Pantograph. The Lean 4 -LSP interface is not conducive to search. Pantograph is designed with this in -mind. It emphasizes the difference between 3 views of a proof: - -- **Presentation View**: The view of a written, polished proof. e.g. Mathlib and - math papers are almost always written in this form. -- **Search View**: The view of a proof exploration trajectory. This is not - explicitly supported by Lean LSP. -- **Kernel View**: The proof viewed as a set of metavariables. - -Pantograph enables proof agents to operate on the search view. - -## Name - -The name Pantograph is a pun. It means two things -- A pantograph is an instrument for copying down writing. As an agent explores - the vast proof search space, Pantograph records the current state to ensure - the proof is sound. -- A pantograph is also an equipment for an electric train. It supplies power to - a locomotive. In comparison the (relatively) simple Pantograph software powers - theorem proving projects. - -## Caveats and Limitations - -Pantograph does not exactly mimic Lean LSP's behaviour. That would not grant the -flexibility it offers. To support tree search means Pantograph has to act -differently from Lean in some times, but never at the sacrifice of soundness. - -- When Lean LSP says "don't know how to synthesize placeholder", this indicates - the human operator needs to manually move the cursor to the placeholder and - type in the correct expression. This error therefore should not halt the proof - process, and the placeholder should be turned into a goal. -- When Lean LSP says "unresolved goals", that means a proof cannot finish where - it is supposed to finish at the end of a `by` block. Pantograph will raise the - error in this case, since it indicates the termination of a proof search branch. - -Pantograph cannot perform things that are inherently constrained by Lean. These -include: - -- If a tactic loses track of metavariables, it will not be caught until the end - of the proof search. This is a bug in the tactic itself. -- Although a timeout feature exists in Pantograph, it relies on the coöperative - multitasking from the tactic implementation. There is nothing preventing a - buggy tactic from stalling Lean if it does not check for cancellation often. -- For the same reason as above, there is no graceful way to stop a tactic which - leaks infinite memory. Users who wish to have this behaviour should run - Pantograph in a controlled environment with limited allocations. e.g. - Linux control groups. -- Interceptions of parsing errors generally cannot be turned into goals (e.g. - `def mystery : Nat := :=`) due to Lean's parsing system. This question is also - not well-defined. - -## References - -* [Pantograph Paper](https://arxiv.org/abs/2410.16429) - diff --git a/apn/lean/pantograph-docs/repl.md b/apn/lean/pantograph-docs/repl.md deleted file mode 100644 index 0498f5f6..00000000 --- a/apn/lean/pantograph-docs/repl.md +++ /dev/null @@ -1,192 +0,0 @@ -# REPL - -This documentation is about interacting with the REPL. - -## Examples - -After building the `repl`, it will be available in `.lake/build/bin/repl`. -Execute it by either directly referring to its name, or `lake exe repl`. - -``` sh -repl MODULES|LEAN_OPTIONS -``` - -The `repl` executable must be given with a list of modules to import. By default -it will import nothing, not even `Init`. It can also accept lean options of the -form `--key=value` e.g. `--pp.raw=true`. - -Running repl with `--version` shows the version and then exits. - -After it emits the `ready.` signal, `repl` accepts commands as single-line JSON -inputs and outputs either an `Error:` (indicating malformed command) or a JSON -return value indicating the result of a command execution. The command must be -given in one of two formats - -``` -command { ... } -{ "cmd": command, "payload": ... } -``` - -The list of available commands can be found below. An empty command aborts the -REPL. - -Example: (~5k symbols) -``` -$ repl Init -env.catalog {} -env.inspect {"name": "Nat.le_add_left"} -``` - -Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting) - -``` -$ repl Mathlib.Analysis.Seminorm -env.catalog {} -``` - -Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) -to prime the proof - -``` -$ repl Init -goal.start {"expr": "∀ (n m : Nat), n + m = m + n"} -goal.tactic {"stateId": 0, "tactic": "intro n m"} -goal.tactic {"stateId": 1, "tactic": "assumption"} -goal.delete {"stateIds": [0]} -stat {} -goal.tactic {"stateId": 1, "tactic": "rw [Nat.add_comm]"} -stat -``` -where the application of `assumption` should lead to a failure. - -### Project Environment - -To use Pantograph in a project environment, setup the `LEAN_PATH` environment -variable so it contains the library path of lean libraries. The libraries must -be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`, -the environment might be setup like this: - -``` sh -LIB="../lib" -LIB_MATHLIB="$LIB/mathlib4/.lake" -export LEAN_PATH="$LIB_MATHLIB:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib" - -LEAN_PATH=$LEAN_PATH repl $@ -``` -The `$LEAN_PATH` executable of any project can be extracted by -``` sh -lake env printenv LEAN_PATH -``` - -Additional modules cannot be imported after the perennial process starts, either -via `env.load` or the frontend functions. The technical reason for this is when -Lean cannot determine whether an imported module's initializer has run. - -## Commands - -See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. -* `reset`: Delete all cached expressions and proof trees -* `stat`: Display resource usage -* `options.set { key: value, ... }`: Set one or more options. These are not Lean - `CoreM` options; those have to be set via command line arguments.), for - options see below. -* `options.print`: Display the current set of options -* `expr.echo {"expr": , "type": , ["levels": []]}`: Determine the - type of an expression and format it. -* `env.catalog`: Display a list of all safe Lean symbols in the current environment -* `env.inspect {"name": , "value": }`: Show the type and package of a - given symbol; If value flag is set, the value is printed or hidden. By default - only the values of definitions are printed. -* `env.save { "path": }`, `env.load { "path": }`: Save/Load the - current environment to/from a file -* `env.module_read { "module": }`: Reads a list of symbols from a module -* `env.describe {}`: Describes the imports and modules in the current environment -* `env.parse { "input": , "category": }`: Parse a bit - of syntax and returns the parser's terminal position. -* `goal.start {["name": ], ["expr": ], ["levels": []], ["copyFrom": ]}`: - Start a new proof from a given expression or symbol -* `goal.tactic {"stateId": , ["goalId": ], ["autoResume": ], ...}`: - Execute a tactic string on a given goal site. The tactic is supplied as additional - key-value pairs in one of the following formats: - - `{ "tactic": }`: Executes a tactic or a sequence of tactics in the - current mode. - - `{ "mode": }`: Enter a different tactic mode. The permitted values - are `tactic` (default), `conv`, `calc`. In case of `calc`, each step must - be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set - to the previous `rhs`. - - `{ "expr": }`: Assign the given proof term to the current goal - - `{ "have": , "binderName": }`: Execute `have` and creates a branch goal - - `{ "let": , "binderName": }`: Execute `let` and creates a branch goal - - `{ "draft": }`: Draft an expression with `sorry`s, turning them into - goals. Coupling is not allowed. - If the `goals` field does not exist, the tactic execution has failed. Read - `messages` to find the reason. -* `goal.continue {"stateId": , ["branch": ], ["goals": ]}`: - Execute continuation/resumption - - `{ "branch": }`: Continue on branch state. The current state must have no goals. - - `{ "goals": }`: Resume the given goals -* `goal.subsume {"stateId": , "goal": , "candidates": - , ["srcStateId": ]}`: determine if any goal in `candidates` (coming - from either the provided state id or `srcStateId`) subsumes `goal`. It returns - the *subsumptor* (goal providing the solution) and a new state id if the - subsumption is not a cycle, in which case the *subsumend* `goal` is erased. -* `goal.remove {"stateIds": []}"`: Drop the goal states specified in the list -* `goal.print {"stateId": }"`: Print a goal state -* `goal.save { "id": , "path": }`, `goal.load { "path": }`: - Save/Load a goal state to/from a file. The environment is not carried with the - state. The user is responsible to ensure the sender/receiver instances share - the same environment. -* `frontend.process { ["fileName": ,] ["file": ], readHeader: - , inheritEnv: , invocations: , newConstants: }`: - Executes the Lean frontend on a file, collecting the tactic invocations - (`"invocations": output-path`), or new constants (`newConstants`) -* `frontend.distil { "file": , ["binderName": ], "ignoreValues": bool - }`: Extract condensed search targets from a file, where coupled search targets - will be condensed into one. Set `binderName` to override the binder name to - e.g. `f`. Set `ignoreValues` to false to incorporate existing solutions. - - Note that `example`s are not search targets! -* `frontend.track { "src": , "dst": }`: Check if one file conforms to - another. The declarations in `src` could have `sorry`s and the declarations in - `dst` would fill them. -* [Experimental] `frontend.refactor { "file": , "coreOptions": - [["="]] }`: Group dependent `sorry`s into one single `sorry`. - Currently only flat dependencies are supported (i.e. an object with a list of - properties). - -## Options - -The full list of options can be found in `Pantograph/Protocol.lean`. Particularly: -- `automaticMode` (default on): Goals will not become dormant when this is - turned on. By default it is turned on, with all goals automatically resuming. - This makes Pantograph act like a gym, with no resumption necessary to manage - your goals. -- `timeout` (default 0): Set `timeout` to a non-zero number to specify timeout - (milliseconds) for all `CoreM` and frontend operations. - -## Errors - -When an error pertaining to the execution of a command happens, the returning JSON structure is - -``` json -{ "error": "type", "desc": "description" } -``` -Common error forms: -* `command`: Indicates malformed command structure which results from either - invalid command or a malformed JSON structure that cannot be fed to an - individual command. -* `index`: Indicates an invariant maintained by the output of one command and - input of another is broken. For example, attempting to query a symbol not - existing in the library or indexing into a non-existent proof state. -* `parse`: Indicates parsing errors -* `elab`: Indicates elaboration errors -* `frontend`: Indicates whole-file parsing and elaboration errors -* `io`: Generic IO error -* `command`: The command's argument is malformed - -## Troubleshooting - -If lean encounters stack overflow problems when printing catalog, execute this before running lean: -```sh -ulimit -s unlimited -``` diff --git a/apn/lean/pypantograph-docs/LICENSE b/apn/lean/pypantograph-docs/LICENSE deleted file mode 100644 index 34f63a39..00000000 --- a/apn/lean/pypantograph-docs/LICENSE +++ /dev/null @@ -1,190 +0,0 @@ - Apache License - Version 2.0, January 2004 - http://www.apache.org/licenses/ - - TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION - - 1. Definitions. - - "License" shall mean the terms and conditions for use, reproduction, - and distribution as defined by Sections 1 through 9 of this document. - - "Licensor" shall mean the copyright owner or entity authorized by - the copyright owner that is granting the License. - - "Legal Entity" shall mean the union of the acting entity and all - other entities that control, are controlled by, or are under common - control with that entity. For the purposes of this definition, - "control" means (i) the power, direct or indirect, to cause the - direction or management of such entity, whether by contract or - otherwise, or (ii) ownership of fifty percent (50%) or more of the - outstanding shares, or (iii) beneficial ownership of such entity. - - "You" (or "Your") shall mean an individual or Legal Entity - exercising permissions granted by this License. - - "Source" form shall mean the preferred form for making modifications, - including but not limited to software source code, documentation - source, and configuration files. - - "Object" form shall mean any form resulting from mechanical - transformation or translation of a Source form, including but - not limited to compiled object code, generated documentation, - and conversions to other media types. - - "Work" shall mean the work of authorship, whether in Source or - Object form, made available under the License, as indicated by a - copyright notice that is included in or attached to the work - (an example is provided in the Appendix below). - - "Derivative Works" shall mean any work, whether in Source or Object - form, that is based on (or derived from) the Work and for which the - editorial revisions, annotations, elaborations, or other modifications - represent, as a whole, an original work of authorship. For the purposes - of this License, Derivative Works shall not include works that remain - separable from, or merely link (or bind by name) to the interfaces of, - the Work and Derivative Works thereof. - - "Contribution" shall mean any work of authorship, including - the original version of the Work and any modifications or additions - to that Work or Derivative Works thereof, that is intentionally - submitted to Licensor for inclusion in the Work by the copyright owner - or by an individual or Legal Entity authorized to submit on behalf of - the copyright owner. For the purposes of this definition, "submitted" - means any form of electronic, verbal, or written communication sent - to the Licensor or its representatives, including but not limited to - communication on electronic mailing lists, source code control systems, - and issue tracking systems that are managed by, or on behalf of, the - Licensor for the purpose of discussing and improving the Work, but - excluding communication that is conspicuously marked or otherwise - designated in writing by the copyright owner as "Not a Contribution." - - "Contributor" shall mean Licensor and any individual or Legal Entity - on behalf of whom a Contribution has been received by Licensor and - subsequently incorporated within the Work. - - 2. Grant of Copyright License. Subject to the terms and conditions of - this License, each Contributor hereby grants to You a perpetual, - worldwide, non-exclusive, no-charge, royalty-free, irrevocable - copyright license to reproduce, prepare Derivative Works of, - publicly display, publicly perform, sublicense, and distribute the - Work and such Derivative Works in Source or Object form. - - 3. Grant of Patent License. Subject to the terms and conditions of - this License, each Contributor hereby grants to You a perpetual, - worldwide, non-exclusive, no-charge, royalty-free, irrevocable - (except as stated in this section) patent license to make, have made, - use, offer to sell, sell, import, and otherwise transfer the Work, - where such license applies only to those patent claims licensable - by such Contributor that are necessarily infringed by their - Contribution(s) alone or by combination of their Contribution(s) - with the Work to which such Contribution(s) was submitted. If You - institute patent litigation against any entity (including a - cross-claim or counterclaim in a lawsuit) alleging that the Work - or a Contribution incorporated within the Work constitutes direct - or contributory patent infringement, then any patent licenses - granted to You under this License for that Work shall terminate - as of the date such litigation is filed. - - 4. Redistribution. You may reproduce and distribute copies of the - Work or Derivative Works thereof in any medium, with or without - modifications, and in Source or Object form, provided that You - meet the following conditions: - - (a) You must give any other recipients of the Work or - Derivative Works a copy of this License; and - - (b) You must cause any modified files to carry prominent notices - stating that You changed the files; and - - (c) You must retain, in the Source form of any Derivative Works - that You distribute, all copyright, patent, trademark, and - attribution notices from the Source form of the Work, - excluding those notices that do not pertain to any part of - the Derivative Works; and - - (d) If the Work includes a "NOTICE" text file as part of its - distribution, then any Derivative Works that You distribute must - include a readable copy of the attribution notices contained - within such NOTICE file, excluding those notices that do not - pertain to any part of the Derivative Works, in at least one - of the following places: within a NOTICE text file distributed - as part of the Derivative Works; within the Source form or - documentation, if provided along with the Derivative Works; or, - within a display generated by the Derivative Works, if and - wherever such third-party notices normally appear. The contents - of the NOTICE file are for informational purposes only and - do not modify the License. You may add Your own attribution - notices within Derivative Works that You distribute, alongside - or as an addendum to the NOTICE text from the Work, provided - that such additional attribution notices cannot be construed - as modifying the License. - - You may add Your own copyright statement to Your modifications and - may provide additional or different license terms and conditions - for use, reproduction, or distribution of Your modifications, or - for any such Derivative Works as a whole, provided Your use, - reproduction, and distribution of the Work otherwise complies with - the conditions stated in this License. - - 5. Submission of Contributions. Unless You explicitly state otherwise, - any Contribution intentionally submitted for inclusion in the Work - by You to the Licensor shall be under the terms and conditions of - this License, without any additional terms or conditions. - Notwithstanding the above, nothing herein shall supersede or modify - the terms of any separate license agreement you may have executed - with Licensor regarding such Contributions. - - 6. Trademarks. This License does not grant permission to use the trade - names, trademarks, service marks, or product names of the Licensor, - except as required for reasonable and customary use in describing the - origin of the Work and reproducing the content of the NOTICE file. - - 7. Disclaimer of Warranty. Unless required by applicable law or - agreed to in writing, Licensor provides the Work (and each - Contributor provides its Contributions) on an "AS IS" BASIS, - WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or - implied, including, without limitation, any warranties or conditions - of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A - PARTICULAR PURPOSE. You are solely responsible for determining the - appropriateness of using or redistributing the Work and assume any - risks associated with Your exercise of permissions under this License. - - 8. Limitation of Liability. In no event and under no legal theory, - whether in tort (including negligence), contract, or otherwise, - unless required by applicable law (such as deliberate and grossly - negligent acts) or agreed to in writing, shall any Contributor be - liable to You for damages, including any direct, indirect, special, - incidental, or consequential damages of any character arising as a - result of this License or out of the use or inability to use the - Work (including but not limited to damages for loss of goodwill, - work stoppage, computer failure or malfunction, or any and all - other commercial damages or losses), even if such Contributor - has been advised of the possibility of such damages. - - 9. Accepting Warranty or Additional Liability. While redistributing - the Work or Derivative Works thereof, You may choose to offer, - and charge a fee for, acceptance of support, warranty, indemnity, - or other liability obligations and/or rights consistent with this - License. However, in accepting such obligations, You may act only - on Your own behalf and on Your sole responsibility, not on behalf - of any other Contributor, and only if You agree to indemnify, - defend, and hold each Contributor harmless for any liability - incurred by, or claims asserted against, such Contributor by reason - of your accepting any such warranty or additional liability. - - END OF TERMS AND CONDITIONS - - Copyright 2024 Leni Aniva - - Licensed under the Apache License, Version 2.0 (the "License"); - you may not use this file except in compliance with the License. - You may obtain a copy of the License at - - http://www.apache.org/licenses/LICENSE-2.0 - - Unless required by applicable law or agreed to in writing, software - distributed under the License is distributed on an "AS IS" BASIS, - WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - See the License for the specific language governing permissions and - limitations under the License. diff --git a/apn/lean/pypantograph-docs/agent-search.md b/apn/lean/pypantograph-docs/agent-search.md deleted file mode 100644 index e640b4a4..00000000 --- a/apn/lean/pypantograph-docs/agent-search.md +++ /dev/null @@ -1,81 +0,0 @@ - - -# Search - -Pantograph supports basic proof search. In this case, Pantograph treats goals as nodes on an and-or tree. The user supplies an agent which should provide two functions: - -1. *Tactic*: Which tactic should be used on a goal? -2. *Guidance*: What is the search priority on a goal? - -The user agent should inherit from `pantograph.search.Agent`. Here is a brute force agent example: - -```python -from typing import Optional -import collections -from pantograph import Server -from pantograph.search import Agent -from pantograph.expr import GoalState, Tactic -``` - -```python -class DumbAgent(Agent): - - def __init__(self): - super().__init__() - - self.goal_tactic_id_map = collections.defaultdict(lambda : 0) - self.intros = [ - "intro", - ] - self.tactics = [ - "intro h", - "cases h", - "apply Or.inl", - "apply Or.inr", - ] - self.no_space_tactics = [ - "assumption", - ] - - def next_tactic( - self, - state: GoalState, - goal_id: int, - ) -> Optional[Tactic]: - key = (state.state_id, goal_id) - i = self.goal_tactic_id_map[key] - - target = state.goals[goal_id].target - if target.startswith('∀'): - tactics = self.intros - elif ' ' in target: - tactics = self.tactics - else: - tactics = self.no_space_tactics - - if i >= len(tactics): - return None - - self.goal_tactic_id_map[key] = i + 1 - return tactics[i] -``` - -Execute the search with `agent.search`. - -```python -server = Server() -agent = DumbAgent() -goal_state = server.goal_start("∀ (p q: Prop), Or p q -> Or q p") -agent.search(server=server, goal_state=goal_state, verbose=False) -``` - -Output: -``` -SearchResult(n_goals_root=1, duration=0.7717759609222412, success=True, steps=16) -``` - -## Automatic and Manual Modes - -The agent chooses one goal and executes a tactic on this goal. What happens to the other goals that are not chosen? By default, the server runs in automatic mode. In automatic mode, all other goals are automatically inherited by a child state, so a user agent could declare a proof finished when there are no more goals remaining in the current goal state. - -Some users may wish to handle sibling goals manually. For example, Aesop's treatment of metavariable coupling is not automatic. To do this, pass the flag `options={ "automaticMode" : False }` to the `Server` constructor. diff --git a/apn/lean/pypantograph-docs/examples/README.md b/apn/lean/pypantograph-docs/examples/README.md deleted file mode 100644 index f03db11e..00000000 --- a/apn/lean/pypantograph-docs/examples/README.md +++ /dev/null @@ -1,24 +0,0 @@ -# Examples - -This example showcases how to bind library dependencies and execute the `Aesop` -tactic in Lean. First build the example project: -``` sh -pushd Example -lake build -popd -``` -This would generate compiled `.olean` files. Then run one of the examples from the -project root: -``` sh -poetry run examples/aesop.py -poetry run examples/sketch.py -``` - -Warning: If you make modifications to any Lean files, you must re-run `lake -build`! Moreover, the version of the Lean used in the example folder (including -dependencies in `lakefile.lean` and `lean-toolchain`) **must match exactly** -with the version in `src/`! - -* `aesop.py`: Example of how to use the `aesop` tactic -* `sketch.py`: Example of loading a sketch - diff --git a/apn/lean/pypantograph-docs/examples/aesop.py b/apn/lean/pypantograph-docs/examples/aesop.py deleted file mode 100644 index b502ddfc..00000000 --- a/apn/lean/pypantograph-docs/examples/aesop.py +++ /dev/null @@ -1,14 +0,0 @@ -#!/usr/bin/env python3 - -from pathlib import Path -from pantograph.server import Server - -# This example shows how to use project dependencies - -if __name__ == '__main__': - project_path = Path(__file__).parent.resolve() / 'Example' - print(f"$PWD: {project_path}") - server = Server(imports=['Example'], project_path=project_path) - state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p") - state1 = server.goal_tactic(state0, tactic="aesop") - assert state1.is_solved diff --git a/apn/lean/pypantograph-docs/examples/branch-sorry.py b/apn/lean/pypantograph-docs/examples/branch-sorry.py deleted file mode 100644 index 0187c183..00000000 --- a/apn/lean/pypantograph-docs/examples/branch-sorry.py +++ /dev/null @@ -1,13 +0,0 @@ -#!/usr/bin/env python3 - -from pantograph.server import Server -from pantograph.expr import TacticHave - -# This example shows what happens when a tactic generates a sorry. -if __name__ == '__main__': - server = Server(imports=['Init']) - state0 = server.goal_start("1 = 0") - state1 = server.goal_tactic(state0, tactic=TacticHave("1 = 0")) - print(state1) - state1b = server.goal_tactic(state1, tactic="apply?") - print(state1b) diff --git a/apn/lean/pypantograph-docs/examples/simple.py b/apn/lean/pypantograph-docs/examples/simple.py deleted file mode 100644 index cbd5328b..00000000 --- a/apn/lean/pypantograph-docs/examples/simple.py +++ /dev/null @@ -1,7 +0,0 @@ -from pantograph.server import Server - -if __name__ == '__main__': - server = Server(imports=['Init']) - state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p") - state1 = server.goal_tactic(state0, tactic="intro") - print(state1) diff --git a/apn/lean/pypantograph-docs/examples/sketch.py b/apn/lean/pypantograph-docs/examples/sketch.py deleted file mode 100644 index eeaa0a4c..00000000 --- a/apn/lean/pypantograph-docs/examples/sketch.py +++ /dev/null @@ -1,41 +0,0 @@ -#!/usr/bin/env python3 - -from pantograph.server import Server -from pantograph.expr import TacticDraft - -root = """ -theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := sorry -""" - -sketch = """ -by - -- Consider some n and m in Nats. - intros n m - -- Perform induction on n. - induction n with - | zero => - sorry - | succ n ih => - -- Inductive step: Assume n + m = m + n, we need to show succ n + m = m + succ n. - -- By the inductive hypothesis, we have n + m = m + n. - have h_inductive: n + m = m + n := sorry - -- 1. Note we start with: Nat.succ n + m = m + Nat.succ n, so, pull the succ out from m + Nat.succ n on the right side from the addition using addition facts Nat.add_succ. - have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := sorry - -- 2. then to flip m + S n to something like S (n + m) we need to use the IH. - have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := sorry - -- 3. Now the n & m are on the correct sides Nat.succ n + m = Nat.succ (n + m), so let's use the def of addition to pull out the succ from the addition on the left using Nat.succ_add. - have h_pull_succ_out_from_left: Nat.succ n + m = Nat.succ (n + m) := sorry - -- Combine facts to close goal - sorry -""" - -if __name__ == '__main__': - server = Server() - unit, = server.load_sorry(root) - print(unit.goal_state) - - # Send the draft payload using `TacticDraft` - state1 = server.goal_tactic( - unit.goal_state, - tactic=TacticDraft(sketch)) - print(state1) diff --git a/apn/lean/pypantograph-docs/frontend.md b/apn/lean/pypantograph-docs/frontend.md deleted file mode 100644 index 0d8f75ee..00000000 --- a/apn/lean/pypantograph-docs/frontend.md +++ /dev/null @@ -1,234 +0,0 @@ - - -# Data Extraction - -```python -import os -from pathlib import Path -from pantograph.server import Server -``` - -## Tactic Invocation - -Pantograph can extract tactic invocation data from a Lean file. A **tactic -invocation** is a tuple containing the before and after goal states, and the -tactic which converts the "before" state to the "after" state. - -To extract tactic invocation data, use `server.tactic_invocations(file_name)` -and supply the file name of the input Lean file. - -```python -project_path = Path(os.getcwd()).parent.resolve() / 'examples/Example' -print(f"$PWD: {project_path}") -server = await Server.create(imports=['Example'], project_path=project_path) -units = await server.tactic_invocations_async(project_path / "Example.lean") -``` - -Output: -``` -$PWD: /Users/aniva/Projects/matp/PyPantograph/examples/Example -``` - -The function returns a list of `CompilationUnit` objects, corresponding to each compilation unit in the input Lean file. For performance reasons only the text boundaries are loaded into `CompilationUnit`s. - -```python -with open(project_path / "Example.lean", 'rb') as f: - content = f.read() - for i, unit in enumerate(units): - print(f"#{i}: [{unit.i_begin},{unit.i_end}]") - unit_text = content[unit.i_begin:unit.i_end].decode('utf-8') - print(unit_text) -``` - -Output: -``` -#0: [14,85] -/-- Ensure that Aesop is running -/ -example : α → α := - by aesop - - -#1: [85,254] -example : ∀ (p q: Prop), p ∨ q → q ∨ p := by - intro p q h - -- Here are some comments - cases h - . apply Or.inr - assumption - . apply Or.inl - assumption -``` - -Each `CompilationUnit` includes a list of `TacticInvocation`s, which contains the `.before` (corresponding to the state before the tactic), `.after` (corresponding to the state after the tactic), and `.tactic` (tactic executed) fields. - -```python -for i in units[0].invocations: - print(f"[Before]\n{i.before}") - print(f"[Tactic]\n{i.tactic} (using {i.used_constants})") - print(f"[After]\n{i.after}") -``` - -Output: -``` -[Before] -α : Sort ?u.7 -⊢ α → α -[Tactic] -aesop (using []) -[After] -``` - -```python -for i in units[1].invocations: - print(f"[Before]\n{i.before}") - print(f"[Tactic]\n{i.tactic} (using {i.used_constants})") - print(f"[After]\n{i.after}") -``` - -Output: -``` -[Before] -⊢ ∀ (p q : Prop), p ∨ q → q ∨ p -[Tactic] -intro p q h (using []) -[After] -p q : Prop -h : p ∨ q -⊢ q ∨ p -[Before] -p q : Prop -h : p ∨ q -⊢ q ∨ p -[Tactic] -cases h (using ['Eq.refl', 'Or']) -[After] -case inl -p q : Prop -h✝ : p -⊢ q ∨ p -case inr -p q : Prop -h✝ : q -⊢ q ∨ p -[Before] -case inl -p q : Prop -h✝ : p -⊢ q ∨ p -[Tactic] -apply Or.inr (using ['Or.inr']) -[After] -case inl.h -p q : Prop -h✝ : p -⊢ p -[Before] -case inl.h -p q : Prop -h✝ : p -⊢ p -[Tactic] -assumption (using []) -[After] - -[Before] -case inr -p q : Prop -h✝ : q -⊢ q ∨ p -[Tactic] -apply Or.inl (using ['Or.inl']) -[After] -case inr.h -p q : Prop -h✝ : q -⊢ q -[Before] -case inr.h -p q : Prop -h✝ : q -⊢ q -[Tactic] -assumption (using []) -[After] -``` - -## Check Compilation - -Use `check_compile` to check if some Lean code compiles. - -Keep in mind that Lean compilation can execute arbitrary code. - -```python -server = await Server.create() -code = """ -example : 1 + 1 = 2 := by rfl -""" -await server.check_compile_async(code) -``` - -Output: -``` -[CompilationUnit(i_begin=0, i_end=31, messages=[], invocations=None, goal_state=None, goal_src_boundaries=None, new_constants=None)] -``` - -If there are no error messages, it means the unit compiles. - -## Loading Definitions - -Pantograph keeps track of a global environment. `Server.load_definitions` adds new definitions to the environment. - -```python -code = """ -def mystery : Nat -> Nat := fun x => x + 1 -""" -await server.load_definitions_async(code) -await server.env_inspect_async("mystery") -``` - -Output: -``` -{'type': {'pp': 'Nat → Nat'}, - 'sourceStart': {'line': 2, 'column': 0}, - 'sourceEnd': {'line': 2, 'column': 42}, - 'isUnsafe': False} -``` - -## Track Checking - -We can check if one file conforms to the definition and theorems of another. If the result object has no `failure`s or error messages, the check has passed. - -```python -src = """ -def f : Nat -> Nat := sorry -theorem property (n : Nat) : f n = n + 1 := sorry -""" -dst = """ -def f (x : Nat) := x + 1 -theorem property (n : Nat) : f n = n + 1 := rfl -""" -await server.check_track_async(src, dst) -``` - -Output: -``` -CheckTrackResult(src_messages=[], dst_messages=[], failure=None) -``` - -```python -src = """ -def f : Nat -> Nat := sorry -theorem property (n : Nat) : f n = n + 1 := sorry -""" -# Tampering! -dst = """ -def f (x : Nat) := x + 1 -theorem property (n : Nat) : 0 = 0 := rfl -""" -await server.check_track_async(src, dst) -``` - -Output: -``` -CheckTrackResult(src_messages=[], dst_messages=[], failure='Type clash of property') -``` diff --git a/apn/lean/pypantograph-docs/goal.md b/apn/lean/pypantograph-docs/goal.md deleted file mode 100644 index 489d8f05..00000000 --- a/apn/lean/pypantograph-docs/goal.md +++ /dev/null @@ -1,370 +0,0 @@ - - -# Goals and Tactics - -Executing tactics in Pantograph is simple. To start a proof, call the -`Server.goal_start` function and supply an expression. - -```python -from pantograph import Server -from pantograph.expr import Site, TacticHave, TacticExpr, TacticMode -``` - -```python -server = await Server.create() -state0 = await server.goal_start_async("forall (p q: Prop), Or p q -> Or q p") -``` - -This creates a *goal state*, which consists of some goals. In this -case since it is the beginning of a state, it has only one goal. - -```python -print(state0) -``` - -Output: -``` - -⊢ forall (p q: Prop), Or p q -> Or q p -``` - -To execute a tactic on a goal state, use `Server.goal_tactic`. This function -takes a state, a tactic, and an optional site (see below). Most Lean tactics are strings. - -```python -state1 = await server.goal_tactic_async(state0, "intro a") -print(state1) -``` - -Output: -``` -a : Prop -⊢ ∀ (q : Prop), a ∨ q → q ∨ a -``` - -Executing a tactic produces a new goal state. If this goal state has no goals, -the proof is complete. You can recover the usual form of a goal with `str()` - -```python -print(state1.goals[0]) -``` - -Output: -``` -a : Prop -⊢ ∀ (q : Prop), a ∨ q → q ∨ a -``` - -Starting in v0.3.5, you can run multiple tactics in one shot. Use `?_` to mark goals to be solved later. - -```python -state2 = await server.goal_tactic_async(state0, "intro p q\nintro h\ncases h") -print(state2) -``` - -Output: -``` -inl -p : Prop -q : Prop -h✝ : p -⊢ q ∨ p -inr -p : Prop -q : Prop -h✝ : q -⊢ q ∨ p -``` - -```python -state2 = await server.goal_tactic_async(state0, "intro p q h\nhave random : 1 + 1 = 2 := ?_\ncases h") -print(state2) -``` - -Output: -``` -refine_2.inl -p : Prop -q : Prop -random : 1 + 1 = 2 -h✝ : p -⊢ q ∨ p -refine_2.inr -p : Prop -q : Prop -random : 1 + 1 = 2 -h✝ : q -⊢ q ∨ p -refine_1 -p : Prop -q : Prop -h : p ∨ q -⊢ 1 + 1 = 2 -``` - -## Error Handling and GC - -When a tactic fails, it throws an exception (`TacticFailure`) which contains a list of either `str`s or `Message` objects in `e.args[0]`. - -```python -from pantograph.message import TacticFailure -try: - state2 = await server.goal_tactic_async(state1, "assumption") - print("Should not reach this") -except TacticFailure as e: - print(e) - for msg in e.args[0]: - print(msg) -``` - -Output: -``` -[Message(data="tactic 'assumption' failed\na : Prop\n⊢ ∀ (q : Prop), a ∨ q → q ∨ a", pos=Position(line=0, column=0), pos_end=None, severity=, kind=None)] -0:0: error: tactic 'assumption' failed -a : Prop -⊢ ∀ (q : Prop), a ∨ q → q ∨ a -``` - -A state with no goals is considered solved - -```python -state0 = await server.goal_start_async("forall (p : Prop), p -> p") -state1 = await server.goal_tactic_async(state0, "intro") -state2 = await server.goal_tactic_async(state1, "intro h") -state3 = await server.goal_tactic_async(state2, "exact h") -state3 -``` - -Output: -``` -GoalState(#7, goals=[], _sentinel=#4 -``` - -Execute `server.gc()` once in a while to delete unused goals. - -```python -await server.gc_async() -``` - -## Special Tactics - -Lean has special provisions for some tactics. This includes `have`, `let`, -`calc`. To execute one of these tactics, create a `TacticHave`, `TacticLet`, -instance and feed it into `server.goal_tactic`. - -Technically speaking `have` and `let` are not tactics in Lean, so their execution requires special attention. In v0.3.5, they can be run under the normal tactic function as well (see above). - -```python -state0 = await server.goal_start_async("1 + 1 = 2") -state1 = await server.goal_tactic_async(state0, TacticHave(branch="2 = 1 + 1", binder_name="h")) -print(state1) -``` - -Output: -``` - -⊢ 2 = 1 + 1 -h : 2 = 1 + 1 -⊢ 1 + 1 = 2 -``` - -The `TacticExpr` "tactic" parses an expression and assigns it to the current -goal. This leverages Lean's type unification system and is as expressive as -Lean expressions. Many proofs in Mathlib4 are written in a mixture of expression -and tactic forms. - -```python -state0 = await server.goal_start_async("forall (p : Prop), p -> p") -state1 = await server.goal_tactic_async(state0, "intro p") -state2 = await server.goal_tactic_async(state1, TacticExpr("fun h => h")) -print(state2) -``` - -Output: -``` - -``` - -### Drafting - -Pantograph supports drafting (technically the sketch step) from -[Draft-Sketch-Prove](https://github.com/wellecks/ntptutorial/tree/main/partII_dsp). -Pantograph's drafting feature is more powerful. At any place in the proof, you -can replace an expression with `sorry`, and the `sorry` will become a goal. Any type errors will also become goals. In order to detect whether type errors have occurred, the user can look at the messages from each compilation unit. - -At this point we must introduce the idea of compilation units. Each Lean -definition, theorem, constant, etc., is a *compilation unit*. When Pantograph -extracts data from Lean source code, it sections the data into these compilation -units. - -For example, consider this sketch produced by a language model prover: -```lean -by - intros n m - induction n with - | zero => - have h_base: 0 + m = m := sorry - have h_symm: m + 0 = m := sorry - sorry - | succ n ih => - have h_inductive: n + m = m + n := sorry - have h_pull_succ_out_from_right: m + Nat.succ n = Nat.succ (m + n) := sorry - have h_flip_n_plus_m: Nat.succ (n + m) = Nat.succ (m + n) := sorry - have h_pull_succ_out_from_left: Nat.succ n + m = Nat.succ (n + m) := sorry - sorry -``` -There are some `sorry`s that we want to solve automatically with hammer tactics. We can do this by drafting. - -Pantograph can also load `sorry`s from a code snippet, which provides an alternative way for proof initiation. Warning: `load_sorry` does not work with `example` declarations. - -```python -sketch = """ -theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := sorry -""" -unit, = await server.load_sorry_async(sketch) -print(unit.goal_state) -``` - -Output: -``` - -⊢ ∀ (n m : Nat), n + m = m + n -``` - -```python -step = """ -by - -- Consider some n and m in Nats. - intros n m - -- Perform induction on n. - induction n with - | zero => - -- Base case: When n = 0, we need to show 0 + m = m + 0. - -- We have the fact 0 + m = m by the definition of addition. - have h_base: 0 + m = m := sorry - -- We also have the fact m + 0 = m by the definition of addition. - have h_symm: m + 0 = m := sorry - -- Combine facts to close goal - sorry - | succ n ih => - sorry -""" -from pantograph.expr import TacticDraft -tactic = TacticDraft(step) -state1 = await server.goal_tactic_async(unit.goal_state, tactic) -print(state1) -``` - -Output: -``` -n : Nat -m : Nat -⊢ 0 + m = m -n : Nat -m : Nat -h_base : 0 + m = m -⊢ m + 0 = m -n : Nat -m : Nat -h_base : 0 + m = m -h_symm : m + 0 = m -⊢ 0 + m = m + 0 -n✝ : Nat -m : Nat -n : Nat -ih : n + m = m + n -⊢ n + 1 + m = m + (n + 1) -``` - -### Search Target Distillation - -Sometimes, we want to search for an object (witness) along with proofs (companions) of properties about the object. This problem is known as **companion generation**. In Pantograph, `load_sorry` will automatically pair companions to create coupled search targets. Note that this is only available for flat dependency structures, where one object has a list of properties. - -```python -sketch = """ -def f : Nat -> Nat := sorry -theorem property (n : Nat) : f n = n + 1 := sorry -""" -target, = await server.load_sorry_async(sketch, ignore_values=True) -print(target.goal_state) -``` - -Output: -``` - -⊢ { f // ∀ (n : Nat), f n = n + 1 } -``` - -## Sites - -The optional `site` argument to `goal_tactic` controls the area of effect of a tactic. Site controls what the tactic sees when it asks Lean for the current goal. Most tactics only act on a single goal, but tactics acting on multiple goals are plausible as well. - -The `auto_resume` field defaults to the server option's `automaticMode` (which defaults to `True`). When this field is true, Pantograph will not deliberately hide other goals away from the tactic. This is the usual modus operandi of tactic proofs in Lean. When `auto_resume` is set to `False`, Pantograph will set other goals to dormant. This can be useful in limiting the area of effect of a tactic. However, dormanting a goal comes with the extra burden that it has to be activated ("resume") later, via `goal_resume`. - -```python -state = await server.goal_start_async("forall (p : Prop), p -> And p (Or p p)") -state = await server.goal_tactic_async(state, "intro p h") -state = await server.goal_tactic_async(state, "apply And.intro") -print(state) -``` - -Output: -``` -left -p : Prop -h : p -⊢ p -right -p : Prop -h : p -⊢ p ∨ p -``` - -In the example below, we set `auto_resume` to `False`, and the sibling goal is dormanted. - -```python -state1 = await server.goal_tactic_async(state, "exact h", site=Site(goal_id=0, auto_resume=False)) -print(state1) -``` - -Output: -``` - -``` - -In the example below, we preferentially operate on the second goal. Note that the first goal is still here. - -```python -state2 = await server.goal_tactic_async(state, "apply Or.inl", site=Site(goal_id=1)) -print(state2) -``` - -Output: -``` -right.h -p : Prop -h : p -⊢ p -left -p : Prop -h : p -⊢ p -``` - -## Tactic Modes - -Pantograph has special provisions for handling `conv` and `calc` tactics. The commonality of these tactics is incremental feedback: The tactic can run half way and produce some goal. Pantograph supports this via tactic modes. Every goal carries around with it a `TacticMode`, and the user is free to switch between modes. By default, the mode is `TacticMode.TACTIC`. - -```python -state = await server.goal_start_async("∀ (a b: Nat), (b = 2) -> 1 + a + 1 = a + b") - -state = await server.goal_tactic_async(state, "intro a b h") -state = await server.goal_tactic_async(state, TacticMode.CALC) -state = await server.goal_tactic_async(state, "1 + a + 1 = a + 1 + 1") -state -``` - -Output: -``` -GoalState(#24, goals=[Goal(id='_uniq.381', variables=[Variable(t='Nat', v=None, name='a'), Variable(t='Nat', v=None, name='b'), Variable(t='b = 2', v=None, name='h')], target='1 + a + 1 = a + 1 + 1', sibling_dep=None, name='calc', mode=), Goal(id='_uniq.400', variables=[Variable(t='Nat', v=None, name='a'), Variable(t='Nat', v=None, name='b'), Variable(t='b = 2', v=None, name='h')], target='a + 1 + 1 = a + b', sibling_dep=None, name=None, mode=)], _sentinel=#14 -``` diff --git a/apn/lean/pypantograph-docs/intro.md b/apn/lean/pypantograph-docs/intro.md deleted file mode 100644 index 0d257bcc..00000000 --- a/apn/lean/pypantograph-docs/intro.md +++ /dev/null @@ -1,79 +0,0 @@ -# Introduction - -This is Pantograph, an machine-to-machine interaction interface for Lean 4. -Its main purpose is to train and evaluate theorem proving agents. The main -features of Pantograph are: - -1. Writing mixed expression and tactic style proofs -2. Exposing the minimum amount of information for a search agent -3. Handling of metavariable coupling -4. Reading/Adding symbols from the environment -5. Extraction of tactic training data -6. Drafting incomplete proofs - -## Name - -The name Pantograph is a pun. It means two things -- A pantograph is an instrument for copying down writing. As an agent explores - the vast proof search space, Pantograph records the current state to ensure - the proof is sound. -- A pantograph is also an equipment for an electric train. It supplies power to - a locomotive. In comparison the (relatively) simple Pantograph software powers - theorem proving projects. - -## Design Rationale - -The Lean 4 interface is not conducive to search. Readers familiar with Coq may -know that the Coq Serapi was superseded by CoqLSP. In the opinion of the -authors, this is a mistake. An interface conducive for human operators to write -proofs is often not an interface conductive to machine learning agents for -searching. - -All of Pantograph's business logic is written in Lean, allowing coupling between -the data extraction and proof search components. - -## Caveats and Limitations - -Pantograph does not exactly mimic Lean LSP's behaviour. That would not grant the -flexibility it offers. To support tree search means Pantograph has to act -differently from Lean in some times, but never at the sacrifice of soundness. - -- When Lean LSP says "don't know how to synthesize placeholder", this indicates - the human operator needs to manually move the cursor to the placeholder and - type in the correct expression. This error therefore should not halt the proof - process, and the placeholder should be turned into a goal. -- When Lean LSP says "unresolved goals", that means a proof cannot finish where - it is supposed to finish at the end of a `by` block. Pantograph will raise the - error in this case, since it indicates the termination of a proof search branch. - -Pantograph cannot perform things that are inherently constrained by Lean. These -include: - -- If a tactic loses track of metavariables, it will not be caught until the end - of the proof search. This is a bug in the tactic itself. -- Lean's concurrency model is coöperative, which means a tactic is responsible - for checking a cancellation flag if it runs for a long time. Pantograph's - built-in timeout feature requires such behaviour. A tactic which hangs without - checking the flag cannot be timeouted. -- Interceptions of parsing errors generally cannot be turned into goals (e.g. - `def mystery : Nat := :=`) due to Lean's parsing system. - -Each Pantograph version is anchored to a Lean version specified in -`src/lean-toolchain`. Features can be backported to older Lean versions upon -request. - -## Referencing - -[Paper Link](https://arxiv.org/abs/2410.16429) - -```bib -@misc{pantograph, - title={Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4}, - author={Leni Aniva and Chuyue Sun and Brando Miranda and Clark Barrett and Sanmi Koyejo}, - year={2024}, - eprint={2410.16429}, - archivePrefix={arXiv}, - primaryClass={cs.LO}, - url={https://arxiv.org/abs/2410.16429}, -} -``` diff --git a/apn/lean/pypantograph-docs/setup.md b/apn/lean/pypantograph-docs/setup.md deleted file mode 100644 index fa194fcc..00000000 --- a/apn/lean/pypantograph-docs/setup.md +++ /dev/null @@ -1,85 +0,0 @@ -# Setup - -1. Install `uv` -2. Clone this repository with submodules: -```sh -git clone --recurse-submodules -``` -3. Install `elan` and `lake`: See [Lean Manual](https://docs.lean-lang.org/lean4/doc/setup.html) -4. Execute -```sh -cd -uv sync -``` - -`uv build` builds a wheel of Pantograph in `dist` which can then be installed. For -example, a downstream project could have this line in its `pyproject.toml` - -```toml -pantograph = { file = "path/to/wheel/dist/pantograph-0.3.0-cp312-cp312-manylinux_2_40_x86_64.whl" } -``` - -All interactions with Lean pass through the `Server` class. Create an instance of Pantograph using -```python -from pantograph import Server -server = Server() -``` - -## Lean Dependencies - -The server created from `Server()` is sufficient for basic theorem proving tasks -reliant on Lean's `Init` library. Some users may find this insufficient and want -to use non-builtin libraries such as Aesop or Mathlib4. In this case, feed in a -list of module names via the `imports` parameter e.g. `imports=["Mathlib"]`. Due -to inherent restrictions in Lean, importing a module that has not been imported -before after the server has already started is not allowed and will trigger -initializer exceptions. It may be possible to circumvent this if Lean relaxes -this constraint. - -To use external Lean dependencies such as -[Mathlib4](https://github.com/leanprover-community/mathlib4), Pantograph relies -on an existing Lean repository. Instructions for creating this repository can be -found [here](https://docs.lean-lang.org/lean4/doc/setup.html#lake). - -After creating this initial Lean repository, execute in the repository -```sh -lake build -``` - -to build all files from the repository. This step is necessary after any file in -the repository is modified. - -Then, feed the repository's path to the server -```python -server = Server(project_path="./path-to-lean-repo/") -``` - -For a complete example, see `examples/`. - -## Server Parameters - -The server has some additional options. - -- `core_options`: These options are passed to Lean's kernel. For example - `set_option pp.all true` in Lean corresponds to passing `pp.all=true` to - `core_options`. -- `options`: These options are given to Pantograph itself. See below. -- `timeout`: This timeout controls the maximum wait time for the server - instance. If the server instance does not respond within this timeout limit, - it gets terminated. In some cases it is necessary to increase this if loading - a Lean project takes too long. - -A special note about running in Jupyter: Use the asynchronous version of each -function. - -```python -server = await Server.create() -unit, = await server.load_sorry_async(sketch) -print(unit.goal_state) -``` - -### Options - -- `automaticMode`: Set to false to disable automatic goal continuation. -- `timeout`: Set to a positive integer to set tactic execution timeout. -- `printDependentMVars`: Set to true to explicitly store goal inter-dependencies diff --git a/apn/prompts.py b/apn/prompts.py index 97784718..484c4298 100644 --- a/apn/prompts.py +++ b/apn/prompts.py @@ -31,8 +31,6 @@ def encouragement_prompt() -> str: def user_prompt(path: str, token_limit: int | None, literature: bool, util_module: str) -> str: parts = [] - PYTHON_LIBS = ["sympy", "mpmath", "numpy", "pantograph"] - PROOF_PATH = "/workspace/leanproject/Submission/Spec.lean" parts.append(f"""\ @@ -50,11 +48,14 @@ def user_prompt(path: str, token_limit: int | None, literature: bool, util_modul Your submission may depend only on the following axioms: {', '.join(f'`{a}`' for a in PERMITTED_AXIOMS)}. Don't attempt to cheat with Lean loopholes, the verifier will reject such attempts. Your environment has the following available: -* A Lean 4 toolchain with Mathlib -* `git`, `rg`, and `jq` -* The `sage` computer algebra system -* `python` with the following libraries: {', '.join(f'`{lib}`' for lib in PYTHON_LIBS)}. -* Documentation for libraries is available at `/opt/` +* A Lean 4 toolchain with Mathlib, plus the `loogle` search CLI. +* The `sage` computer algebra system (version 10), with `gp` (PARI), `gap`, `Singular`, and `maxima` also on PATH. +* `python3` with numpy, scipy, sympy, mpmath, pandas, networkx, igraph, python-flint, highspy (LP/MIP), cvxpy (with Clarabel), pyscipopt (SCIP, global MINLP), clingo (answer-set programming), graphillion (ZDD set families), libsemigroups_pybind11 (semigroups/automata), pymanopt (manifold optimization), pysindy (sparse dynamics identification), hypothesis (property-based testing), python bindings for z3, cvc5, OR-Tools CP-SAT, and pysat, and snappy (SnapPy, 3-manifolds). +* `julia` with OSCAR and Hecke preinstalled (Galois groups, number fields, group theory). +* Solver binaries: `z3`, `cvc5`, `kissat` (SAT, DIMACS), `cryptominisat` (SAT), `drat-trim`/`lrat-check` and `cake_lpr` (SAT proof checkers), `breakid` (CNF symmetry breaking), `smsg` (SAT-modulo-symmetries graph search), `march_cu` (cube-and-conquer splitting), `vampire` (first-order prover, finite models via --mode fmb), `eprover` (first-order prover), `prover9`/`mace4` (first-order prover / countermodel finder), `csdp` (semidefinite programs), `msolve` (polynomial systems), `clingo` (ASP), `minizinc` (constraint modeling), `berkeley-abc` (Boolean networks). +* Mathematical CLI tools: `primesieve`, `primecount`, `ecm` and `msieve` (integer factorization), `srsieve2` (k*b^n+-c sieving), `sllr64` and `pfgw64` (special-form primality proving), the nauty suite (`geng`, `genbg`, `gentreeg`, `gentourng`, `vcolg`, `shortg`, `labelg`, `showg`, `amtog`, ...), `plantri` (planar graphs), `polymake` (polyhedral geometry), `normaliz` (rational cones), 4ti2 (lattice ideals), `lrs` (vertex enumeration), `redumis` (large independent sets), `M2` (Macaulay2, commutative algebra), `regina-python` (low-dimensional topology), `topcom-*` (point-configuration triangulations), `cadabra2` (tensor algebra), `mpsolve` (certified polynomial roots), `gclc` (Euclidean geometry proving), and `/opt/walnut/walnut.sh` (Walnut: decides automatic-sequence/base-k digit statements). +* `git`, `rg`, `jq`, and `gcc`/`make` +* Documentation for the less famous tools is available at `/opt/docs` Blindly searching for counterexamples using numerics is rarely a good approach. """) diff --git a/apn/redteam.py b/apn/redteam.py index cad29dff..26bdbe8e 100644 --- a/apn/redteam.py +++ b/apn/redteam.py @@ -110,8 +110,9 @@ def collatzStep (n : ℕ) : ℕ := if n % 2 = 0 then n / 2 else 3 * n + 1 cannot break it, report what you tried and why each approach failed. Be persistent and methodical: when one approach fails, understand why from the -codebase and try another. You have a Lean toolchain, `git`, `rg`, `jq`, `python` -(sympy/mpmath/numpy/pantograph), and `sage` available. +codebase and try another. You have a Lean toolchain, `git`, `rg`, `jq`, `python3` +(numpy/scipy/sympy/mpmath and more), `sage`, and a suite of solver and math CLI +tools available. """ @@ -123,7 +124,7 @@ def _apn_codebase_tar() -> bytes: root = Path(apn.__file__).parent skip_top = {"data", "__pycache__"} - skip_any = {"__pycache__", "pantograph-docs", "pypantograph-docs"} + skip_any = {"__pycache__"} buf = io.BytesIO() with tarfile.open(fileobj=buf, mode="w:gz") as tf: for p in sorted(root.rglob("*")): diff --git a/pyproject.toml b/pyproject.toml index 10ef6e4d..c0d6684a 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -1,6 +1,6 @@ [project] name = "apn" -version = "0.1.9" +version = "0.1.10rc3" description = "An Inspect implementation of the AlphaProof Nexus formal proof-search framework" license = "MIT AND Apache-2.0" license-files = ["LICENSE"] @@ -48,8 +48,6 @@ files = ["apn", "tests"] # tests/ is a namespace package (no __init__.py); tests import shared plumbing # as `tests.lean_sandbox`, so pin the repo root as the package base. explicit_package_bases = true -# Vendored third-party docs/examples, not our code. -exclude = 'pypantograph-docs' strict = true # Inspect ships py.typed; lean on its annotations. warn_unused_configs = true diff --git a/tests/test_agent_image.py b/tests/test_agent_image.py new file mode 100644 index 00000000..0a2798ed --- /dev/null +++ b/tests/test_agent_image.py @@ -0,0 +1,426 @@ +"""Contract test for the agent image's declared compute stack. + +The agent image's tool roster is *declared* -- in ``apn/lean/compute-env.yaml`` +plus the explicit install lines of the Dockerfile's ``compute_build``/ +``solvers_build``/``agent`` stages -- and advertised to the agent by +``apn.prompts.user_prompt``. This suite is the hardcoded contract between the +two: every advertised binary resolves, every advertised python module imports, +a handful of end-to-end smokes prove the big tools actually run (a present +binary with a broken runtime, e.g. a Sage missing its GAP, would pass a bare +``command -v``), and the vendored docs directories exist. If an install line is +dropped or a conda pin stops shipping a binary, this fails before an eval does. + +Every exec runs through ``bash --login -c`` -- exactly how the agent's bash +tool executes (``apn.tools``) -- so the PATH plumbing (/opt/env/bin first, via +/etc/profile.d) is itself under test. + +The agent (``default``) sandbox is brought up **once for the whole module** +through Inspect's lifecycle from the production compose +(``apn.task.get_compose_file``, which builds from ``apn/lean/Dockerfile``), +exactly like ``tests/test_gold_proofs.py``, sharing one module-scoped event +loop. Docker is part of the test environment, so this always runs. +""" + +from __future__ import annotations + +import platform +from collections.abc import AsyncIterator +from contextlib import asynccontextmanager + +import pytest +import pytest_asyncio +from inspect_ai.util import SandboxEnvironment +from inspect_ai.util._sandbox.context import ( + cleanup_sandbox_environments_sample, + init_sandbox_environments_sample, +) +from inspect_ai.util._sandbox.docker.docker import DockerSandboxEnvironment + +from apn.dataset import OEIS_DIR, fc_commit +from apn.task import get_compose_file + +# --------------------------------------------------------------------------- # +# The contract: hardcoded rosters (no manifest machinery by design -- these # +# lists and the Dockerfile install lines are maintained together by hand). # +# --------------------------------------------------------------------------- # + +# Binaries, by provenance: +BINARIES = [ + # lean layer (base) + loogle_build + "lake", + "lean", + "loogle", + # conda env (/opt/env/bin; spec: compute-env.yaml) + "python3", + "sage", + "gp", + "gap", + "Singular", + "maxima", + "z3", + "clingo", + "primesieve", + "primecount", + "ecm", + "geng", + "genbg", + "gentreeg", + "gentourng", + "vcolg", + "shortg", + "labelg", + "showg", + "amtog", + "normaliz", + "zsolve", + "lrs", + # solvers_build (/usr/local/bin) + "kissat", + "plantri", + "cvc5", + "msolve", + "prover9", + "mace4", + "vampire", + "drat-trim", + "lrat-check", + "cake_lpr", + "breakid", + "smsg", + "march_cu", + "msieve", + "redumis", + "gclc", + # julia_build + "julia", + # apt (bookworm) + "polymake", + "M2", + "regina-python", + "cryptominisat", + "csdp", + "topcom-points2triangs", + "cadabra2", + "minizinc", + "berkeley-abc", + "eprover", + "mpsolve", + "java", + "jq", + "rg", + "git", + "gcc", + "make", +] + +# The special-form primality toolchain: absent from arm64 images (local dev +# on Apple silicon); CI and production images are amd64. sllr64/pfgw64 are +# x86-64 gwnum assembly; srsieve2's makefile only knows x86 and 32-bit ARM. +BINARIES_X86_ONLY = [ + "sllr64", + "pfgw64", + "srsieve2", +] + +# Python modules importable from the agent's `python3` (the /opt/env python). +PYTHON_MODULES = [ + "numpy", + "scipy", + "sympy", + "mpmath", + "pandas", + "networkx", + "igraph", + "flint", # python-flint + "highspy", + "fpylll", + "z3", + "cvc5", + "ortools", + "pysat", # python-sat + "snappy", # SnapPy + "cvxpy", + "pyscipopt", + "clingo", + "graphillion", + "libsemigroups_pybind11", + "pymanopt", + "pysindy", + "hypothesis", + "sage.all", +] + +# Docs directories, downloaded at image build from pinned upstream sources +# (Dockerfile `docs_fetch` stage -> /opt/docs/). +DOCS_DIRS = [ + "loogle", + "plantri", + "normaliz", + "4ti2", + "lrslib", + "msolve", + "csdp", + "regina", + "snappy", + "python-flint", + "sms", + "graphillion", + "breakid", + "drat-trim", + "cake_lpr", + "kamis", + "gclc", + "msieve", + "walnut", +] + + +@asynccontextmanager +async def _sandbox_envs() -> AsyncIterator[dict[str, SandboxEnvironment]]: + """Bring up the production compose and yield the live ``{name: env}`` dict + (mirrors ``tests/test_gold_proofs.py``; the agent workspace is ``default``).""" + compose = str(get_compose_file(fc_commit(OEIS_DIR), literature=False)) + task_name = "pytest_agent_image" + await DockerSandboxEnvironment.task_init(task_name, compose) + try: + envs = await init_sandbox_environments_sample( + sandboxenv_type=DockerSandboxEnvironment, + task_name=task_name, + config=compose, + files={}, + setup=None, + metadata={}, + ) + try: + yield envs + finally: + await cleanup_sandbox_environments_sample( + type="docker", + task_name=task_name, + config=compose, + environments=envs, + interrupted=False, + ) + finally: + await DockerSandboxEnvironment.task_cleanup(task_name, compose, cleanup=True) + + +@pytest_asyncio.fixture(loop_scope="module", scope="module") +async def agent_env() -> AsyncIterator[SandboxEnvironment]: + async with _sandbox_envs() as envs: + yield envs["default"] + + +async def _bash( + env: SandboxEnvironment, command: str, timeout: int = 120 +) -> tuple[int, str, str]: + """Run ``command`` exactly as the agent's bash tool does (login shell).""" + result = await env.exec(["bash", "--login", "-c", command], timeout=timeout) + return result.returncode, result.stdout, result.stderr + + +@pytest.mark.asyncio(loop_scope="module") +@pytest.mark.parametrize("binary", BINARIES) +async def test_binary_on_path(agent_env: SandboxEnvironment, binary: str) -> None: + code, stdout, stderr = await _bash(agent_env, f"command -v {binary}") + assert code == 0, f"binary {binary!r} not on the agent's login-shell PATH" + + +@pytest.mark.asyncio(loop_scope="module") +@pytest.mark.parametrize("binary", BINARIES_X86_ONLY) +@pytest.mark.skipif( + platform.machine() in ("arm64", "aarch64"), + reason="x86-64-only binaries; the sandbox is built for the host arch", +) +async def test_x86_binary_on_path(agent_env: SandboxEnvironment, binary: str) -> None: + code, stdout, stderr = await _bash(agent_env, f"command -v {binary}") + assert code == 0, f"binary {binary!r} not on the agent's login-shell PATH" + + +@pytest.mark.asyncio(loop_scope="module") +async def test_walnut_launcher_present(agent_env: SandboxEnvironment) -> None: + # Walnut is a tree at /opt/walnut, not a PATH binary; the prompt advertises + # its upstream launcher path verbatim. + code, stdout, _ = await _bash(agent_env, "test -x /opt/walnut/walnut.sh") + assert code == 0, "/opt/walnut/walnut.sh missing or not executable" + + +@pytest.mark.asyncio(loop_scope="module") +@pytest.mark.parametrize("module", PYTHON_MODULES) +async def test_python_module_imports( + agent_env: SandboxEnvironment, module: str +) -> None: + # Sage-adjacent imports (sage.all, ore_algebra, snappy) are slow cold. + code, stdout, stderr = await _bash( + agent_env, f"python3 -c 'import {module}'", timeout=300 + ) + assert code == 0, f"import {module} failed:\n{stderr[-2000:]}" + + +@pytest.mark.asyncio(loop_scope="module") +@pytest.mark.parametrize("tool", DOCS_DIRS) +async def test_docs_dir_present(agent_env: SandboxEnvironment, tool: str) -> None: + # Non-empty, not merely present. + code, stdout, _ = await _bash(agent_env, f"ls /opt/docs/{tool} | head -1") + assert code == 0 and stdout.strip(), f"/opt/docs/{tool} missing or empty" + + +# --------------------------------------------------------------------------- # +# End-to-end smokes: the big tools actually run. # +# --------------------------------------------------------------------------- # + + +@pytest.mark.asyncio(loop_scope="module") +async def test_sage_factors(agent_env: SandboxEnvironment) -> None: + code, stdout, stderr = await _bash( + agent_env, "sage -c 'print(factor(2^67-1))'", timeout=600 + ) + assert code == 0, f"sage failed:\n{stderr[-2000:]}" + assert stdout.strip() == "193707721 * 761838257287" + + +@pytest.mark.asyncio(loop_scope="module") +async def test_geng_counts_graphs_on_five_vertices( + agent_env: SandboxEnvironment, +) -> None: + code, stdout, _ = await _bash(agent_env, "geng -q 5 | wc -l") + assert code == 0 + assert stdout.strip() == "34" + + +@pytest.mark.asyncio(loop_scope="module") +async def test_cpsat_solves_trivial_model(agent_env: SandboxEnvironment) -> None: + script = ( + "from ortools.sat.python import cp_model\n" + "m = cp_model.CpModel()\n" + "x = m.new_int_var(0, 10, 'x')\n" + "m.add(x > 7)\n" + "s = cp_model.CpSolver()\n" + "assert s.solve(m) == cp_model.OPTIMAL\n" + "print(s.value(x))\n" + ) + code, stdout, stderr = await _bash( + agent_env, f"python3 - <<'EOF'\n{script}EOF", timeout=300 + ) + assert code == 0, f"CP-SAT smoke failed:\n{stderr[-2000:]}" + + +@pytest.mark.asyncio(loop_scope="module") +async def test_kissat_drattrim_roundtrip(agent_env: SandboxEnvironment) -> None: + """An UNSAT claim is only usable if its certificate checks: kissat emits a + DRAT proof (exit 20 = UNSAT), drat-trim verifies it (s VERIFIED).""" + code, stdout, stderr = await _bash( + agent_env, + "cd /tmp && printf 'p cnf 1 2\\n1 0\\n-1 0\\n' > smoke.cnf " + "&& kissat -q smoke.cnf smoke.drat; test $? -eq 20 " + "&& drat-trim smoke.cnf smoke.drat; rc=$?; rm -f smoke.cnf smoke.drat; exit $rc", + ) + assert code == 0, f"kissat/drat-trim roundtrip failed:\n{stdout[-1000:]}{stderr[-1000:]}" + + +@pytest.mark.asyncio(loop_scope="module") +async def test_gap_small_group(agent_env: SandboxEnvironment) -> None: + # The conda GAP ships the SmallGrp library; its absence would silently + # gut the group-theory workflow the prompt implies. + code, stdout, stderr = await _bash( + agent_env, "gap -q -c 'Print(Size(SmallGroup(64, 1)), \"\\n\"); QUIT;'", timeout=300 + ) + assert code == 0, f"gap failed:\n{stderr[-2000:]}" + # gap prints informational "#I ..." banner lines before the answer. + assert stdout.strip().splitlines()[-1] == "64", stdout[-2000:] + + +@pytest.mark.asyncio(loop_scope="module") +async def test_scip_solves_miqcp(agent_env: SandboxEnvironment) -> None: + # pyscipopt's wheel bundles libscip; max x+y s.t. x^2+y^2<=25, x integer. + script = ( + "from pyscipopt import Model\n" + "m = Model()\n" + "x = m.addVar('x', vtype='I', lb=0, ub=10)\n" + "y = m.addVar('y', lb=0, ub=5)\n" + "m.addCons(x*x + y*y <= 25)\n" + "m.setObjective(x + y, 'maximize')\n" + "m.hideOutput()\n" + "m.optimize()\n" + "assert m.getStatus() == 'optimal', m.getStatus()\n" + "assert abs(m.getObjVal() - 7) < 1e-4, m.getObjVal()\n" + ) + code, stdout, stderr = await _bash( + agent_env, f"python3 - <<'EOF'\n{script}EOF", timeout=300 + ) + assert code == 0, f"SCIP smoke failed:\n{stderr[-2000:]}" + + +@pytest.mark.asyncio(loop_scope="module") +async def test_vampire_refutes(agent_env: SandboxEnvironment) -> None: + code, stdout, stderr = await _bash( + agent_env, + "printf 'fof(a, axiom, p).\\nfof(c, conjecture, p).\\n' " + "| vampire --time_limit 30", + ) + assert code == 0, f"vampire failed:\n{stderr[-2000:]}\n{stdout[-2000:]}" + assert "Refutation" in stdout + + +@pytest.mark.asyncio(loop_scope="module") +async def test_walnut_decides_trivial_property(agent_env: SandboxEnvironment) -> None: + # Walnut ships the Thue-Morse word T; a universally true statement about + # it must come back TRUE (proves the jar + word automata actually load). + code, stdout, stderr = await _bash( + agent_env, + "cd /opt/walnut && printf 'eval smoketest \"?msd_2 An T[n]=T[n]\";\\nexit;\\n' | ./walnut.sh", + timeout=300, + ) + assert code == 0, f"walnut failed:\n{stderr[-2000:]}\n{stdout[-2000:]}" + assert "TRUE" in stdout, f"expected TRUE:\n{stdout[-2000:]}" + + +@pytest.mark.asyncio(loop_scope="module") +async def test_julia_oscar_loads(agent_env: SandboxEnvironment) -> None: + # The baked depot must load offline with no re-precompilation surprises. + code, stdout, stderr = await _bash( + agent_env, + "julia -e 'using Oscar; println(order(symmetric_group(4)))'", + timeout=600, + ) + assert code == 0, f"julia/Oscar failed:\n{stderr[-2000:]}" + assert stdout.strip().endswith("24") + + +@pytest.mark.asyncio(loop_scope="module") +async def test_loogle_finds_nat_prime(agent_env: SandboxEnvironment) -> None: + # Upstream's documented invocation (vendored at /opt/docs/loogle): from + # the project, via `lake env`. The Mathlib index is prebuilt in the image, + # so this must not fall into the slow index-construction path -- but cold + # start still imports Mathlib, hence the generous timeout. + code, stdout, stderr = await _bash( + agent_env, + "cd /workspace/leanproject && lake env loogle --module Mathlib 'Nat.Prime'", + timeout=900, + ) + assert code == 0, f"loogle failed:\n{stderr[-2000:]}" + assert "Nat.Prime" in stdout + + +@pytest.mark.asyncio(loop_scope="module") +async def test_trace_state_prints_goal(agent_env: SandboxEnvironment) -> None: + """The prompt's advertised goal-state idiom: `trace_state` before a `sorry` + prints the goal on stdout under `lake env lean` (regression-pins the + workflow the agent is told to use, in the real Lake project).""" + lean = ( + "import Mathlib.Tactic\\n" + "example (a b : Nat) : a + b = b + a := by\\n" + " trace_state\\n" + " sorry\\n" + ) + code, stdout, stderr = await _bash( + agent_env, + "cd /workspace/leanproject && mkdir -p Submission " + f"&& printf '{lean}' > Submission/TraceStateSmoke.lean " + "&& lake env lean Submission/TraceStateSmoke.lean; rc=$?; " + "rm -f Submission/TraceStateSmoke.lean; exit $rc", + timeout=600, + ) + # `sorry` warns but exits 0; the goal state must appear on stdout. + assert code == 0, f"lake env lean failed:\n{stderr[-2000:]}\n{stdout[-2000:]}" + assert "a + b = b + a" in stdout, f"goal state not printed:\n{stdout[-2000:]}" diff --git a/tests/test_tools.py b/tests/test_tools.py index 84b76e6f..97a6d030 100644 --- a/tests/test_tools.py +++ b/tests/test_tools.py @@ -21,10 +21,26 @@ def test_user_prompt_references_path() -> None: assert PROOF_PATH in rendered -def test_user_prompt_mentions_lean_and_pypantograph() -> None: +def test_user_prompt_mentions_environment_tools() -> None: + # Sentinel tools from each layer of the agent image's compute stack: the + # lean layer (loogle), the conda env (sage, z3, clingo), the pip layer + # (pyscipopt), the source-built/release solvers (kissat, vampire), the + # julia stack (Oscar), Walnut's launcher path, and the docs location. rendered = user_prompt(PROOF_PATH, token_limit=None, literature=False, util_module=UTIL_MODULE) assert "Lean 4" in rendered - assert "pantograph" in rendered.lower() + assert "loogle" in rendered + assert "sage" in rendered + assert "z3" in rendered + assert "clingo" in rendered + assert "pyscipopt" in rendered + assert "kissat" in rendered + assert "vampire" in rendered + assert "OSCAR" in rendered + assert "/opt/walnut/walnut.sh" in rendered + assert "/opt/docs" in rendered + # The pantograph toolchain is gone from the image; the prompt must not + # advertise it. + assert "pantograph" not in rendered.lower() # Statement-integrity rule must still be present (it's the one substantive # constraint the agent gets from the prompt rather than from the verifier). assert "statement" in rendered diff --git a/uv.lock b/uv.lock index 8f2c70b4..f3e86349 100644 --- a/uv.lock +++ b/uv.lock @@ -182,7 +182,7 @@ wheels = [ [[package]] name = "apn" -version = "0.1.9" +version = "0.1.10rc3" source = { editable = "." } [package.dev-dependencies]