From aeb3d6cabedeca1ec26e95c5a67d6b638452bc8b 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 1/3] 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"] } } ] From 6100565578fae681f839c81de07600a0da9a7bf6 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:51:57 +0000 Subject: [PATCH 2/3] fix: regression test now actually exercises --staged in temp repo MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Addresses Devin Review on PR #11 ("Staged regression test passes vacuously — git diff runs in real repo, not temp repo"). Root cause: scripts/math-first/require_math_evidence.py hardcoded cwd=REPO_ROOT on the git subprocess. REPO_ROOT is computed from __file__, which always resolves to the REAL repo path -- even when the test invokes the script with cwd=tmp_path. So 'git diff --cached --name-only' queried the real (clean) repo, returned an empty list, and the script exited 0 via the noop short-circuit. The regression test then printed OK while never actually exercising the --staged classification logic. Fix: Introduce _git_toplevel() in require_math_evidence.py that runs 'git rev-parse --show-toplevel' from the *inherited* cwd. Both _files_from_staged() and _files_from_git_diff() now use that toplevel as their subprocess cwd. Pre-commit and CI both invoke the script from inside the repo root anyway, so behaviour in production is unchanged; only the test (and any other caller that runs the script from a non-Research-Stack directory) now works correctly. Test hardening: test_require_math_evidence.py's staged regression now drives the script via plain subprocess with cwd=tmp_path (no runpy wrapper, no os.chdir trickery) and covers three sub-cases against the same temp repo: (a) math-track-only staged -> expect exit 1 (negative) (b) math-track + receipt staged -> expect exit 0 (the bug) (c) math-track + claims.yaml -> expect exit 0 (registry) Sub-case (a) is the key addition: with the pre-fix script, this case wrongly returns 0 (real repo is clean -> noop), so the test fails loudly. Verified locally by temporarily reverting the cwd fix -- the test correctly reports 'FAIL staged_regression_negative: expected exit 1, got 0'. Docs: docs/math-first-tooling.md notes that receipt-required-for-math-content is a no-op in the CI pre-commit job (pre-commit's --from-ref/--to-ref mode does not touch the index, so --staged returns an empty list and the hook exits 0). PR-scope enforcement of the same rule lives in the dedicated require-evidence CI job. This addresses the Devin Review info comment on .pre-commit-config.yaml. Co-Authored-By: Allaun Silverfox --- docs/math-first-tooling.md | 6 +- scripts/math-first/require_math_evidence.py | 48 ++++++- .../math-first/test_require_math_evidence.py | 122 +++++++++++------- 3 files changed, 126 insertions(+), 50 deletions(-) diff --git a/docs/math-first-tooling.md b/docs/math-first-tooling.md index 5dfe93cd..2806927e 100644 --- a/docs/math-first-tooling.md +++ b/docs/math-first-tooling.md @@ -184,7 +184,11 @@ math-first surface. It has three jobs: 3. **`pre-commit`** — runs every pre-commit hook against the PR's range of changed files (`pre-commit run --from-ref --to-ref HEAD`), so the guardrails are honoured even when a contributor has not installed the - hooks locally. + hooks locally. Note: `receipt-required-for-math-content` is a no-op in + this CI job because pre-commit's `--from-ref / --to-ref` mode does not + stage anything in the index, so the script's `--staged` lookup returns + an empty file list and exits 0. PR-scope enforcement of the same rule + lives in the dedicated `require-evidence` job above. The pre-existing `wolfram-verification.yml` workflow continues to police mathematical formulas inside Lean source for missing Wolfram Alpha diff --git a/scripts/math-first/require_math_evidence.py b/scripts/math-first/require_math_evidence.py index d551eb20..b0115a09 100755 --- a/scripts/math-first/require_math_evidence.py +++ b/scripts/math-first/require_math_evidence.py @@ -40,8 +40,42 @@ import subprocess import sys from pathlib import Path +# Only used for logging/help -- *not* as the subprocess ``cwd`` for the git +# calls below. Hardcoding the subprocess cwd to this path caused the +# regression test in ``test_require_math_evidence.py`` to pass vacuously +# because the test stages files in a *temp* repo and expects ``git diff +# --cached`` to query that temp repo, not the real one. Pre-commit and CI +# both happen to invoke the script from inside the repo root, so letting +# the git subprocess inherit cwd is correct in every real-world case. REPO_ROOT = Path(__file__).resolve().parents[2] + +def _git_toplevel(cwd: Path | None = None) -> Path: + """Return the absolute path of the git working tree containing ``cwd``. + + Defaults to the current working directory. The script never assumes the + git repo lives at ``REPO_ROOT`` because that would be wrong when the + script is run from a different working tree -- notably, the temp repo + set up by ``test_require_math_evidence.py``. + """ + cmd = ["git", "rev-parse", "--show-toplevel"] + try: + result = subprocess.run( + cmd, + capture_output=True, + text=True, + check=True, + cwd=str(cwd) if cwd is not None else None, + ) + except subprocess.CalledProcessError as exc: + print( + f"error: `{' '.join(cmd)}` failed: {exc.stderr.strip()}", + file=sys.stderr, + ) + raise SystemExit(2) + return Path(result.stdout.strip()) + + MATH_TRACK_PREFIXES: tuple[str, ...] = ( "0-Core-Formalism/lean/Semantics/", "6-Documentation/docs/distilled/", @@ -82,9 +116,12 @@ def _is_evidence(path: str) -> bool: def _files_from_git_diff(base_ref: str) -> list[str]: + cwd = _git_toplevel() cmd = ["git", "diff", "--name-only", f"{base_ref}...HEAD"] try: - result = subprocess.run(cmd, capture_output=True, text=True, check=True, cwd=REPO_ROOT) + result = subprocess.run( + cmd, capture_output=True, text=True, check=True, cwd=str(cwd) + ) except subprocess.CalledProcessError as exc: print(f"error: `{' '.join(cmd)}` failed: {exc.stderr.strip()}", file=sys.stderr) raise SystemExit(2) @@ -99,10 +136,17 @@ def _files_from_staged() -> list[str]: ``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. + + The subprocess cwd is the actual git toplevel containing the *current* + working directory, not a hardcoded path -- so the script works + correctly inside the regression test's temp repo too. """ + cwd = _git_toplevel() cmd = ["git", "diff", "--cached", "--name-only"] try: - result = subprocess.run(cmd, capture_output=True, text=True, check=True, cwd=REPO_ROOT) + result = subprocess.run( + cmd, capture_output=True, text=True, check=True, cwd=str(cwd) + ) except subprocess.CalledProcessError as exc: print(f"error: `{' '.join(cmd)}` failed: {exc.stderr.strip()}", file=sys.stderr) raise SystemExit(2) diff --git a/scripts/math-first/test_require_math_evidence.py b/scripts/math-first/test_require_math_evidence.py index f51e397d..38776de3 100755 --- a/scripts/math-first/test_require_math_evidence.py +++ b/scripts/math-first/test_require_math_evidence.py @@ -123,71 +123,99 @@ def _run_mutex_check() -> int: def _run_staged_regression() -> int: - """Regression test: ``--staged`` sees the entire index, not just argv. + """Regression for the pre-commit ``files``-filter bug. - 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. + Builds a throwaway git repo so this test is self-contained -- the + test does not depend on the state of the real repo's index. The + script is run with ``cwd=tmp_path`` (NOT via ``runpy``) so that + ``git rev-parse --show-toplevel`` inside the script resolves to the + temp repo, and ``git diff --cached`` queries the temp repo's index. + + Three sub-cases: + (a) math-track-only staged -> expect exit 1 + (proves the script actually evaluates classification logic; + without (a) the next sub-case could pass vacuously by + short-circuiting on an empty diff) + (b) math-track + receipt staged -> expect exit 0 + (the original pre-commit ``files``-filter bug) + (c) math-track + claims.yaml staged -> expect exit 0 + (verifies the registry-update path) """ failures = 0 with tempfile.TemporaryDirectory() as tmp: - tmp_path = Path(tmp) + tmp_path = Path(tmp).resolve() _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" + 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) + claims = tmp_path / "claims.yaml" + claims.write_text("claims: []\n") - # 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" + def _stage_only(*relpaths: str) -> None: + # Reset the index to a clean state, then stage exactly the + # supplied paths. ``git reset`` is safe here -- the temp repo + # has no commits, so there is no "HEAD" to reset against. We + # instead remove everything currently in the index. + _git("rm", "--cached", "-rf", "--ignore-unmatch", ".", cwd=tmp_path) + for relpath in relpaths: + _git("add", "--", relpath, cwd=tmp_path) + + def _invoke() -> subprocess.CompletedProcess[str]: + return subprocess.run( + [sys.executable, str(SCRIPT), "--staged"], + capture_output=True, + text=True, + cwd=str(tmp_path), + ) + + def _assert(label: str, expected_exit: int, *staged: str) -> int: + _stage_only(*staged) + indexed = _git("diff", "--cached", "--name-only", cwd=tmp_path).stdout.splitlines() + indexed = [line for line in indexed if line.strip()] + if sorted(indexed) != sorted(staged): + print(f"FAIL {label}: index does not match expected staging") + print(f" expected: {sorted(staged)}") + print(f" actual: {sorted(indexed)}") + return 1 + result = _invoke() + if result.returncode != expected_exit: + print( + f"FAIL {label}: expected exit {expected_exit}, " + f"got {result.returncode}" + ) + if result.stdout.strip(): + print(f" stdout: {result.stdout.strip()}") + if result.stderr.strip(): + print(f" stderr: {result.stderr.strip()}") + return 1 + print(f"OK {label} (exit {expected_exit})") + return 0 + + failures += _assert( + "staged_regression_negative (math-only -> FAIL)", + 1, + "6-Documentation/docs/distilled/Spec.md", ) - result = subprocess.run( - [sys.executable, str(wrapper)], - capture_output=True, - text=True, - cwd=str(tmp_path), + failures += _assert( + "staged_regression_positive_receipt (math + receipt -> OK)", + 0, + "6-Documentation/docs/distilled/Spec.md", + "shared-data/artifacts/deepseek_review/x.receipt.json", + ) + failures += _assert( + "staged_regression_positive_claims (math + claims.yaml -> OK)", + 0, + "6-Documentation/docs/distilled/Spec.md", + "claims.yaml", ) - # 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 From 8ffc4e2fda71cf4b5c35cb51f089d6da87f9a780 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:59:35 +0000 Subject: [PATCH 3/3] chore: remove now-unused REPO_ROOT from require_math_evidence Sourcery-bot housekeeping note on PR #11: REPO_ROOT was only mentioned in comments after the cwd-resolution fix in 61005655 and was no longer used by any logic in this module (other math-first scripts have their own REPO_ROOT constants). Removed it. Folded the rationale that previously lived in the comment above the constant into the _git_toplevel docstring so future readers still see why we don't hardcode the cwd. Co-Authored-By: Allaun Silverfox --- scripts/math-first/require_math_evidence.py | 15 ++++----------- 1 file changed, 4 insertions(+), 11 deletions(-) diff --git a/scripts/math-first/require_math_evidence.py b/scripts/math-first/require_math_evidence.py index b0115a09..065c2c79 100755 --- a/scripts/math-first/require_math_evidence.py +++ b/scripts/math-first/require_math_evidence.py @@ -40,23 +40,16 @@ import subprocess import sys from pathlib import Path -# Only used for logging/help -- *not* as the subprocess ``cwd`` for the git -# calls below. Hardcoding the subprocess cwd to this path caused the -# regression test in ``test_require_math_evidence.py`` to pass vacuously -# because the test stages files in a *temp* repo and expects ``git diff -# --cached`` to query that temp repo, not the real one. Pre-commit and CI -# both happen to invoke the script from inside the repo root, so letting -# the git subprocess inherit cwd is correct in every real-world case. -REPO_ROOT = Path(__file__).resolve().parents[2] - def _git_toplevel(cwd: Path | None = None) -> Path: """Return the absolute path of the git working tree containing ``cwd``. Defaults to the current working directory. The script never assumes the - git repo lives at ``REPO_ROOT`` because that would be wrong when the + git repo lives at a hardcoded path because that would be wrong when the script is run from a different working tree -- notably, the temp repo - set up by ``test_require_math_evidence.py``. + set up by ``test_require_math_evidence.py``. Pre-commit and CI both + happen to invoke the script from inside the repo root, so letting the + git subprocess inherit cwd is correct in every real-world case. """ cmd = ["git", "rev-parse", "--show-toplevel"] try: