# Scripts Index
A one-line per script index of the 8 shell scripts in `scripts/`.
Grouped by purpose (theorem checks, doc / changelog checks, lean
check, paper-artifact regeneration, doc-vs-reality consistency,
health check).
## How to run all checks
```bash
bash scripts/health_check.sh
```
`health_check.sh` is the one-command entry point that runs the
3 observability examples + `cargo fmt --check` + `cargo build
--offline` + `cargo test --offline --test theory_release_gate` +
2 syntax checks. Exits 0 always; prints
`tokitai_health: N of 8 checks passed`.
## Theorem checks (2)
These scripts verify that the Lean-side theorem and the
finite-sheaf-gluing theorem are consistent with the Rust-side
property-based tests. Both scripts write a
`target/tokitai-*-theorem-evidence.txt` artifact that the
release-gate tests consume.
- `check_padic_valuation_skip_theorem.sh` — checks the
p-adic valuation-skip theorem (`docs/padic_valuation_skip_theorem.md`).
Verifies that the `PadicDomain::Q_5[3]` planner policy
discharges the same obligations as the Lean-side theorem.
- `check_finite_sheaf_gluing_theorem.sh` — checks the finite
sheaf gluing theorem (`docs/finite_sheaf_gluing_theorem.md`).
Verifies that the `Cover` + `SectionTable` glue-check
reports the same `all_succeeded` as the Lean-side theorem.
## Doc / changelog checks (2)
These scripts verify that the documentation and changelog
hygiene invariants added in the P401-P415 and P416-P420
batches hold. Both are wired into `.github/workflows/ci.yml`
as pre-merge checks and exit 1 on the first missing item.
- `check_dev_docs.sh` — checks the 5 P401-P415 doc files
(`tests/README.md`, `scripts/README.md`,
`docs/development/local_dev_setup.md`,
`docs/development/ci_debugging.md`,
`docs/development/whatsnew.md`) all exist and are non-empty.
- `check_changelog_sections.sh` — checks the
Keep-a-Changelog structure of `CHANGELOG.md` (`## [Unreleased]`
+ `### Added` / `### Changed` / `### Non-Claims` subsections).
## Lean check (1)
The optional Lean-side check. Requires the `lean` toolchain on
the local machine. Default behavior is a 20-second timeout;
if the toolchain is not available, the script reports
`lean_version_unavailable` and continues (fail-soft).
- `optional_lean_check.sh` — runs the actual `lean` compiler on
`lean/Tokitai/Ultrametric.lean` and verifies the proof
skeleton parses + type-checks. CI runs this on every PR.
## Paper-artifact regeneration (1)
The paper-artifact regeneration script. Re-runs the
`paper_benchmarks` example and records the pre/post SHA-256 of
every `target/paper-results/*` file. The diff is informational
(not a failure signal), because the regenerated artifacts
include timestamps.
- `regenerate_paper_artifacts.sh` — wrapper around
`cargo run --example paper_benchmarks`. Records the
pre/post SHA-256 of every paper-results file. The CI
workflow syntax-checks the script (it does not run it, since
the artifacts are committed and reviewers regenerate
locally).
## Doc-vs-reality consistency (1)
The P416-P420 doc-drift guard. Asserts the counts cited in the
top-level README/index files match the actual filesystem state.
- `check_doc_consistency.sh` — 4 checks: `tests/README.md`'s
"N test files" matches `ls tests/*.rs | wc -l`;
`examples/README.md`'s "17 standalone examples" matches
`ls examples/*.rs | wc -l`; `scripts/README.md`'s "7 shell
scripts" matches `ls scripts/*.sh | wc -l`; `CLAIMS.md` has
exactly 8 `*_claim_allowed` lines. Exits 1 on the first
mismatch with a clear error message.
## Health check (1)
The one-command health check. Wraps the 3 observability
commands + 5 software-only checks in a single script.
- `health_check.sh` — runs 8 checks, prints
`tokitai_health: N of 8 checks passed`. Exits 0 always
(informational). Supports `TOKITAI_HEALTH_SKIP_BUILD=1`
for fast iteration.
## How to add a new script
When adding a new release-gate or observability check:
1. Decide which bucket it belongs in (theorem, doc / changelog,
lean, paper, doc-vs-reality, health).
2. Use the `set -eu` (or `set -u`) header for fail-fast
behavior; the existing scripts follow this convention.
3. Print a one-line `==` banner at the start so the output is
greppable.
4. If the script writes a target artifact, name it
`target/tokitai-*-evidence.txt` so the release-gate tests
can find it.
5. Add a one-line entry to this README in the appropriate
bucket, and bump the bucket count and the top-line "N
shell scripts" count if needed. The
`check_doc_consistency.sh` CI step (P419) asserts the
documented count matches `ls scripts/*.sh | wc -l`.