From 3fb27157799295d53acea2e2b11d35940bf6bc70 Mon Sep 17 00:00:00 2001 From: InauguralPhysicist Date: Mon, 3 Aug 2026 06:21:28 -0500 Subject: [PATCH] Bump EigenScript pin v0.34.0 -> v0.35.1 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Picks up the #827 fix: unbounded temporal assignment history that armed on dead code. v0.35.0 also carries the lib/ui x-y chart widget (#819). COUNTER CHECK — both banked Tseitin regimes reproduce BYTE-IDENTICALLY on v0.35.1: 3x3 = 1,850 resolutions / 619 conflicts, 4x4 = 96,733 / 27,421, both UNSAT. No re-bank needed or performed. RSS stayed flat at 3,756 kB across the 675s 4x4 solve. Pin sites: ci.yml inline clone, CLAUDE.md x2, and GAPS.md's "the CI pin is now v0.34.0" clause. Left untouched as record of record: "#772 shipped in v0.34.0 (PR #773)", the 2026-07-31 RE-BANK entry, and ALL of TSEITIN_LADDER.md — line 454 records the pin of the two LIVE HF Space control lanes. No Space was touched, redeployed, or paused. Preflight: tests/run_smoke.sh exit 0 (all four solver modes, six bench modes, vendored corpus). Co-Authored-By: Claude Opus 5 (1M context) --- .github/workflows/ci.yml | 2 +- CLAUDE.md | 4 ++-- GAPS.md | 8 ++++++-- 3 files changed, 9 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 59b69ad..8b9548e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -14,7 +14,7 @@ jobs: - name: Build EigenScript run: | - git clone --branch v0.34.0 --depth 1 https://github.com/InauguralSystems/EigenScript.git /tmp/eigenscript + git clone --branch v0.35.1 --depth 1 https://github.com/InauguralSystems/EigenScript.git /tmp/eigenscript cd /tmp/eigenscript && make build echo "/tmp/eigenscript/src" >> $GITHUB_PATH diff --git a/CLAUDE.md b/CLAUDE.md index b36be9c..dd5ea6e 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -32,7 +32,7 @@ Minimum is **v0.11.8** — the earliest release that runs the CDCL suite green. The floor is set by a v0.11.x VM fix, not by stdlib integer vectors (those shipped in v0.11.2, but that release still crashes the CDCL path). -CI builds and tests against EigenScript **v0.34.0** (pinned in +CI builds and tests against EigenScript **v0.35.1** (pinned in `.github/workflows/ci.yml`): the correctness suite is green — all `test_solver.eigs` assertions and the full `run_smoke.sh` pass. The `Inline tiny accessors in CDCL hot path` commit captures the hoist @@ -245,7 +245,7 @@ Latest commits are the budgeted, resumable CDCL sessions (the one-shot solve is re-derived from them), landed via PR #56. The benchmark surface is mature — most current work is data-driven decisions out of `docs/EIGENSCRIPT_FEEDBACK.md`. Verified green on -EigenScript v0.34.0 (correctness suite only; not an `n=5` perf claim). +EigenScript v0.35.1 (correctness suite only; not an `n=5` perf claim). ## Gotchas diff --git a/GAPS.md b/GAPS.md index d468f72..2e29193 100644 --- a/GAPS.md +++ b/GAPS.md @@ -13,13 +13,17 @@ Root EigenScript issues should be fixed upstream instead of worked around here. run. Soundness is unaffected — conflicts are re-verified and drat-trim accepts the refutations — but banked counters measure "solver + periodic loop truncation", deterministically per runtime version. **#772 shipped in - EigenScript v0.34.0 (PR #773); the CI pin is now v0.34.0. RE-BANK DONE + EigenScript v0.34.0 (PR #773); the CI pin is now v0.35.1. RE-BANK DONE (2026-07-31): 3x3 and 4x4 on the released v0.34.0 are byte-identical to the post-clause_locked bank** — the stepped `cdcl_begin`/`cdcl_step` harness resets the old cap's per-frame counter every 300-conflict step, so the cap never fired inside the ladder; regimes 2 and 3 coincide. See the ladder's "Third regime check" section. The pre-clause_locked 4x5 number - keeps its caveat. + keeps its caveat. **RE-VERIFIED on the released v0.35.1 (2026-08-03, at + the pin bump): 3x3 = 1,850 resolutions / 619 conflicts and 4x4 = 96,733 / + 27,421, both byte-identical to the v0.34.0 bank** (UNSAT, 4x4 wall 675s + on the devbox — wall is per-host color only). The runtime bump did not + move a single solver-visible counter, so no re-bank was needed. - **SOUNDNESS BUG FOUND AND FIXED (2026-07-30): `clause_locked` checked only literal position 0.** This solver tracks watch POSITIONS in `watch_a`/`watch_b` rather than swapping literals into slots 0/1 (MiniSat's