mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
3 commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
Devin AI
|
1bc4d9bf7d |
fix: regression test now actually exercises --staged in temp repo
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> |
||
|
Devin AI
|
f70552211b |
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: '<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> |
||
|
Devin AI
|
87960676b4 |
Add math-first tooling: receipt schema, claims registry, pre-commit, CI, MCP
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> |