Skip to content

v1.14.0 — the Identity Engine + a faster, leaner swarm

Choose a tag to compare

View all tags
@cgbarlow cgbarlow released this 15 Jun 02:03
v1.14.0
43a599d
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

Headline: the Identity Engine, and a faster, more self-sufficient swarm — the #400 big-hairy-goal lands as the Identity Engine (ADR-043), a themed program to mass-source mathlib-absent, non-trivial, swarm-provable identities & inequalities at scale, each vetted (absence + triviality + a compiling proof + an adversarial skeptic) before sourcing, with the next 200–300 staged as a candidate backlog. Around it, Gate A gets much faster — an incremental Lake build cache (ADR-045) replaces the ~16–21-min-per-job cold build, with timeout headroom for the rare cold path — and the swarm gets less idle and less brittle: parked-goal recovery (ADR-044), an archive-aware goal-immutability check, and self-verify/lint parity fixes that unblock main (#612).

Added

  • The Identity Engine (docs/plans/identity-engine.md, ADR-043): a themed program to mass-source mathlib-absent, non-trivial, swarm-provable elementary identities & inequalities at scale — the #400 big-hairy-goal. Each candidate is verified before sourcing (absence + ADR-035 triviality + a compiling intended proof + an adversarial skeptic pass), and the next 200–300 are staged as a vetted candidate backlog under backlog/candidates/.

Changed

  • Gate A's gate-a-prepare and gate-a-audit jobs now allow 45 minutes (was 30); gate-a-replay stays at 60 — headroom for the rare cold library build (#567/#573, SPEC-045-A).
  • Gate A now caches the local Lake build directory (.lake/build) across runs, so lake build UnsorryLibrary is incremental instead of cold-building the whole library in every job (ADR-045/SPEC-045-A) — the library is built once per run instead of three times. Soundness unchanged: the axiom audit + leanchecker kernel replay still validate every olean that reaches main.

Fixed

  • Fixed agent-lint failing on main (and therefore every open PR): rewrote the #612 binding-suppression check in swarm/agent.sh to clear shellcheck SC2015. No behaviour change; --self-test green.
  • Gate A's goal-immutability check (tools/gate_a/check_goal_immutability.py, ADR-018) is now archive-aware, unblocking ADR-041 archive-block retirement — a delete is exempt iff the goal id is in an archive manifest and the archived statement is byte-identical at the base ref.
  • The swarm no longer reports "nothing claimable" while dozens of open goals sit recoverable (ADR-044/SPEC-044-A): a --prove cycle with no claimable viable goal now re-surfaces one goal parked below TAU_V and retries it through the same pipeline with its accumulated lesson history.
  • The swarm's local proof self-verify now suppresses linter.unusedVariables in the regenerated ADR-011 statement-binding obligation, matching Gate A — so a proof that leaves a hypothesis unused is no longer needlessly decomposed (#612).

Full changelog: https://github.com/agenticsnz/unsorry/blob/main/CHANGELOG.md

Assets 2
Loading