Release tooling: --bump, sidecar coverage, single-owner check inventory with drift test

.aii/config.yaml

@@ -5,9 +5,7 @@ repo:
   name: fep_lean
   slug: fep-lean
   full_name: ActiveInferenceInstitute/fep_formal
-  description: '> **Release v1.6.0 candidate** (2026-10-07; prepared locally, unpublished) · Concept DOI [10.5281/zenodo.19699233](https://doi.org/10.5281/zenodo.19699233)
-    · License [CC BY 4.0](LICENSE) > > **Cite as:** Friedman, D. A. (2026). *Towards
-    Lean 4 Formalization of the Free Energy Principle:…'
+  description: 'Release v1.6.0 (2026-10-07; tagged v1.6.0) · Concept DOI [10.5281/zenodo.19699233](https://doi.org/10.5281/zenodo.19699233) · License CC BY 4.0. Standalone 168-topic Free Energy Principle / Active Inference Lean 4 catalogue.'
 institute:
   category: research-software
   steward: Active Inference Institute

AGENTS.md

@@ -120,6 +120,13 @@ document wins.
 
 ## Required checks
 
+This block is the single owner of the required-check list. `docs/development.md`,
+`docs/testing.md` and the README link here instead of re-listing it, and
+`tests/test_check_inventory.py` fails if a command below is neither executed in
+`.github/workflows/ci.yml` nor on that test's commented hosted-only/local-only
+allow-lists, or if CI runs a gate that is missing here. Add a check to CI and
+to this block in the same change.
+
 ```bash
 uv lock --check && uv pip check
 uv run python scripts/_maint_build_topics_catalogue.py --check
@@ -135,6 +142,8 @@ uv run fep-lean --project-root . methods check --output-root docs/mathematical-p
 uv run pytest specs/openai-math-methods/test_methods.py \
   specs/openai-math-methods/test_upstream.py \
   specs/openai-math-methods/test_visualization.py -q --no-cov
+uv run ruff check specs/openai-math-methods
+uv run ruff format --check specs/openai-math-methods
 uv run python scripts/audit_formalisms.py \
   --receipt output/formalism-audit.json
 uv run python docs/theorem_ref_audit.py
@@ -143,10 +152,17 @@ uv run fep-lean catalogue
 uv run python scripts/render_manuscript.py --check
 uv run python scripts/build_render_fonts.py --check
 uv run python scripts/check_render_log.py --verify-receipt
+uv run python scripts/build_manuscript_figures.py
+uv run python scripts/build_manuscript_figures.py --check
+uv run pytest specs/publication-browser-acceptance/test_validate_acceptance.py -q --no-cov
+uv run ruff check specs/publication-browser-acceptance
+uv run ruff format --check specs/publication-browser-acceptance
+uv run python specs/publication-browser-acceptance/validate_acceptance.py --collect output/python-acceptance-collection.json
 uv run pytest tests/ -q --cov=src --cov-fail-under=89 -m "not serial_lean"
 uv run mypy src
 uv run ruff check src tests scripts docs
 uv run ruff format --check src tests scripts docs
+git diff --check
 uv run python docs/check_links.py --strict --include-root
 uv run python docs/md_hygiene.py --strict --include-root
 uv run python docs/pin_audit.py --check-latest
@@ -156,6 +172,19 @@ uv run python specs/gnn-bridge-q5-artifact-proof/generate_probe.py --check
 uv run python specs/geo-infer-notation-bridge/check_geo_notation_bridge.py --check
 ```
 
+Native Lean checks need the built pinned Mathlib cache (`lake exe cache get`)
+and run in the hosted `lean` job:
+
+```bash
+(cd lean && lake build FepSketches)
+uv run pytest tests/ -q -m serial_lean -n 1 --no-cov
+uv run fep-lean verify --fail-on-warnings --receipt output/native-verification.json
+```
+
+Hosted CI also runs the `distribution` installed-wheel matrix, the isolated
+live Chrome pair and the membership aggregate of
+`validate_acceptance.py`; see `docs/testing.md` for those boundaries.
+
 The listed Q5 `generate_probe.py --check` and GEO notation checks validate
 retained static artifacts without a sibling checkout. CI runs both. Q5
 generation establishes fixture/probe/manifest freshness, not current

