ci: skip heavy jobs on artifacts/docs-only diffs

[avrabe]

Why

Every PR — including one that edits a single line of rivet YAML — runs Kani, Miri, mutation testing, fuzz smoke, Bazel, coverage and a Mathlib lake build. That is hours of self-hosted runner time buying nothing: a diff confined to artifacts/*.yaml, safety/, docs/ or markdown cannot change a proof, a mutant, a fuzz target or a Miri run.

What

A changes job in ci.yml and proofs.yml classifies the PR diff once; 13 expensive jobs consume its output.

always run	gated on code == 'true'
Detect changed paths, Format, Security Audit (RustSec), Cargo Deny, Rivet validate (artifacts)	Clippy, Test, Codegen compile oracle, Bench compile smoke, Code Coverage, Miri, Proptest (extended), Mutation Testing, Fuzz smoke, Supply Chain (cargo-vet), Bazel test, Kani BMC, Lean proof typecheck

fmt / audit / deny / rivet-validate stay ungated: they are cheap, and rivet-validate is precisely the check an artifacts-only PR must pass.

The load-bearing detail

The jobs are skipped, never removed. A job-level if: reports a skipped conclusion, which satisfies a required status check, so the 14-context branch-protection gate stays non-empty and intact. Filtering at the workflow level (on: paths:) would instead leave those required checks permanently pending and block every merge. The ci.yml comment states this explicitly, because the distinction is exactly the kind of thing a later "simplification" removes.

Fail-safe direction is toward code: an allow-list names the non-code paths and anything outside it counts as code, so a new top-level path runs the full suite until it is deliberately allow-listed. A mixed diff (artifacts and Rust) classifies as code — the gate counts non-matching files rather than grep -q-ing matching ones, so the decision is both explicit and readable in the job log. Non-PR events (push to main, tags, schedules) always run everything.

Verification

The filter was exercised against 12 hand-built diffs in bash (CI's shell) — artifacts-only, multi-artifact, root markdown, nested markdown, docs/, safety/, Rust, mixed, workflow, manifest, Lean, non-yaml artifact. All 12 classify as intended.

This PR touches .github/**, so it classifies as code and runs the full 14-check suite — which is the correct self-test of the gate. The next artifacts-only PR is what empirically confirms the skip path.

Follow-up required after merge (do not skip)

If the changes job itself fails (runner error, checkout failure), GitHub skips its dependents for dependency-failure — also reported as skipped, which would satisfy all required checks with zero tests run. Closing that hole means adding Detect changed paths and Detect changed paths (proofs) to the required contexts (14 → 16). That must happen after this merges, since a required context that no run reports would leave existing PRs pending; open PRs then need a branch update.

🤖 Generated with Claude Code

[github-actions]

Rivet verification gate

✅ 20/20 passed

	count
Passed	20
Failed	0
Skipped (no steps)	0

Filter: (and (= type "feature") (or (has-tag "v093") (has-tag "v0100")))

Failed artifacts

(none)

_{Updated automatically by tools/post_verification_comment.py. Source of truth: artifacts/verification.yaml.}

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!