Expected standard (the "full circle"): a formal-verification asset should be (1) wired into CI, (2) gating — not continue-on-error — so a regression actually blocks the merge, and (3) complete — no sorry/axioms standing in for proofs. When any link is missing, the proof exists but cannot stop a regression, so the loop is open. Maybe there is a reason here; if so it should be documented — otherwise it should follow the standard.
Found: proofs/Proofs/Scheduling/{EDF,RMBound,RTA}.lean are complete (0 sorry) real-time scheduling proofs — but no workflow builds or checks them (no lake/Lean job in .github/workflows/). They can silently break on a Lean/Mathlib bump with nothing catching it.
Recommend: add a lake build (+ check) job for proofs/ and gate it. These are high-value, finished proofs — they deserve to be protected.
Context: kiln is planning a no_std/no-alloc cooperative async scheduler and these EDF/RM/RTA proofs are a direct reuse target for verifying its real-time properties — keeping them green matters beyond spar.
Expected standard (the "full circle"): a formal-verification asset should be (1) wired into CI, (2) gating — not
continue-on-error— so a regression actually blocks the merge, and (3) complete — nosorry/axioms standing in for proofs. When any link is missing, the proof exists but cannot stop a regression, so the loop is open. Maybe there is a reason here; if so it should be documented — otherwise it should follow the standard.Found:
proofs/Proofs/Scheduling/{EDF,RMBound,RTA}.leanare complete (0sorry) real-time scheduling proofs — but no workflow builds or checks them (nolake/Lean job in.github/workflows/). They can silently break on a Lean/Mathlib bump with nothing catching it.Recommend: add a
lake build(+ check) job forproofs/and gate it. These are high-value, finished proofs — they deserve to be protected.Context: kiln is planning a
no_std/no-alloccooperative async scheduler and these EDF/RM/RTA proofs are a direct reuse target for verifying its real-time properties — keeping them green matters beyond spar.