README.md

@@ -286,8 +286,9 @@ The operator command quick reference lives at
 ## Development checks
 
 Contributor setup, check tiers and repository rules are in
-[`CONTRIBUTING.md`](CONTRIBUTING.md). The complete release-gate list is maintained as "Required release gates" in
-[`docs/testing.md`](docs/testing.md); the quick local dev checks are:
+[`CONTRIBUTING.md`](CONTRIBUTING.md). The complete required-check list is
+maintained once, in the "Required checks" block of
+[`AGENTS.md`](AGENTS.md#required-checks); the quick local dev checks are:
 
 ```bash
 uv run pytest tests/ -q --cov=src --cov-fail-under=89 -m "not serial_lean"

docs/development.md

@@ -43,42 +43,16 @@ uv run python scripts/theorem_maturity_audit.py
 uv run python scripts/build_formalism_coverage.py
 uv run fep-lean atlas
 uv run fep-lean dashboard
-
-uv run python scripts/_maint_build_topics_catalogue.py --check
-uv run python scripts/_maint_build_fep_all_lean.py --check
-uv run python scripts/_maint_build_formal_modules.py --check
-uv run python scripts/theorem_maturity_audit.py --check
-uv run python scripts/build_formalism_coverage.py --check
-uv run python scripts/_maint_build_lean_landscape.py --check
-uv run fep-lean atlas --check
-uv run fep-lean dashboard --check
-uv run python specs/geo-infer-notation-bridge/check_geo_notation_bridge.py --check
-uv run python docs/theorem_ref_audit.py
-uv run python docs/citation_audit.py
-uv run fep-lean catalogue
-uv run python scripts/render_manuscript.py --check
-
-uv run ruff check src tests scripts docs
-uv run ruff format --check src tests scripts docs
-uv run mypy src
-uv run pytest tests/ -q --cov=src --cov-fail-under=89 -m "not serial_lean"
-uv run python docs/check_links.py --strict --include-root
-uv run python docs/md_hygiene.py --strict
-uv run python docs/pin_audit.py --check-latest
-uv run python docs/xref_audit.py
 ```
 
-Run native Lean acceptance separately because it is the expensive semantic
-compiler boundary:
+The required verification list (`--check` gates, audits, tests, lint, native
+Lean) is owned by the "Required checks" block in
+[`AGENTS.md`](../AGENTS.md#required-checks); it is not repeated here, and
+`tests/test_check_inventory.py` keeps it in step with `.github/workflows/ci.yml`.
 
-```bash
-uv run fep-lean verify \
-  --fail-on-warnings \
-  --receipt output/native-verification.json
-cd lean && lake build FepSketches
-cd .. && uv run python scripts/audit_formalisms.py \
-  --receipt output/formalism-audit.json
-```
+Native Lean acceptance (`lake build FepSketches`, `fep-lean verify`, the
+formalism audit) is the expensive semantic compiler boundary; its commands are in the same
+[required-checks block](../AGENTS.md#required-checks).
 
 The native receipt establishes exact-source compilation for the stable topic
 roster; the formalism audit separately covers the maintained formal modules

docs/release.md

@@ -9,8 +9,8 @@ actually ships, and it is fully checked by
 
 | Requirement | Checked by |
 | --- | --- |
-| One version across `pyproject.toml`, `src/fep_lean/__init__.py`, `CITATION.cff`, `manuscript/config.yaml`, `config/settings.yaml`, `uv.lock` and the release-bundle constants | `release_check.py` |
-| One release date across `CITATION.cff`, `manuscript/config.yaml` and the release-bundle constants | `release_check.py` |
+| One version across `pyproject.toml`, `src/fep_lean/__init__.py`, `CITATION.cff`, `manuscript/config.yaml`, `config/settings.yaml`, `.aii/config.yaml`, `uv.lock` and the release-bundle constants | `release_check.py` |
+| One release date across `CITATION.cff`, `manuscript/config.yaml`, `.aii/config.yaml` and the release-bundle constants | `release_check.py` |
 | A `## X.Y.Z — YYYY-MM-DD — title` section in `CHANGELOG.md` | `release_check.py` |
 | Clean working tree; `HEAD` equals `origin/main` | `release_check.py --hosted` |
 | The newest hosted `ci.yml` run on that exact commit succeeded, and its `python`, `static`, `lean`, `render-deps`, `render` and every `distribution` matrix job each succeeded (none skipped) | `release_check.py --hosted` |
@@ -31,8 +31,14 @@ A release changes no scientific claim. Unrun lanes stay described as unrun.
 
 ## Steps
 
-1. Bump the version and date in every file listed above, add the dated
-   `CHANGELOG.md` section, and run `uv lock`.
+1. Bump with
+   `uv run python docs/release_check.py --bump X.Y.Z --date YYYY-MM-DD`. It
+   rewrites the version and date in every file listed above plus the
+   InstituteOS sidecar (`.aii/config.yaml`: `meta.updated` and the
+   `Release vX.Y.Z (date; ...)` description, which must be reworded by hand if
+   the release is not yet tagged). Then add the dated `CHANGELOG.md` section
+   and run the printed `uv lock` (the bump never touches `uv.lock` or the
+   changelog).
 2. `uv run python docs/release_check.py` — fix every reported mismatch.
 3. Run the local suite and audits (see [development](development.md)), commit
    and push to `main`.
@@ -75,3 +81,9 @@ citation. The manuscript DOI identifies its exact scholarly version under the
 scholarly concept. For v1.6.0 the reserved version is
 `10.5281/zenodo.23220027`. Keep the scholarly concept, scholarly version and
 software concept distinct; do not describe the two histories as one version chain.
+
+## Deferred
+
+Publication is a maintainer action: there is intentionally no publishing
+workflow. Automating tag, GitHub release and Zenodo upload is deferred until a
+maintainer decides to delegate that authority.

docs/release_check.py

@@ -27,6 +27,9 @@
 #: conclusion alone is not enough.
 REQUIRED_JOBS = ("python", "static", "lean", "render-deps", "render")
 DISTRIBUTION_PREFIX = "distribution ("
+#: InstituteOS sidecar: ``repo.description`` names ``Release vX.Y.Z`` and the
+#: date; ``meta.updated`` carries the release date.
+SIDECAR = ".aii/config.yaml"
 
 
 @dataclass(frozen=True)
@@ -66,6 +69,14 @@ def _lock_version(root: Path) -> str | None:
     return versions[0] if len(versions) == 1 else None
 
 
+def _sidecar_release(root: Path) -> str | None:
+    """The release version the InstituteOS sidecar description names."""
+    repo = _yaml(root, SIDECAR).get("repo")
+    description = str(repo.get("description", "")) if isinstance(repo, dict) else ""
+    match = re.search(r"Release v(\d+\.\d+\.\d+\S*)", description)
+    return match.group(1) if match else None
+
+
 def read_versions(root: Path) -> dict[str, str | None]:
     """Every version-bearing source, keyed by the file a maintainer edits."""
     pyproject = tomllib.loads(_text(root, "pyproject.toml"))
@@ -86,6 +97,7 @@ def read_versions(root: Path) -> dict[str, str | None]:
         "config/settings.yaml": _nested(
             _yaml(root, "config/settings.yaml"), "project", "version"
         ),
+        SIDECAR: _sidecar_release(root),
         "uv.lock": _lock_version(root),
     }
 
@@ -101,6 +113,7 @@ def read_dates(root: Path) -> dict[str, str | None]:
             "src/fep_lean/output/release_bundle/_constants.py",
             "_CANONICAL_RELEASE_DATE",
         ),
+        SIDECAR: _nested(_yaml(root, SIDECAR), "meta", "updated"),
     }
 
 
