-
-
Notifications
You must be signed in to change notification settings - Fork 0
ci(proofs): build verification/proofs/ in CI — nothing runs just proof-check-all #57
Copy link
Copy link
Open
Labels
cicdCI/CD: workflows, actions, lockfiles, pins, runners, release gatesCI/CD: workflows, actions, lockfiles, pins, runners, release gatesfeeds:valence-shellFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes thereFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes therepriority:p2Normal - queue itNormal - queue itproofsFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debtFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debtscope:repoConfined to this repositoryConfined to this repositorystatus:readyFully specified and ready to be picked upFully specified and ready to be picked up
Description
Activity
Metadata
Metadata
Assignees
Labels
cicdCI/CD: workflows, actions, lockfiles, pins, runners, release gatesCI/CD: workflows, actions, lockfiles, pins, runners, release gatesfeeds:valence-shellFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes thereFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes therepriority:p2Normal - queue itNormal - queue itproofsFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debtFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debtscope:repoConfined to this repositoryConfined to this repositorystatus:readyFully specified and ready to be picked upFully specified and ready to be picked up
Per OQ-001's resolution (#56),
verification/proofs/is the canonical content of this repo's "verification host" role — but no CI workflow runs it, so the proofs are asserted, not enforced (thejust proof-check-allrecipe exists but is never invoked by CI).Add a proof-CI job that builds each prover layer:
verification/proofs/idris2/**(viajust proof-check-idris2)EchoTyping.agda/Verification.agdadepend on it); see echo-types' own CI for the stdlib-2.3-from-source patternApiTypes.leanTypeSafety.vStateMachine.tlaSHA-pin the setup actions. This makes the coordinator's verification-host identity enforced rather than asserted, and is the natural next step after the OQ-001 cleanup.
https://claude.ai/code/session_01GJatEm2TVFSTBEkKXmserJ