Research-Stack/.github/workflows/math-check.yml
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>
2026-05-12 04:40:20 +00:00

181 lines
6.1 KiB
YAML

name: Math-First Checks
on:
pull_request:
paths:
- '0-Core-Formalism/lean/Semantics/**'
- '6-Documentation/docs/distilled/**'
- 'shared-data/artifacts/deepseek_review/**'
- 'shared-data/data/stack_solidification/**'
- 'shared-data/schemas/**'
- 'scripts/math-first/**'
- 'claims.yaml'
- '.pre-commit-config.yaml'
- '.github/workflows/math-check.yml'
push:
branches:
- main
- distilled
paths:
- '0-Core-Formalism/lean/Semantics/**'
- '6-Documentation/docs/distilled/**'
- 'shared-data/artifacts/deepseek_review/**'
- 'shared-data/data/stack_solidification/**'
- 'shared-data/schemas/**'
- 'scripts/math-first/**'
- 'claims.yaml'
- '.pre-commit-config.yaml'
- '.github/workflows/math-check.yml'
workflow_dispatch:
permissions:
contents: read
pull-requests: write
concurrency:
group: math-check-${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true
jobs:
validate-schemas:
name: Validate DeepSeek receipts and claims registry
runs-on: ubuntu-latest
steps:
- name: Checkout repository
uses: actions/checkout@v4
with:
fetch-depth: 0
submodules: false
- name: Setup Python 3.11
uses: actions/setup-python@v5
with:
python-version: '3.11'
- name: Install validator dependencies
run: |
python -m pip install --upgrade pip
python -m pip install "jsonschema>=4.21" "rfc3339-validator" "PyYAML"
- name: Validate JSON Schema files compile
run: |
python - <<'PY'
import json, sys
from pathlib import Path
from jsonschema import Draft202012Validator
for path in sorted(Path("shared-data/schemas").glob("*.schema.json")):
schema = json.loads(path.read_text())
Draft202012Validator.check_schema(schema)
print(f"OK {path}")
PY
- name: Validate all tracked DeepSeek review receipts
run: |
python3 scripts/math-first/validate_deepseek_receipts.py
- name: Self-tests for receipt validator
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
- name: Verify receipt SHA-256 integrity against answer files
# Re-run the canonical emitter in --verify-only mode against every
# tracked receipt. This is the AGENTS.md contract for promoted
# Ollama/DeepSeek review receipts: answer_sha256 must match the bytes
# of the answer file on disk.
run: |
set -euo pipefail
shopt -s nullglob
emitter="5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py"
if [ ! -x "$emitter" ] && [ ! -f "$emitter" ]; then
echo "skip: $emitter not present (nothing to verify)"
exit 0
fi
receipts=(shared-data/artifacts/deepseek_review/*.receipt.json)
if [ "${#receipts[@]}" -eq 0 ]; then
echo "no receipts to verify"
exit 0
fi
failures=0
for receipt in "${receipts[@]}"; do
if python3 "$emitter" --verify-only "$receipt"; then
echo "OK $receipt"
else
echo "FAIL $receipt"
failures=$((failures + 1))
fi
done
if [ "$failures" -gt 0 ]; then
echo "$failures receipt(s) failed --verify-only" >&2
exit 1
fi
require-evidence:
name: Require math evidence on math-track PRs
runs-on: ubuntu-latest
if: github.event_name == 'pull_request'
steps:
- name: Checkout repository
uses: actions/checkout@v4
with:
fetch-depth: 0
- name: Setup Python 3.11
uses: actions/setup-python@v5
with:
python-version: '3.11'
- name: Require receipt or Lean change alongside math-track edits
run: |
python3 scripts/math-first/require_math_evidence.py \
--from-git-diff origin/${{ github.base_ref }}
pre-commit:
name: Run pre-commit hooks on changed files
runs-on: ubuntu-latest
if: github.event_name == 'pull_request'
steps:
- name: Checkout repository
uses: actions/checkout@v4
with:
fetch-depth: 0
# We deliberately do not smudge LFS pointers here -- the pre-commit
# hooks never need the actual binary content, and pulling LFS would
# add noise. The next step disables the LFS smudge filters locally
# so pre-commit's stash/pop cycle does not trip over pointer files.
lfs: false
- name: Disable LFS filters for pre-commit
# pre-commit stashes unstaged changes before running hooks and pops
# them back after. When the working tree contains LFS pointer files
# but Git's LFS smudge filter is configured (per .gitattributes), the
# stash/pop cycle reports a phantom diff against the binary content
# Git thinks it should smudge, and the pop fails. Clearing the
# filters locally for this job removes the disagreement without
# mutating the repository or any LFS-tracked files.
run: |
git config --local filter.lfs.smudge ""
git config --local filter.lfs.clean ""
git config --local filter.lfs.process ""
git config --local filter.lfs.required false
- name: Setup Python 3.11
uses: actions/setup-python@v5
with:
python-version: '3.11'
- name: Install pre-commit
run: python -m pip install --upgrade pip "pre-commit>=3.7"
- name: Run pre-commit on changed files
run: |
base="origin/${{ github.base_ref }}"
head="HEAD"
pre-commit run --from-ref "$base" --to-ref "$head" --show-diff-on-failure