@@ -111,6 +124,72 @@ def read_release(root: Path) -> Release:
     )
 
 
+_VERSION_RE = re.compile(r"\d+\.\d+\.\d+")
+_DATE_RE = re.compile(r"\d{4}-\d{2}-\d{2}")
+_CONSTANTS = "src/fep_lean/output/release_bundle/_constants.py"
+
+
+def _sub_once(text: str, pattern: str, replacement: str) -> str:
+    new, count = re.subn(pattern, replacement, text, count=1, flags=re.MULTILINE)
+    if count != 1:
+        raise ValueError(f"pattern not found: {pattern}")
+    return new
+
+
+def bump(root: Path, version: str, date: str) -> tuple[str, ...]:
+    """Rewrite the version and date in every file the gate reads.
+
+    Edits are line-local regex substitutions so quoting and comments survive.
+    ``uv.lock`` and ``CHANGELOG.md`` are deliberately left to the maintainer
+    (``uv lock``; a dated section); returns the files rewritten.
+    """
+    if not _VERSION_RE.fullmatch(version):
+        raise ValueError(f"version must look like X.Y.Z, got {version!r}")
+    if not _DATE_RE.fullmatch(date):
+        raise ValueError(f"date must look like YYYY-MM-DD, got {date!r}")
+    qv, qd = f'"{version}"', f'"{date}"'
+    edits: dict[str, list[tuple[str, str]]] = {
+        "pyproject.toml": [(r'^version\s*=\s*"[^"]+"', f"version = {qv}")],
+        "src/fep_lean/__init__.py": [
+            (r'^__version__\s*=\s*"[^"]+"', f"__version__ = {qv}")
+        ],
+        _CONSTANTS: [
+            (
+                r'^_CANONICAL_RELEASE_VERSION\s*=\s*"[^"]+"',
+                f"_CANONICAL_RELEASE_VERSION = {qv}",
+            ),
+            (
+                r'^_CANONICAL_RELEASE_DATE\s*=\s*"[^"]+"',
+                f"_CANONICAL_RELEASE_DATE = {qd}",
+            ),
+        ],
+        "CITATION.cff": [
+            (r"^version:.*$", f"version: {qv}"),
+            (r"^date-released:.*$", f"date-released: {qd}"),
+        ],
+        "manuscript/config.yaml": [
+            (r"^(  version:\s*).*$", rf"\g<1>{qv}"),
+            (r"^(  date:\s*).*$", rf"\g<1>{qd}"),
+        ],
+        "config/settings.yaml": [(r"^(  version:\s*).*$", rf"\g<1>{qv}")],
+        SIDECAR: [
+            (r"Release v\d+\.\d+\.\d+\S*", f"Release v{version}"),
+            (r"(?<=\()\d{4}-\d{2}-\d{2}", date),
+            (r"^(  updated:\s*).*$", rf"\g<1>'{date}'"),
+        ],
+    }
+    # Compute everything first so a failed pattern leaves the tree untouched.
+    rewritten: dict[str, str] = {}
+    for relative, subs in edits.items():
+        text = _text(root, relative)
+        for pattern, replacement in subs:
+            text = _sub_once(text, pattern, replacement)
+        rewritten[relative] = text
+    for relative, text in rewritten.items():
+        (root / relative).write_text(text, encoding="utf-8")
+    return tuple(rewritten)
+
+
 def _heading(release: Release) -> str:
     return f"## {release.version} — {release.date}"
 
