Agent workspace rework: declared compute layer, expanded tool roster, Loogle, Pantograph removal - #39
Draft
tadamcz wants to merge 7 commits into
Draft
Agent workspace rework: declared compute layer, expanded tool roster, Loogle, Pantograph removal#39tadamcz wants to merge 7 commits into
tadamcz wants to merge 7 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).
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.