[Amaury Chamayou (achamayou)]

Motivation

Simplify CCF-Raft verification by checking its library and replay executable together, rather than rewriting lakefile.toml and running a separate kernel check for each target.
This removes a redundant verification invocation over overlapping dependencies and aligns Raft with the other packages, without dropping verification coverage.

This is a simplification and deduplication, not a demonstrated wall-time speedup.
The historical main-based run took 44m52s for Check packages and 53m24s for the full models job; this PR's run took 52m30s and 65m34s respectively.
Cache restoration also differed: 4m33s historically versus 7m32s on this PR.
These separate runs are not a controlled A/B comparison and establish neither a speedup nor a regression attributable to this change.
See the historical Lean CI run for merged #8633 and this PR's Lean CI run.
Any elapsed-time saving remains unmeasured pending a controlled comparison.

This is a standalone follow-up to #8339, based on main and not stacked on that KV PR.

Implementation summary

Run lake check --inadvisably-no-sandbox once per package, using the existing CCF-Raft default targets CCFRaft and ccfraft-replay together.
Remove the Raft-specific temporary configuration rewrite and restoration logic.
Update CCF-Raft validation documentation to describe the combined check.
This does not address repeated dependency verification across different packages.

Safety and compatibility

The Lean CI run passed.
Both default targets remain checked.
The warning-as-error build, kernel verification, standard axiom allowlist, import-coverage and architecture checks, linting, and fixture validation are retained.
This CI-only change has no runtime or compatibility impact.

[Copilot]

🟢 Approval recommended

No active review issues remain for the Lean CI simplification and accompanying documentation updates.

No open issues 🎉

What changed in this PR

This PR simplifies CCF’s Lean CI by checking both Raft default targets in one invocation, avoiding a repeated kernel and axiom check. The expected runtime improvement is not yet measured.

Changes:

• Replace Raft-specific per-target checks with one lake check --inadvisably-no-sandbox call per package.
• Update validation documentation to describe the combined check of CCFRaft and ccfraft-replay.

Custom instructions used

Applied the CCF repository guidance supplied in the review context; no additional instruction files were loaded.

File	Description
lean/​ccf-raft/​replay/​README.md	Describe library and executable roots being checked together.
lean/​ccf-raft/​README.md	Document one kernel-check invocation covering both default targets.
.github/​workflows/​lean.yml	Remove temporary target rewrites and the separate Raft check loop.

_{Review effort: Balanced}