allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
Research-Stack/docs/math-first-tooling.md
Devin AI 6100565578 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>
2026-05-12 04:51:57 +00:00

269 lines
13 KiB
Markdown
Raw Blame History

# Math-First Tooling
This document codifies the "math first" contract for the Research Stack: every
mathematical claim that ships from this repository must carry machine-checkable
evidence — a Lean proof, a DeepSeek review receipt with SHA-256 integrity, or
both — and the development environment must make it harder to bypass that
contract than to honour it.
It is the human-readable companion to:
| Artifact | Path |
|----------|------|
| Receipt schema | [`shared-data/schemas/deepseek-review-receipt.schema.json`](../shared-data/schemas/deepseek-review-receipt.schema.json) |
| Claim registry schema | [`shared-data/schemas/claims-registry.schema.json`](../shared-data/schemas/claims-registry.schema.json) |
| Claim registry | [`claims.yaml`](../claims.yaml) |
| Receipt validator | [`scripts/math-first/validate_deepseek_receipts.py`](../scripts/math-first/validate_deepseek_receipts.py) |
| Registry validator | [`scripts/math-first/validate_claims_registry.py`](../scripts/math-first/validate_claims_registry.py) |
| Evidence gate | [`scripts/math-first/require_math_evidence.py`](../scripts/math-first/require_math_evidence.py) |
| Pre-commit config | [`.pre-commit-config.yaml`](../.pre-commit-config.yaml) |
| CI workflow | [`.github/workflows/math-check.yml`](../.github/workflows/math-check.yml) |
| MCP server registry | [`.mcp.json`](../.mcp.json) |
Read [`AGENTS.md`](../AGENTS.md) and
[`6-Documentation/wiki/DeepSeek-Review-Process.md`](../6-Documentation/wiki/DeepSeek-Review-Process.md)
first — this document layers tooling on top of those contracts and does not
restate them.
## Philosophy
1. **Lean is the source of truth.** Anything that can be stated as a Lean
`theorem` or kernel obligation should live under
`0-Core-Formalism/lean/Semantics/`. Other evidence (DeepSeek reviews,
SymPy/Wolfram cross-checks, hardware receipts) is a witness, not a proof.
2. **Every claim has a status.** The states are
`conjecture → verified-by-ai → formally-proven → published`. Movement only
ever travels in that direction, and every transition is accompanied by a
change to `claims.yaml`.
3. **Receipts pin model output to disk.** DeepSeek answers and their
`*.receipt.json` siblings carry `prompt_sha256` and `answer_sha256` so a
review can be re-validated without re-running the model.
4. **CI enforces the contract.** Anything humans are expected to remember is
re-checked by a workflow that fails the PR if the contract is broken.
5. **AI assistants get tool access, not trust.** The `.mcp.json` registry
gives Claude / Devin / Codex the Wolfram, SymPy, and Lean bridges they need
to discharge proof obligations — and nothing else. DeepSeek review remains
available through the canonical CLI emitter until a real MCP wrapper exists.
## Repository Layout (math-first surfaces)
```
0-Core-Formalism/lean/Semantics/ # Lean source of truth (lakefile.toml)
shared-data/schemas/ # JSON Schemas for every receipt format
shared-data/artifacts/deepseek_review/ # Promoted DeepSeek review receipts
shared-data/data/stack_solidification/ # Stack receipts (math-track)
6-Documentation/docs/distilled/ # Distilled math specs (math-track)
scripts/math-first/ # Validators + evidence gate
claims.yaml # Single source of truth for claims
.pre-commit-config.yaml # Local guardrail
.github/workflows/math-check.yml # CI guardrail
.mcp.json # AI-assistant tool registry
```
## Receipt Schema (`ollama_deepseek_review_receipt_v1`)
The schema at
[`shared-data/schemas/deepseek-review-receipt.schema.json`](../shared-data/schemas/deepseek-review-receipt.schema.json)
formalises the contract that the canonical emitter
[`5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py`](../5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py)
already writes. It validates two receipt flavours:
* **Primary review** (`ollama_deepseek_review_receipt_v1`) — requires
`schema`, `created_at`, `model`, `endpoint`, `prompt_sha256`,
`answer_sha256`, `usage.{prompt_tokens,completion_tokens,total_tokens}`,
`context_files` (non-empty), and `answer_path`.
* **Continuation review** (`ollama_deepseek_review_continuation_receipt_v1`)
— replaces `context_files` with `previous_answer_path` and optionally
reports the `message_keys` returned by the continuation endpoint.
Both flavours pin SHA-256 hashes as the literal string `sha256:<64 hex>`,
require token counts to be non-negative integers, and require paths to be
repo-relative POSIX strings ending in `.md` for answer paths. Additional
fields are rejected so receipts stay shaped exactly as the emitter writes
them.
### Re-validate locally
```bash
uv run --python 3.11 \
--with "jsonschema>=4.21" --with "rfc3339-validator" \
python3 scripts/math-first/validate_deepseek_receipts.py
```
To validate a single receipt:
```bash
python3 scripts/math-first/validate_deepseek_receipts.py \
shared-data/artifacts/deepseek_review/<topic>_<model>_<ts>.receipt.json
```
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
level of every tracked mathematical claim. The schema accepts these fields:
| Field | Required | Notes |
|-------|----------|-------|
| `id` | yes | Stable kebab-case slug. |
| `title` | yes | One-line natural-language statement of the claim. |
| `status` | yes | `conjecture` \| `verified-by-ai` \| `formally-proven` \| `published`. |
| `lean` | conditional | Required when `status == formally-proven`. Repo-relative Lean source path. |
| `review_receipts` | conditional | Required when `status == verified-by-ai`. Repo-relative `*.receipt.json` paths. |
| `sources` | no | Supporting docs, scripts, or external citations. |
| `notes` | no | Free-form context. |
```bash
uv run --python 3.11 \
--with "jsonschema>=4.21" --with "PyYAML" \
python3 scripts/math-first/validate_claims_registry.py
```
The validator enforces the JSON Schema, asserts every `id` is unique, and
asserts every repo-relative path referenced from `lean`, `review_receipts`,
or `sources` exists on disk.
## Pre-Commit Hooks
`.pre-commit-config.yaml` wires four guardrails:
* `pre-commit-hooks` — `check-json`, `check-yaml`, EOF / trailing whitespace
scoped to math-first files only (see [`AGENTS.md`](../AGENTS.md) "Do Not
Sweep"), and `detect-private-key`.
* `deepseek-receipt-schema` — runs the receipt validator on every staged
`*.receipt.json` under `shared-data/artifacts/deepseek_review/`.
* `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 --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`). 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
```bash
uv tool install pre-commit # one-time, per machine
pre-commit install # one-time, per clone
pre-commit run --all-files # smoke-test
```
## CI Workflow
[`.github/workflows/math-check.yml`](../.github/workflows/math-check.yml)
runs on every PR and on pushes to `main` or `distilled` that touch a
math-first surface. It has three jobs:
1. **`validate-schemas`** — compiles every schema under
`shared-data/schemas/`, validates every tracked DeepSeek receipt, runs the
validator's own self-tests, validates `claims.yaml`, and finally re-runs
the canonical emitter in `--verify-only` mode against every receipt to
re-check `answer_sha256` against the answer file bytes on disk. This is
the AGENTS.md contract for promoted Ollama/DeepSeek review receipts.
2. **`require-evidence`** — runs only on PRs and invokes
`scripts/math-first/require_math_evidence.py --from-git-diff
origin/<base>` to enforce the same evidence rule at PR scope that the
pre-commit hook enforces at commit scope.
3. **`pre-commit`** — runs every pre-commit hook against the PR's range of
changed files (`pre-commit run --from-ref <base> --to-ref HEAD`), so the
guardrails are honoured even when a contributor has not installed the
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
verification comments; nothing here replaces it.
## MCP Servers for AI-Assisted Math
[`.mcp.json`](../.mcp.json) declares the math-first tool surface that
Claude Desktop, Devin, and other MCP-aware clients should advertise when
working in this repo. Each server is intentionally **gated on a runtime
environment variable**, so the config itself never carries secrets and
contributors who have not provisioned a backend simply skip it.
| Server | Purpose | Runtime requirement |
|--------|---------|---------------------|
| `filesystem` | Read/write proof artifacts, Lean kernels, receipts. | `npx`, scope pinned to repo root. |
| `sympy` | Local SymPy bridge for symbolic verification of arithmetic claims. | `uv tool run sympy-mcp` (`sympy-mcp` upstream). |
| `wolfram-alpha` | Wolfram Alpha verification for the formulas policed by `wolfram-verification.yml`. | `WOLFRAM_ALPHA_APPID`. |
| `lean` | Lean 4 / Mathlib typecheck bridge against `0-Core-Formalism/lean/Semantics/lakefile.toml`. | `elan` on PATH with `leanprover/lean4:v4.30.0-rc2`. |
| DeepSeek review | Use `5-Applications/tools-scripts/llm/ollama_deepseek_review_emitter.py` directly; no MCP server is currently advertised for it. | `OLLAMA_API_KEY` for non-local endpoints. |
To use these from Claude Desktop, point its `claude_desktop_config.json` at
the repo root or copy the relevant entries verbatim. Secrets live in the
shell/env, never in the config.
## Workflow: adding a new claim
1. Land the natural-language claim in `claims.yaml` with `status: conjecture`.
2. Produce a DeepSeek review via the canonical emitter. Commit both the
answer markdown and `*.receipt.json`; promote `status` to
`verified-by-ai` in the same commit. The pre-commit `require-evidence`
gate now finds a receipt alongside any math-track edit, and the schema
validator confirms the receipt parses.
3. When a Lean proof lands under `0-Core-Formalism/lean/Semantics/`, promote
`status` to `formally-proven` and set `lean:` to the proof's source path.
4. On external publication, promote `status` to `published` and add the
citation to `sources:`.
## Workflow: editing a math-track file
The math-first surfaces are:
* `0-Core-Formalism/lean/Semantics/...`
* `6-Documentation/docs/distilled/...`
* `shared-data/data/stack_solidification/...`
Any commit touching one of these surfaces must, in the same commit, touch
one of:
* `shared-data/artifacts/deepseek_review/...` (new receipt + answer file)
* `0-Core-Formalism/lean/Semantics/...` (Lean change in the same commit
counts as evidence — Lean is the source of truth)
* `claims.yaml` (registry update)
The pre-commit hook and CI both enforce this. To bypass intentionally — for
example, a typo fix in a distilled doc with no semantic change — commit with
`git commit --no-verify` and explain the bypass in the PR description; CI
will still flag the PR and the maintainer can apply the
`math-first-exempt` label (one-off override).
## Verifying everything in one shot
```bash
# Schemas + receipts + claims + emitter --verify-only
uv run --python 3.11 \
--with "jsonschema>=4.21" --with "rfc3339-validator" --with "PyYAML" \
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"; \
done
'
```
If any of the above fails, the corresponding PR will not merge.
Reference in a new issue View git blame Copy permalink