[johnchandlerburnham]

fix(bench): pass --allow-declined in ooc whole-env check-lean benchmark

Summary

Fixes the failing ooc-InitStd-execute, ooc-Lean-execute, and ooc-Mathlib-execute jobs in bench-main.yml after PR #677 switched ooc from ix check-rs to ix check-lean (IxC).

Background & Problem

ix bench run --backend ooc runs two ix check-lean passes per environment:

1. A whole-environment record check (ix check-lean <ixe> --anon --json <out> --json-name <env> --per-const <out>.perconst.csv).
2. A per-constant full-closure check over the selected benchConstants (ix check-lean <ixe> --anon --consts-file <namesFile> --json <out>).

While all per-constant rows pass with "status": "ok", upstream Lean libraries (InitStd.ixe, Lean.ixe, Mathlib.ixe) contain declarations outside IxC's fragment that receive outcome == "decline" (and dependents that receive outcome == "blocked"), with 0 kernel rejections (outcome == "reject"):

• InitStd.ixe (99,519 subjects): 99,514 pass (922 typed), 0 reject, 5 decline/blocked (Lean.trustCompiler + its 4 native-eval dependents).
• Lean.ixe (173,337 subjects): 173,250 pass (3,415 typed), 0 reject, 87 decline/blocked (the 5 InitStd subjects + 5 unsafe inductive blocks + 7 unsafe defs whose type check requires unfolding a tier definition + their blocked dependents).
• Mathlib.ixe (~672,938 constants): imports Init, Std, and Lean, inheriting the same decline/blocked set with 0 reject.

Because default ix check-lean treats any !success outcome (decline, blocked, or reject) as a refusal (exit 3, "status": "rejected"), the whole-env row was written with "status": "rejected", causing ix bench run's final gate to fail with exit 3 and ix bench bmf to drop the whole-env row.

Solution

• Ix/Cli/CheckLeanCmd.lean:
  • Add --allow-declined (CheckCfg.allowDeclined) and CheckReport.hasReject (r.targets.any (·.outcome == "reject") || r.rows.any (·.outcome == "reject")).
  • Under --allow-declined, check-lean runs in record-check mode: it tolerates decline and blocked outcomes (when no target or support record in the closure has outcome == "reject"), skips checkWhole whole-artifact admission, rejects --host-out / --host-store with exit 2, and still fails with exit 3 ("status": "rejected") on any genuine kernel or reader reject.
  • Default strict ix check-lean behavior and exit codes (0, 2, 3, 4, 5) are unchanged.
• Ix/Cli/BenchCmd.lean:
  • Pass --allow-declined on ooc's whole-env ix check-lean invocation while keeping the per-constant --consts-file closure runs strict.
• Tests/Ix/Kernel/CheckLeanCli.lean & docs/:
  • Add CLI test controls for --allow-declined (decline/blocked rows marked ok, reject still exits 3 / rejected, unbound whole run skips whole-artifact admission and exits 0 / ok, and --host-store exits 2) and document the flag in docs/kernel.md and docs/benchmarking.md.

Verification

• IxTests bench-measures kernel-check-lean-cli (24 process controls passing).
• ix bench run --backend ooc --env InitStd --mode execute --ixe ./InitStd.ixe + ix bench bmf (exits 0; all 8 rows status: ok and emitted to BMF).
• ix bench run --backend ooc --env Lean --mode execute --ixe ./Lean.ixe + ix bench bmf (exits 0; both Lean and Lean.Json rows status: ok and emitted to BMF).