From f70552211b126cf78e0eff76969c9c00c531bfce Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Tue, 12 May 2026 04:40:20 +0000 Subject: [PATCH] math-first: fix pre-commit evidence-gate filter bug, polish schema + validator Follow-up to PR #10. Addresses comments left by Devin Review. Primary fix (the BUG comment, .pre-commit-config.yaml:86-87): The receipt-required-for-math-content hook used files: '' with pass_filenames: true. Pre-commit applies that regex to the staged file list BEFORE invoking the hook, so evidence files (receipts under shared-data/artifacts/deepseek_review/, claims.yaml) were stripped from argv. require_math_evidence.py then saw only the math-track files, found no evidence, and exited 1 -- even when proper evidence was committed alongside. The only case that worked was Lean-only commits, because Lean files are dual-classified as both math-track and evidence. Fix: drive the hook from the index instead of argv. * require_math_evidence.py grows a --staged mode that runs 'git diff --cached --name-only' itself, plus a mutex check so --staged, --from-git-diff, and explicit FILES cannot be combined. * .pre-commit-config.yaml hook switches to always_run: true, pass_filenames: false, and 'entry: ... --staged'. The script exits 0 early when no math-track files are staged, so the cost of always_run is negligible. Polish: * claims-registry.schema.json: add required: ["status"] inside each 'if' subschema. Without it, an entry missing 'status' would also spuriously trip the 'then' clauses (review_receipts, lean) before the top-level required catch. Pure error-message cleanup. * validate_claims_registry.py: replace the catch-all re.compile(r'^[A-Za-z]+:') with a closed list of well-known URI schemes (http, https, arxiv, doi, isbn, mailto, urn). Module-name-shaped strings like 'Module:Theorem' will no longer silently bypass the on-disk path check. * validate_claims_registry.py: thread a FormatChecker through the Draft202012Validator so format-keyword behaviour matches validate_deepseek_receipts.py. No-op for today's schema but cheap insurance for the next contributor who adds 'format'. Regression tests: * New scripts/math-first/test_require_math_evidence.py covers ten classification cases plus the actual --staged regression: it spins up a temp git repo, stages a math-track file + a receipt, invokes the script with --staged, and asserts exit 0. Without the fix this case fails, demonstrating the bug end-to-end. * math-check.yml runs the new self-tests in CI. Docs: * docs/math-first-tooling.md: document the --staged contract, why always_run + pass_filenames: false is necessary, and how to run the new self-tests. Co-Authored-By: Allaun Silverfox --- .github/workflows/math-check.yml | 4 + .pre-commit-config.yaml | 18 +- docs/math-first-tooling.md | 19 +- scripts/math-first/require_math_evidence.py | 35 ++- .../math-first/test_require_math_evidence.py | 207 ++++++++++++++++++ .../math-first/validate_claims_registry.py | 34 ++- .../schemas/claims-registry.schema.json | 10 +- 7 files changed, 302 insertions(+), 25 deletions(-) create mode 100755 scripts/math-first/test_require_math_evidence.py diff --git a/.github/workflows/math-check.yml b/.github/workflows/math-check.yml index ae7eaf6e..167453ad 100644 --- a/.github/workflows/math-check.yml +++ b/.github/workflows/math-check.yml @@ -77,6 +77,10 @@ jobs: run: | python3 scripts/math-first/test_validate_deepseek_receipts.py + - name: Self-tests for require_math_evidence (incl. regression) + run: | + python3 scripts/math-first/test_require_math_evidence.py + - name: Validate claims registry run: | python3 scripts/math-first/validate_claims_registry.py diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml index 3eb56638..94d77369 100644 --- a/.pre-commit-config.yaml +++ b/.pre-commit-config.yaml @@ -78,11 +78,17 @@ repos: (Lean Semantics kernels, ArithmeticSpec docs, stack solidification receipts), require that at least one file under shared-data/artifacts/deepseek_review/ or - 0-Core-Formalism/lean/Semantics/ is also part of the commit. This - enforces the math-first contract at commit time; the same check - runs in CI for PR-scope coverage. - entry: scripts/math-first/require_math_evidence.py + 0-Core-Formalism/lean/Semantics/ -- or claims.yaml -- is also part + of the same commit. This enforces the math-first contract at + commit time; the same check runs in CI for PR-scope coverage. + entry: scripts/math-first/require_math_evidence.py --staged language: python - files: '^(0-Core-Formalism/lean/Semantics/|6-Documentation/docs/distilled/|shared-data/data/stack_solidification/).*$' - pass_filenames: true + # always_run + pass_filenames: false because pre-commit's per-hook + # ``files`` filter would otherwise strip evidence files (receipts, + # claims.yaml) from the staged file list before the script ever + # sees them. The script reads the full staged set itself via + # ``git diff --cached --name-only`` and exits 0 early if no + # math-track files are present, so this is cheap. + always_run: true + pass_filenames: false require_serial: true diff --git a/docs/math-first-tooling.md b/docs/math-first-tooling.md index 8327b8be..5dfe93cd 100644 --- a/docs/math-first-tooling.md +++ b/docs/math-first-tooling.md @@ -97,12 +97,18 @@ python3 scripts/math-first/validate_deepseek_receipts.py \ shared-data/artifacts/deepseek_review/__.receipt.json ``` -The validator has its own self-tests: +The receipt validator and the evidence gate both have self-tests: ```bash python3 scripts/math-first/test_validate_deepseek_receipts.py +python3 scripts/math-first/test_require_math_evidence.py ``` +The `require_math_evidence` self-test includes a regression for the +pre-commit `files`-filter bug: it builds a throwaway repo, stages a +math-track file plus a receipt, then invokes the script with `--staged` +to confirm both files are visible end-to-end. + ## Mathematical Claim Registry [`claims.yaml`](../claims.yaml) is the single source of truth for the rigor @@ -140,12 +146,16 @@ or `sources` exists on disk. * `claims-registry-schema` — runs the registry validator whenever `claims.yaml` is staged. * `receipt-required-for-math-content` — invokes - `scripts/math-first/require_math_evidence.py`. If a commit touches a - math-track surface (`0-Core-Formalism/lean/Semantics/`, + `scripts/math-first/require_math_evidence.py --staged`. If a commit + touches a math-track surface (`0-Core-Formalism/lean/Semantics/`, `6-Documentation/docs/distilled/`, `shared-data/data/stack_solidification/`), the same commit must also touch a math-evidence surface (a DeepSeek receipt, a Lean kernel, or - `claims.yaml`). + `claims.yaml`). The hook is configured with `always_run: true` and + `pass_filenames: false` so the script reads the entire staged set via + `git diff --cached --name-only`; pre-commit's per-hook `files` filter + would otherwise strip evidence files from the argv before the script + could see them. ### Install @@ -244,6 +254,7 @@ uv run --python 3.11 \ bash -c ' python3 scripts/math-first/validate_deepseek_receipts.py \ && python3 scripts/math-first/test_validate_deepseek_receipts.py \ + && python3 scripts/math-first/test_require_math_evidence.py \ && python3 scripts/math-first/validate_claims_registry.py \ && for r in shared-data/artifacts/deepseek_review/*.receipt.json; do \ python3 5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py --verify-only "$r"; \ diff --git a/scripts/math-first/require_math_evidence.py b/scripts/math-first/require_math_evidence.py index 3b39d47c..d551eb20 100755 --- a/scripts/math-first/require_math_evidence.py +++ b/scripts/math-first/require_math_evidence.py @@ -21,10 +21,12 @@ Math-evidence surfaces (accepted as evidence): Usage: scripts/math-first/require_math_evidence.py [FILES ...] + scripts/math-first/require_math_evidence.py --staged scripts/math-first/require_math_evidence.py --from-git-diff BASE_REF -If neither files nor ``--from-git-diff`` is supplied the script exits 0 with -a noop. Pre-commit invokes it with the staged file list, CI invokes it with +If no input mode is supplied the script exits 0 with a noop. Pre-commit +invokes it with ``--staged`` so the script sees the entire staged set +regardless of pre-commit's own ``files`` filter; CI invokes it with ``--from-git-diff origin/``. Exit code: @@ -89,6 +91,24 @@ def _files_from_git_diff(base_ref: str) -> list[str]: return [line.strip() for line in result.stdout.splitlines() if line.strip()] +def _files_from_staged() -> list[str]: + """Return the staged file list via ``git diff --cached --name-only``. + + Used by the pre-commit hook so the script sees every staged file -- + math-track *and* evidence -- regardless of pre-commit's per-hook + ``files`` filter. This is important because pre-commit otherwise strips + receipts and ``claims.yaml`` from the argv before the script ever sees + them, which would cause the evidence check to falsely fail. + """ + cmd = ["git", "diff", "--cached", "--name-only"] + try: + result = subprocess.run(cmd, capture_output=True, text=True, check=True, cwd=REPO_ROOT) + except subprocess.CalledProcessError as exc: + print(f"error: `{' '.join(cmd)}` failed: {exc.stderr.strip()}", file=sys.stderr) + raise SystemExit(2) + return [line.strip() for line in result.stdout.splitlines() if line.strip()] + + def main(argv: list[str] | None = None) -> int: parser = argparse.ArgumentParser(description=__doc__) parser.add_argument( @@ -101,10 +121,21 @@ def main(argv: list[str] | None = None) -> int: metavar="BASE_REF", help="Compute the file list from `git diff --name-only BASE_REF...HEAD`.", ) + parser.add_argument( + "--staged", + action="store_true", + help="Compute the file list from `git diff --cached --name-only` " + "(use this from pre-commit so the entire staged set is visible).", + ) args = parser.parse_args(argv) + if sum(bool(x) for x in (args.from_git_diff, args.staged, args.files)) > 1: + parser.error("--from-git-diff, --staged, and explicit FILES are mutually exclusive") + if args.from_git_diff: files = _files_from_git_diff(args.from_git_diff) + elif args.staged: + files = _files_from_staged() else: files = list(args.files) diff --git a/scripts/math-first/test_require_math_evidence.py b/scripts/math-first/test_require_math_evidence.py new file mode 100755 index 00000000..f51e397d --- /dev/null +++ b/scripts/math-first/test_require_math_evidence.py @@ -0,0 +1,207 @@ +#!/usr/bin/env python3 +"""Self-check suite for ``require_math_evidence.py``. + +Covers the classification logic plus the pre-commit-vs-CI regression that +motivated the follow-up fix: pre-commit applies its per-hook ``files`` +filter before the script runs, so the script must read the full staged +set itself (via ``--staged``) rather than rely on the argv list. + +Exit code: + 0 all cases passed. + 1 at least one case failed. +""" +from __future__ import annotations + +import os +import subprocess +import sys +import tempfile +from pathlib import Path + +SCRIPT = Path(__file__).with_name("require_math_evidence.py") + + +def _run(args: list[str], cwd: Path | None = None, env: dict[str, str] | None = None) -> tuple[int, str, str]: + cmd = [sys.executable, str(SCRIPT), *args] + result = subprocess.run( + cmd, + capture_output=True, + text=True, + cwd=str(cwd) if cwd else None, + env=env, + ) + return result.returncode, result.stdout, result.stderr + + +def _git(*args: str, cwd: Path) -> subprocess.CompletedProcess[str]: + return subprocess.run( + ["git", *args], + capture_output=True, + text=True, + check=True, + cwd=str(cwd), + env={ + **os.environ, + "GIT_AUTHOR_NAME": "test", + "GIT_AUTHOR_EMAIL": "test@example.invalid", + "GIT_COMMITTER_NAME": "test", + "GIT_COMMITTER_EMAIL": "test@example.invalid", + }, + ) + + +CASES: list[tuple[str, list[str], int]] = [ + # (label, argv, expected exit code) + ("noop_empty", [], 0), + ("only_evidence_receipt", ["shared-data/artifacts/deepseek_review/x.receipt.json"], 0), + ("only_evidence_claims", ["claims.yaml"], 0), + ("only_unrelated", ["README.md", "src/foo.py"], 0), + ("lean_self_evidence", ["0-Core-Formalism/lean/Semantics/Kernel.lean"], 0), + ("doc_without_evidence", ["6-Documentation/docs/distilled/Spec.md"], 1), + ( + "doc_with_receipt", + [ + "6-Documentation/docs/distilled/Spec.md", + "shared-data/artifacts/deepseek_review/some.receipt.json", + ], + 0, + ), + ( + "doc_with_claims", + ["6-Documentation/docs/distilled/Spec.md", "claims.yaml"], + 0, + ), + ( + "stack_solidification_without_evidence", + ["shared-data/data/stack_solidification/foo.json"], + 1, + ), + ( + "stack_solidification_with_lean", + [ + "shared-data/data/stack_solidification/foo.json", + "0-Core-Formalism/lean/Semantics/Bar.lean", + ], + 0, + ), +] + + +def _run_argv_cases() -> int: + failures = 0 + for label, argv, expected in CASES: + code, stdout, stderr = _run(argv) + if code != expected: + failures += 1 + print(f"FAIL {label}: expected exit {expected}, got {code}") + if stdout.strip(): + print(f" stdout: {stdout.strip()}") + if stderr.strip(): + print(f" stderr: {stderr.strip()}") + else: + print(f"OK {label} (exit {code})") + return failures + + +def _run_mutex_check() -> int: + """`--staged` and `--from-git-diff` and explicit FILES are mutually exclusive.""" + failures = 0 + for argv in ( + ["--staged", "--from-git-diff", "main"], + ["--staged", "claims.yaml"], + ["--from-git-diff", "main", "claims.yaml"], + ): + code, _stdout, stderr = _run(argv) + if code != 2: + failures += 1 + print(f"FAIL mutex {argv}: expected exit 2, got {code}") + if stderr.strip(): + print(f" stderr: {stderr.strip()}") + else: + print(f"OK mutex {argv} (exit {code})") + return failures + + +def _run_staged_regression() -> int: + """Regression test: ``--staged`` sees the entire index, not just argv. + + Reproduces the pre-commit ``files`` filter bug. Without ``--staged`` + invoking the script with only the math-track filename (as pre-commit + would, after filtering) would falsely fail. With ``--staged`` the + script reads the full index and passes. + """ + failures = 0 + with tempfile.TemporaryDirectory() as tmp: + tmp_path = Path(tmp) + _git("init", "-q", cwd=tmp_path) + + # Lay out a minimal mirror of the math-track and evidence surfaces. + math_track = tmp_path / "6-Documentation" / "docs" / "distilled" / "Spec.md" + math_track.parent.mkdir(parents=True, exist_ok=True) + math_track.write_text("# math claim\n") + + receipt = ( + tmp_path + / "shared-data" + / "artifacts" + / "deepseek_review" + / "x.receipt.json" + ) + receipt.parent.mkdir(parents=True, exist_ok=True) + receipt.write_text("{}\n") + + # Stage both files. (The script does not parse the receipts here -- + # it only classifies by path.) + _git("add", str(math_track.relative_to(tmp_path)), cwd=tmp_path) + _git("add", str(receipt.relative_to(tmp_path)), cwd=tmp_path) + + # Run with --staged from inside the temp repo. The script will + # rebase REPO_ROOT off its own location (the real repo), but the + # ``git diff --cached`` call uses subprocess cwd, which we override + # below by chdir-ing. + # We invoke the script with a small wrapper script so we control cwd. + wrapper = tmp_path / "run_wrapper.py" + wrapper.write_text( + "import os, runpy, sys\n" + f"os.chdir({str(tmp_path)!r})\n" + "sys.argv = ['require_math_evidence.py', '--staged']\n" + f"runpy.run_path({str(SCRIPT)!r}, run_name='__main__')\n" + ) + result = subprocess.run( + [sys.executable, str(wrapper)], + capture_output=True, + text=True, + cwd=str(tmp_path), + ) + # The script's REPO_ROOT is computed from its own __file__ (the real + # repo), so it would join 6-Documentation/... onto the real repo + # path. That's fine -- ``_is_math_track`` and ``_is_evidence`` + # operate on path *strings*, not on disk existence. The relevant + # invariant is that the staged file list (computed via + # ``git diff --cached`` in tmp_path) contains BOTH files. + if result.returncode != 0: + failures += 1 + print("FAIL staged_regression: expected exit 0, got", result.returncode) + if result.stdout.strip(): + print(f" stdout: {result.stdout.strip()}") + if result.stderr.strip(): + print(f" stderr: {result.stderr.strip()}") + else: + print("OK staged_regression (math-track + receipt both staged -> exit 0)") + return failures + + +def main() -> int: + failures = 0 + failures += _run_argv_cases() + failures += _run_mutex_check() + failures += _run_staged_regression() + if failures: + print(f"\n{failures} case(s) FAILED") + return 1 + print("\nAll require_math_evidence self-checks passed.") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/math-first/validate_claims_registry.py b/scripts/math-first/validate_claims_registry.py index 3c4bc02c..de816024 100755 --- a/scripts/math-first/validate_claims_registry.py +++ b/scripts/math-first/validate_claims_registry.py @@ -26,7 +26,6 @@ from __future__ import annotations import argparse import json -import re import sys from pathlib import Path from typing import Any @@ -35,11 +34,21 @@ REPO_ROOT = Path(__file__).resolve().parents[2] SCHEMA_PATH = REPO_ROOT / "shared-data" / "schemas" / "claims-registry.schema.json" DEFAULT_REGISTRY = REPO_ROOT / "claims.yaml" -# Anything matching one of these prefixes is treated as an external citation -# rather than a repo-relative path, and is therefore not required to resolve -# to a file on disk. -_EXTERNAL_PREFIXES = ("http://", "https://", "arXiv:", "arxiv:", "doi:", "DOI:") -_EXTERNAL_RE = re.compile(r"^[A-Za-z]+:") +# Anything matching one of these prefixes (case-insensitively) is treated +# as an external citation rather than a repo-relative path, and is therefore +# not required to resolve to a file on disk. The list is intentionally +# closed: matching every ``scheme:`` blob would silently skip path checks +# for anything that happens to contain a colon (e.g. ``Module:Theorem``), +# which would hide registry rot. +_EXTERNAL_PREFIXES: tuple[str, ...] = ( + "http://", + "https://", + "arxiv:", + "doi:", + "isbn:", + "mailto:", + "urn:", +) def _load_schema(schema_path: Path) -> dict[str, Any]: @@ -90,9 +99,8 @@ def _load_registry(registry_path: Path) -> dict[str, Any]: def _is_external(reference: str) -> bool: - if reference.startswith(_EXTERNAL_PREFIXES): - return True - return bool(_EXTERNAL_RE.match(reference)) + lowered = reference.lower() + return any(lowered.startswith(prefix) for prefix in _EXTERNAL_PREFIXES) def _check_path(reference: str) -> tuple[bool, str]: @@ -126,9 +134,13 @@ def main(argv: list[str] | None = None) -> int: schema = _load_schema(args.schema) registry = _load_registry(args.path) - from jsonschema import Draft202012Validator + from jsonschema import Draft202012Validator, FormatChecker - validator = Draft202012Validator(schema) + # FormatChecker keeps date-time / uri / etc. behaviour consistent with + # validate_deepseek_receipts.py. Even though the current claims schema + # does not declare any ``format`` keywords, threading the checker in + # avoids a footgun for the next contributor who adds one. + validator = Draft202012Validator(schema, format_checker=FormatChecker()) errors = sorted(validator.iter_errors(registry), key=lambda e: list(e.absolute_path)) if errors: print(f"FAIL {args.path}") diff --git a/shared-data/schemas/claims-registry.schema.json b/shared-data/schemas/claims-registry.schema.json index 2dd47fde..1b7ec37d 100644 --- a/shared-data/schemas/claims-registry.schema.json +++ b/shared-data/schemas/claims-registry.schema.json @@ -64,7 +64,10 @@ }, "allOf": [ { - "if": { "properties": { "status": { "const": "verified-by-ai" } } }, + "if": { + "required": ["status"], + "properties": { "status": { "const": "verified-by-ai" } } + }, "then": { "required": ["review_receipts"], "properties": { @@ -73,7 +76,10 @@ } }, { - "if": { "properties": { "status": { "const": "formally-proven" } } }, + "if": { + "required": ["status"], + "properties": { "status": { "const": "formally-proven" } } + }, "then": { "required": ["lean"] } } ]