Repository navigation
ci-kani: run the Kani lane for PRs touching crates/mlog and crates/minvmd #2075
Description
.github/workflows/ci-kani.yml only runs the Kani lane for PRs that touch certain paths. crates/mlog and crates/minvmd are not among them, so a PR that changes an mlog or minvmd harness (or the code they prove: the telemetry switch decision, the spool prune plan, the guest boot-line budget) never runs Kani on the PR. Main pushes still run it.
Ask: add crates/mlog/** and crates/minvmd/** to the workflow's path filter. Workflows are frozen, so this needs a person.
Cost, measured on a 16 GB cap with swap off (spec 25 stack, 2026-10-07): the minvmd harnesses are 5 of 5 in 122 s cold, 5.55 GB peak (42 s and 1.67 GB warm); the mlog harnesses add 9. The whole scripts/kani.sh (27 harnesses) peaks at 12.32 GB, from the existing sessions harnesses, with no OOM.
Referenced from spec 25 (#1988) and the Kani lane test in #1989.
Activity