Agent workspace rework: declared compute layer, expanded tool roster, Loogle, Pantograph removal - #39
Draft
tadamcz wants to merge 19 commits into
Draft
Agent workspace rework: declared compute layer, expanded tool roster, Loogle, Pantograph removal#39tadamcz wants to merge 19 commits into
tadamcz wants to merge 19 commits into
Conversation
Replace the accreted apt-Sage/PyPantograph agent stack with a declared compute layer: one locked conda-forge env at /opt/env (compute-env.yaml, exact pins, verified for linux-64 and linux-aarch64), a solvers_build stage for tools with no packaging (kissat, plantri, prover9/mace4, msolve with static FLINT, official cvc5 static binary), a bookworm apt line for the rest, and a loogle_build stage compiling the Loogle Mathlib-search CLI at the FC pin's Mathlib rev. PyPantograph and its two vendored doc trees are removed; the Lean loop is lake env lean + trace_state. The prompt's environment section now advertises the full roster, and tests/test_agent_image.py contract-tests it (new agent-image CI suite).
The full agent image now builds at the oeis pin and passes the new contract suite end to end (binaries, imports, sage/geng/CP-SAT/loogle smokes, docs dirs). Fixes found by building: prover9 fetched as a tarball (no git in solvers_build), msolve's binary lands at the build root, ore_algebra installed pure-python (Cython >= 3.2, required env-wide by sage 10.9, cannot compile its optional arb extensions) and imported after sage.all, libmpfr6 declared for msolve. Loogle, per the build spike: the binary is statically linked, ignores LEAN_PATH, and takes --path flags that replace its whole search path, so a wrapper (loogle.sh) passes the FC project's package roots plus the toolchain stdlib; the index is prebuilt in loogle_build where the Mathlib rev provably matches. /opt/loogle ships binary + own oleans + index (~560 MB) with no second Mathlib copy. Vendored docs: apn/lean/docs/<tool> -> /opt/docs/<tool>, 14 tools, ~1 MB total, text/markdown only, one provenance line each, upstream LICENSE per dir, version-matched to the installed packages.
Loogle is now built as its own project at /opt/loogle with .lake/packages symlinked to the FC project's checkouts: lake update resolves its deps to exactly the project's pinned revs (nothing re-clones, Mathlib replays from the existing oleans), the binary's compile-time-embedded search path is the agent image's real layout, and the search index sits at the canonical LoogleMathlibCache.extra location the binary checks by itself. The agent image copies the raw binary, loogle's olean/index lib, and recreates the symlink -- the runtime shell wrapper and its --path roster are gone. (Adding loogle to the FC project itself was tried and rejected: lake update loogle drags transitive deps to loogle's stale manifest revs.) ore_algebra is dropped as low-value-high-pain: no PyPI release, a patched setup.py, and only the degraded pure-python build was possible anyway since sage 10.9's Cython >= 3.2 cannot compile its extensions; its common use is covered by sage's berlekamp_massey or a hand-rolled ansatz solve. With it go the setuptools pin and the stage's compiler/pkg-config, leaving the pip layer as four pinned wheels. Verified: full contract suite green against the rebuilt image.
Loogle master (pinned at 9f11169) is dependency-free, honors lake env's LEAN_PATH, and caches its search index next to the searched module's .olean with automatic invalidation -- and it builds cleanly under this track's v4.27.0 toolchain. So the loogle_build stage is now exactly upstream's documented recipe (clone, copy the project's lean-toolchain, lake build) plus one query to bake the Mathlib index; the agent image copies the binary and that index file. Agents invoke it per the vendored doc: lake env loogle --module Mathlib '<query>' (~15s per query with the baked index). The rev-retargeting build script, packages symlink, and Mathlib-rev coupling are all gone -- only the toolchain ties loogle to the pin. Verified: full contract suite green against the rebuilt image.
The corpus-sweep delta on the compute-stack rework. Every addition was route-verified empirically (conda/apt probes on both arches, sha256'd release binaries, trial source builds on arm64) before landing: - conda: clingo, cvxpy, clarabel. SCIP arrives via pyscipopt's bundled wheel instead (no scip/soplex build coexists with the sage stack's boost pin; exact rational LP stays covered by glpk's --exact). - pip: pyscipopt, graphillion (sdist, verified on py3.13), pysindy, hypothesis, libsemigroups_pybind11, pymanopt. - apt: topcom, cadabra2, minizinc, berkeley-abc, eprover, mpsolve, default-jre-headless. - solvers_build: vampire (pinned release, both arches), drat-trim + lrat-check, cake_lpr (upstream's pre-generated per-arch asm), breakid, smsg (SAT modulo symmetries), march_cu, msieve (portable OPT_FLAGS), redumis (KaMIS), gclc; amd64-only (gwnum/x86 asm; CI and production are amd64): srsieve2, sllr64 (LLR), pfgw64 (OpenPFGW). - walnut_build: Walnut v7.1.0 at /opt/walnut (automatic-sequence decision procedure; bookworm JRE). - julia_build: Julia 1.12.7 + Oscar 1.8.1/Hecke 0.39.22, fully precompiled offline-usable depot at /opt/julia-depot. Docs policy change: /opt/docs is now DOWNLOADED at image build by the docs_fetch stage -- verbatim upstream text files at pins matching the installed revisions (shared ARGs where the install is ARG-pinned) -- and the vendored apn/lean/docs/ tree is gone. PDF-only or unpinnable docs mean the tool ships undocumented. Dropped as not worth the complexity (fragile builds, unpinnable deps, cross-package interactions, abandonware, or redundant coverage): QEPCAD B, REDUCE/Redlog, dReal4, ganak, d4, yafu, cado-nfs, twee, MetiTarski, SDPA-GMP, ncpol2sdpa, gudhi, latte-integrale, genreg, snarkhunter, PHCpack/phcpy, Ibex, CAPD, PySR, GAP package suite (conda GAP already ships SmallGrp + CTblLib), soplex. Prompt and the hardcoded contract suite extended to match (new smokes: kissat->drat-trim certificate roundtrip, GAP SmallGroup, SCIP MIQCP, vampire refutation, Walnut on Thue-Morse, offline Oscar load); version 0.1.10rc2 for fresh image tags. Contract suite: 116 passed, 3 skipped (the amd64-only binaries, on an arm64 host).
…ports problems
One sample per tool group (lean, cas, python, solvers, number_theory,
discrete); a react agent with the tester system prompt works through each
tool -- starts, does real cross-checked work, fails well, integrates, docs --
and writes /workspace/report.{md,json}. The scorer records the report as
the score explanation/metadata; value = problems reported (a punch-list
size, not an accuracy). Dataset-agnostic, on the OEIS pin's agent image,
with the comparator service dropped from the sandbox config.
The prompt advertised '/opt/walnut/walnut.sh' -- an invocation upstream never documents (the launcher uses a jar path relative to its own directory, so it only works from /opt/walnut, which Walnut's README is where agents learn) -- and 'vampire --mode fmb', which Vampire rejects (its help documents -sa fmb). Both were surfaced by all three models in the math-software-test runs. The prompt now gives Walnut's location and Vampire's capability only; how to run a tool is its own documentation's job. Same trim in the software-test briefs.
…ies load breakid shipped unrunnable: upstream's CMake defaults to a shared libbreakid that the executable loads at start, and only the executable was copied out of solvers_build, so every run died with 'libbreakid.so.3.1: cannot open shared object file'. Found by all three models in the math-software-test runs. Build with BUILD_SHARED_LIBS=OFF so the library is linked in (the binary still links only libstdc++/libc, per the stage contract). test_binary_on_path now also runs ldd on each binary's real path and fails on any 'not found' library -- the check that catches present-but-unloadable binaries, which 'command -v' cannot. readlink -f first: java and julia are reached via symlinks and use an $ORIGIN rpath. Version 0.1.10rc4 for fresh image tags.
With conda highspy installed, highspy and the ortools wheel each bring a libhighs, and whichever imports second fails on an undefined symbol (or a GLIBCXX version error); cvxpy's GLOP/PDLP backends, which load ortools, failed the same way. All three models hit it in the math-software-test runs. Remove highspy from the spec and pin cvxpy-base instead of the cvxpy metapackage (which hard-depends on highspy). Nothing is lost: LP/MIP stay covered by scipy's statically built HiGHS (linprog/milp) and OR-Tools' own HiGHS backend, and cvxpy keeps Clarabel/SCIP/GLOP/PDLP/SCS/OSQP/GLPK; only cvxpy's solver named HIGHS goes. Spec re-solved for linux-64 and linux-aarch64 (402 packages each, no highspy). New contract smoke runs CP-SAT and cvxpy GLOP/PDLP/Clarabel in one interpreter.
compute-env.yaml is now the whole declaration of the agent's python: the former Dockerfile pip line moves into its `pip:` section (micromamba 2.9 installs it into the same env after the conda solve), and the two pip packages that do have both-platform conda builds (hypothesis, libsemigroups_pybind11) move to the conda list. Rule stated in the header: conda-forge when a both-platform pin exists and coexists with the sage stack, pip otherwise. Sage's optional backends and databases -- ordinary packages in this env, since conda-forge's Sage has no `sage -i` -- are installed, each from its upstream's own distribution: - pip (wheels, both arches): PyNormaliz (normaliz Polyhedron backend), pycryptosat (CryptoMiniSat SAT backend), the KnotInfo, matroid and cubic Hecke databases. conda: pycosat, python-symengine. - sagemath-giac 0.1.4 (Groebner bases via giac, giac integration engine): release tarball, meson build against the env's giac, no build isolation (its build-requires name sagemath-standard == the installed sage). - GAP packages (Sage's gap_packages list + grape/guava + hap's dependency nq, and packagemanager, which silences conda GAP's startup warning): from GAP's own packages-v4.15.1 tarball into the env's GAP root, the compiled three built as GAP's BuildPackages does. - Databases from Sage's upstream tarballs at the sha256s in sage 10.9's build/pkgs: full Cremona tables, Jones number fields, Odlyzko zeta zeros (pickled by sage per its recipe). polytopes_db_4d (9.2 GB) deliberately not installed. Every route was validated end to end in containers and on the rebuilt compute stage: Sage detects all 16 declared features (88 of 140 optional features present, from 77), the backends compute through Sage, spec solves on linux-64 and linux-aarch64. Env grows 6.1 -> 7.4 GB. Contract: PYTHON_MODULES gains the new modules; test_sage_optional_features_ present asks Sage's own feature detection for the declared list; test_sage_ optional_backends_compute exercises normaliz/giac/cryptominisat/GRAPE/ Cremona/Odlyzko through Sage. Prompt's Sage bullet names the installed backends and databases (what exists, not how to invoke it); the software- test brief asks to exercise them.
main's #48 removed PyPantograph, which this branch had already done in a broader rework; every conflicting file keeps this branch's version (a superset of main's change). main's release is 0.1.10, so this branch's 0.1.10rc4 would sort below it: version is now 0.1.11rc1 for fresh image tags. Non-conflicting changes from main (ExtractRanges.lean, Hawk configs, the oeis-open-lite config) come in as-is.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Reworks the agent sandbox so its math tooling is declared, not accreted, then expands the roster per the corpus sweep.
Base rework (first four commits)
lake env lean+trace_state./opt/env(apn/lean/compute-env.yaml, exact pins, everything explicit — nothing rides on sage's dependency closure), first on the agent's PATH; apt only for what conda-forge lacks; pinned source builds for the rest. No manifest machinery: the spec + Dockerfile install lines are the source of truth,tests/test_agent_image.pyis the hardcoded contract,apn/prompts.pyadvertises the roster.lake env loogle --module Mathlib "<query>", Mathlib index prebaked (~15s queries).Delta (last commit): expanded roster + docs policy
Driven by a four-subagent sweep of all 1,189 FormalConjectures problem files; every install route verified empirically before landing (conda/apt probes on both arches, sha256'd release binaries, trial source builds).
--mode fmb), eprover.glpsol --exact), cvxpy + clarabel, clingo (ASP), minizinc, redumis (KaMIS)./opt/walnut, topcom, cadabra2, mpsolve, berkeley-abc, gclc, graphillion, libsemigroups, pymanopt, pysindy, hypothesis./opt/docsis now downloaded at image build (docs_fetchstage) — verbatim upstream text files pinned to the installed revisions; the vendoredapn/lean/docs/tree is deleted. PDF-only/unpinnable ⇒ ships undocumented.Verification
tests/test_agent_image.py, newagent-imageCI matrix entry): binaries on the login-shell PATH, python imports, docs dirs, and end-to-end smokes (sage, geng, CP-SAT, loogle, trace_state, kissat→drat-trim certificate roundtrip, GAP SmallGroup, SCIP MIQCP, vampire refutation, Walnut on Thue–Morse, offline Oscar load): 116 passed, 3 skipped (amd64-only binaries, on an arm64 host) against the locally built image at the oeis pin.Version bumped to 0.1.10rc2 for fresh image tags. Note for CI: the amd64 Oscar precompile is the one path not verifiable on an arm host (emulated precompiles crash by design of qemu, artifacts verified complete) — the first CI image build exercises it.