| Filename | Latest commit message | Latest commit date |
|---|---|---|
ebe9985a82
All checks were successful
wai formal verification (integer core) / does this change touch it (pull_request) Successful in 9s
wai formal verification (integer core) / every harness in one shard (pull_request) Successful in 26s
wai formal verification (integer core) / kani (stage) (pull_request) Successful in 2m30s
wai formal verification (integer core) / kani (plan) (pull_request) Successful in 8m7s
wai formal verification (integer core) / kani (integer-core) (pull_request) Successful in 6m0s
wai formal verification (integer core) / kani (sound) (pull_request) Successful in 9m22s
wai formal verification (integer core) / kani (arith) (pull_request) Successful in 9m53s
wai formal verification (integer core) / kani (stage-long) (pull_request) Successful in 18m18s
wai formal verification (integer core) / kani (isqrt512) (pull_request) Successful in 29m45s
wai formal verification (integer core) / kani (rans64-t2) (pull_request) Successful in 13m41s
standards workspaces build + test / which workspaces this change touches (pull_request) Successful in 10s
standards workspaces build + test / macOS energy backends (pull_request) Has been skipped
repository checks / lockfiles, advisories, tests in CI, workflow hygiene, spec and section references, public text (pull_request) Successful in 3m42s
The move to `macos-proofs` left a condition behind. `Cache Kani toolchain` was skipped by `matrix.os != 'macos'`, and the comment above it gives the reason: those runners execute on the host, so `~` is the host's own home, where Kani is already installed, and a restore writes over a live install. `macos-proofs` is a second such host, and `!= 'macos'` is false for it, so the step would have run there -- and `runner.os` is `macOS` on both, so the two hosts would also have been sharing one cache key, each saving its own install over the other's. The test is now a prefix, `!startsWith(matrix.os, 'macos')`, which is what the comment always meant. Kani 0.67.0 is installed on that host: `cargo-kani 0.67.0`, with `~/.kani/kani-0.67.0/bin/kani-driver`, `bin/cbmc` and `toolchain/bin/rustc` all present, which is exactly the three-way test the `Install Kani` step skips on. So the shards find a prover and do not fetch one. Two things this run will also test that the last one could not, because it never reached a step: the proofs host's own provisioning, and whether these harnesses fit its 96 GB. Co-Authored-By: Claude Opus 5 <[email protected]> |
||
| .. | ||
| workflows | ||