@@ -223,10 +302,34 @@ def main(argv: list[str] | None = None) -> int:
         action="store_true",
         help="also require a clean HEAD equal to origin/main with green hosted CI",
     )
+    parser.add_argument(
+        "--bump",
+        metavar="X.Y.Z",
+        help="rewrite the version in every gated file (requires --date), then exit",
+    )
+    parser.add_argument("--date", metavar="YYYY-MM-DD", help="release date for --bump")
     parser.add_argument("--notes", type=Path, help="write the release notes here")
     parser.add_argument("--json", action="store_true", help="print a JSON report")
     args = parser.parse_args(argv)
     root = args.root.resolve()
+    if args.bump or args.date:
+        if not (args.bump and args.date):
+            parser.error("--bump and --date must be given together")
+        try:
+            changed = bump(root, args.bump, args.date)
+        except ValueError as exc:
+            print(f"FAIL: {exc}", file=sys.stderr)
+            return 1
+        print(f"Bumped {len(changed)} files to {args.bump} ({args.date}):")
+        for relative in changed:
+            print(f"  {relative}")
+        print("Remaining manual steps:")
+        print(
+            f"  1. add a '## {args.bump} — {args.date} — title' section to CHANGELOG.md"
+        )
+        print("  2. uv lock   # refreshes the fep-lean entry in uv.lock")
+        print("  3. uv run python docs/release_check.py")
+        return 0
     release = read_release(root)
     errors = list(metadata_errors(root))
     if args.hosted:

