Fix Kani version parsing in install script - #58
Conversation
`kani --version` reports versions as:
Kani Rust Verifier <version> (<invocation>)
so `awk '{print $2}'` extracts `Rust` instead of the version. Kani
0.33.0, which this repository uses as its pinned older-version test,
already used this output format.
Parse the version from the `Kani Rust Verifier` line explicitly and
fail if it cannot be determined. Apply the same parsing to the two
version checks in `test-action.yml`.
|
Thanks for digging into this, and apologies for the slow review. The underlying bug is real and this is an important fix — the action is currently broken for everyone on The 0.33.0 claim doesn't hold
0.33.0 emits that string as the banner at the start of a verification run, but not for
Kani 0.68.0 is where this changed, via model-checking/kani#4466: So Since Suggestioninstalled_version=$(
kani --version |
sed -nE 's/^(Kani Rust Verifier|kani) ([^[:space:]]+).*/\2/p' |
head -1
)Verified against captured output for Two smaller things
I've pushed a branch with all of the above on top of your diagnosis if it's easier to pull from: I'm happy either way, and glad to keep your commit as the base since the Context worth recording
|
|
Branch name, for reference: |
The custom `--version` handler is new in Kani 0.68.0: `args/mod.rs` sets
`disable_version_flag = true` and `main.rs` calls `print_kani_version`.
Through 0.67.0, `--version` was clap's derived flag from
`#[command(version, name = "kani", ...)]` and printed
kani <version>
`print_kani_version` existed back then too, but only the verification
paths reached it, so it was a run banner rather than `--version` output.
Checked 0.60, 0.63, 0.65, 0.66, 0.67 and 0.68: `disable_version_flag`
appears only at 0.68.0.
Parsing just the `Kani Rust Verifier` line therefore fails for every
version up to 0.67.0, including the pinned 0.33.0 test case, which is
what CI reported:
[5/5] Successfully completed Kani first-time setup.
##[error]Could not determine installed Kani version
`kani-version` accepts any published version, so accept both formats.
Anchor on the program name instead of line 1, since `kani` prints
first-time setup progress ahead of the banner when setup is incomplete.
Drop the `if [ $? -eq 0 ]` guard around the comparison: `$?` there is the
status of the preceding assignment, that is of the command substitution,
so it never guarded the parse. The empty check above covers that now.
Report both versions in the mismatch error, since the old message made
this failure needlessly hard to diagnose, print the requested version
instead of the unset `$VERSION` on the `latest` path, and re-anchor the
`cargo search` grep, verified against `cargo search kani-verifier`
output.
`cargo search` output is colored in CI: the Rust toolchain action exports
CARGO_TERM_COLOR=always via $GITHUB_ENV, which applies to every later
step in the job, and cargo honors it even when stdout is a pipe. The line
arrives as
\e[1m\e[32mkani-verifier\e[0m = "0.68.0" # ...
so `grep '^kani-verifier '` never matches, `requested_version` is empty,
and the `latest` path fails the comparison it is meant to pass:
The version of Kani installed (0.68.0) was different than the one requested ()
This is why 2534b7a dropped the anchor. Keep the anchor, which also
avoids matching unrelated crates whose descriptions mention Kani, and set
CARGO_TERM_COLOR=never for the lookup instead. Reproduced both the
failure and the fix against `cargo search kani-verifier`.
Fail loudly when the lookup yields nothing, rather than comparing against
an empty string. Keeping the comparison on the `latest` path is
deliberate: it is what catches `cargo install` leaving an older binary in
place, for instance when a runner image already ships Kani.
PropProof relied on a cargo `paths` override pointing at
`model-checking/kani` branch `features/proptest`, whose last commit is
2025-05-13. Its vendored proptest no longer compiles: recent nightly std
added inherent `SIGN_MASK`, `EXP_MASK` and `MANTISSA_MASK` consts on f32
and f64, which collide with proptest's own `FloatLayout` trait consts.
That fires `unstable_name_collisions`, a member of the
`future_incompatible` group that `proptest/src/lib.rs` puts under
`#![forbid(...)]`, so 16 sites in `proptest/src/num.rs` fail to build:
error: an associated constant with this name may be added to the
standard library in the future
--> propproof/proptest/src/num.rs:607:21
|
607 | $typ::SIGN_MASK
Fixing that belongs on the upstream branch, not here, and nothing has
maintained it for over a year. Anyone passing `enable-propproof: true`
today already fails this way, so remove the input, the two steps that
set up the override, the workflow test, its fixture crate, and the
README section rather than carry a lint workaround for a feature that no
longer works.
This drops a documented input. GitHub only warns on unknown inputs to a
composite action, so existing workflows keep running; they lose a feature
that is already broken for them.
|
Thanks for correcting me & glad I could help |
2 participants
Description of changes:
install-kani.shextracts the installed Kani version withawk '{print $2}'. Kani reports its version asKani Rust Verifier <version> (<invocation>), so field 2 isRust, not the version number. Newer Kani releases may also print aCBMC <version>line, making the parsed value multi-line.This is not caused by the additional CBMC output: Kani 0.33.0, which this repository uses as its pinned older-version test case, already emitted
Kani Rust Verifier 0.33.0 (standalone).This PR parses the version explicitly from the
Kani Rust Verifierline, reports an error if no version can be determined, and applies the same fix to the two version checks intest-action.yml.Resolved issues:
N/A
Related RFC:
N/A
Call-outs:
N/A
Testing:
The existing workflow exercises both Kani 0.33.0 and the latest version. Both checks now use the corrected parser.
Also verified locally against Kani 0.68.0 output containing the additional CBMC version line.
This is not a refactor.
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.