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 <bigdataiscoming+9i37y6j2@protonmail.com>
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 <bigdataiscoming+9i37y6j2@protonmail.com>
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: '<math-track
regex>' 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 <bigdataiscoming+9i37y6j2@protonmail.com>
Adds automated guardrails so mathematical rigor is enforced by tooling
instead of by convention. See docs/math-first-tooling.md for the full
contract.
Schemas + registry:
- shared-data/schemas/deepseek-review-receipt.schema.json
Draft 2020-12 schema for the existing ollama_deepseek_review_receipt_v1
and ollama_deepseek_review_continuation_receipt_v1 receipt formats. Pins
sha256:<hex> hashes, non-negative token counts, repo-relative POSIX
paths, and rejects additional fields.
- shared-data/schemas/claims-registry.schema.json
Schema for claims.yaml. Requires review_receipts when status is
verified-by-ai and a lean source when status is formally-proven.
- claims.yaml
Initial registry entry: prime-gap-entropy-collapse (verified-by-ai)
linked to the two existing receipts under
shared-data/artifacts/deepseek_review/.
Validators (scripts/math-first/):
- validate_deepseek_receipts.py: validates tracked or passed receipts
against the JSON Schema; shared by pre-commit and CI.
- test_validate_deepseek_receipts.py: positive + 7 negative fixtures
asserting exit-code behaviour.
- validate_claims_registry.py: schema check + unique id check + on-disk
existence check for every referenced repo-relative path.
- require_math_evidence.py: gate that requires a DeepSeek receipt, a
Lean change, or a claims.yaml update alongside edits to math-track
surfaces (Lean Semantics kernels, ArithmeticSpec docs, stack
solidification receipts).
Pre-commit (.pre-commit-config.yaml):
- check-json, check-yaml, end-of-file-fixer, trim trailing whitespace,
detect-private-key (scoped to math-first files only per AGENTS.md
Do Not Sweep).
- Local hooks wiring all three math-first validators above.
CI (.github/workflows/math-check.yml):
- validate-schemas: compiles every schema, runs both validators, runs
the validator self-tests, then re-invokes the canonical Ollama
emitter in --verify-only mode against every tracked receipt to
re-check answer_sha256 against the answer-file bytes on disk.
- require-evidence: enforces the math-track evidence rule at PR scope.
- pre-commit: runs all pre-commit hooks against the PR diff so the
contract holds even for contributors who skip installing hooks
locally.
MCP (.mcp.json):
- filesystem, sympy, wolfram-alpha, lean, deepseek-review entries
pointing at off-the-shelf upstream servers and at the canonical
ollama_deepseek_review_emitter.py. Secrets stay in the runtime env
(WOLFRAM_ALPHA_APPID, OLLAMA_API_KEY) and are never embedded.
Docs (docs/math-first-tooling.md):
- Philosophy, surfaces, schema reference, registry workflow, hook
catalogue, CI catalogue, MCP catalogue, end-to-end verify command.
shared-data/schemas/*.schema.json and claims.yaml live under paths the
top-level .gitignore would normally exclude; they are force-added via
git add -f the same way existing promoted receipts under
shared-data/artifacts/deepseek_review/ are tracked (per AGENTS.md).
Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>