docs/testing.md

@@ -10,8 +10,10 @@ The suite uses real temporary files, SQLite databases, subprocesses, and local
 HTTP servers. Environment variables isolate secrets and expensive external
 integration tests; they do not manufacture successful execution results.
 
-Local checks are below; hosted `ci.yml` runs them, and a green hosted run on
-the exact commit is the release gate (see the [release procedure](release.md)):
+The full required-check list lives in one place, the "Required checks" block
+of [`AGENTS.md`](../AGENTS.md#required-checks); it is not repeated here.
+Hosted `ci.yml` runs it, and a green hosted run on the exact commit is the
+release gate (see the [release procedure](release.md)).
 
 Hosted Python acceptance records the complete non-serial test selection, runs
 the remainder in parallel, then runs the two real Chrome probes once with no
@@ -24,45 +26,9 @@ coverage are retained even when a component fails. This scheduling policy
 preserves the browser startup deadline and does not diagnose the historical
 startup timeouts. See the [acceptance validator](../specs/publication-browser-acceptance/README.md).
 
-```bash
-uv lock --check && uv pip check
-uv run python scripts/_maint_build_topics_catalogue.py --check
-uv run python scripts/_maint_build_fep_all_lean.py --check
-uv run python scripts/_maint_build_formal_modules.py --check
-uv run python scripts/theorem_maturity_audit.py --check
-uv run python scripts/build_formalism_coverage.py --check
-uv run python scripts/_maint_build_lean_landscape.py --check
-uv run python scripts/build_formalism_atlas.py --check
-uv run python scripts/build_formal_kernel_dashboard.py --check
-uv run pytest tests/ -q --cov=src --cov-fail-under=89 -m "not serial_lean"
-uv run mypy src
-uv run ruff check src tests scripts docs
-uv run ruff format --check src tests scripts docs
-git diff --check
-uv run python docs/check_links.py --strict --include-root
-uv run python docs/md_hygiene.py --strict --include-root
-uv run python docs/pin_audit.py --check-latest
-uv run python docs/xref_audit.py
-uv run python docs/theorem_ref_audit.py
-uv run python docs/citation_audit.py
-uv run fep-lean catalogue
-uv run python scripts/build_render_fonts.py --check
-uv run python scripts/check_render_log.py --verify-receipt
-uv run python scripts/render_manuscript.py --check
-uv run python scripts/build_manuscript_figures.py
-uv run python scripts/build_manuscript_figures.py --check
-```
-
-Native formal acceptance additionally requires the pinned toolchain and
-Mathlib build:
-
-```bash
-cd lean && lake build FepSketches
-cd .. && uv run python scripts/audit_formalisms.py \
-  --receipt output/formalism-audit.json
-uv run fep-lean verify --fail-on-warnings \
-  --receipt output/native-verification.json
-```
+The native formal commands (`lake build FepSketches`, the formalism audit,
+`fep-lean verify --fail-on-warnings --receipt ...`) require the pinned
+toolchain and Mathlib build and are listed in the same block.
 
 Hermes/OpenGauss full validation additionally requires external credentials;
 `fep-lean preflight` reports each missing capability without modifying the