diff --git a/rfc/src/rfcs/0008-kani-version.md b/rfc/src/rfcs/0008-kani-version.md new file mode 100644 index 000000000000..ebc2b39da4bd --- /dev/null +++ b/rfc/src/rfcs/0008-kani-version.md @@ -0,0 +1,109 @@ +- **Feature Name:** Print Kani version (`kani-version`) +- **Feature Request Issue:** +- **RFC PR:** +- **Status:** Under Review +- **Version:** 0 + +------------------- + +## Summary + +Print the version of Kani at the beginning of a run. + +## User Impact + +Many programs print their version at the beginning of a run. +The version of a program communicates the state of the software at a given point (e.g., features that are available or performance on particular problems). +At present, Kani does not print its version, but it's something we should strongly consider from now on. + +There are many benefits to including the version of Kani in its output. +However, I think the main ones will be the following: + * **Earlier detection of version-related discrepancies**: + Users are likely to discuss discrepancies in verification outcomes by looking at Kani's output. + These may look exactly the same[^cbmc-version] (except for the discrepant value) on two different versions of Kani. + Including the version will help users realize sooner that they're using different versions of Kani. + * **Simpler issue triaging**: + New issues require users to post the Kani version they used. + Getting this information requires another call with `--version`, which wouldn't be needed if we simply printed the version. + Also, note that users may need to do more work if they aren't running Kani locally (e.g., Kani running in CI). + +In addition, printing the Kani version may be useful for other purposes (automate CI processes, help users realize they're using outdated versions, etc.). + +## User Experience + +The first line printed in any Kani invocation (either through `kani` or `cargo kani`, and regardless of subcommands) will inform users of the version. +The behavior will be extended for development versions, where it'll print the short hash of the HEAD commit in addition to the version. + +### Release versions + +The first line to be printed will be: + +``` +Launching the Kani Rust Verifier +``` + +where `` is the version of Kani under use, which follows the semantic versioning format `MAJOR.MINOR.PATCH`. + +For example, for the release version of [Kani 0.29.0](https://github.com/model-checking/kani/releases/tag/kani-0.29.0), this would have printed: + +``` +Launching the Kani Rust Verifier 0.29.0 +``` + +### Development versions + +The first line to be printed will be: + +``` +Launching the Kani Rust Verifier (dev. version - commit: ) +``` + +where `` is the version of Kani under use, which follows the semantic versioning format `MAJOR.MINOR.PATCH`, +and `` is the short hash (i.e., 7 hexadecimal digits with format `hhhhhhh`) of the `HEAD` commit. + +For example, for the development version of [Kani 0.29.0](https://github.com/model-checking/kani/releases/tag/kani-0.29.0), this would have printed: + +``` +Launching the Kani Rust Verifier 0.29.0 (dev. version - commit: e4f989b) +``` + +## Detailed Design + +The implementation will require additions to the `kani-driver` module. + +Printing the short hash of the `HEAD` commit would require `git` as a dependency, but it can be made optional if we print `unknown` in the case where `git` isn't available. + +## Rationale and alternatives + +It's possible to argue that Kani shouldn't print its version because other (related) tools don't (e.g., `rustc`). +However, many of those tools are expected to NOT produce any output when all went well (i.e., no errors nor warnings when compiling a program). +This isn't something we expect Kani to do though: it'll always produce some output to inform users about the verification results. + +In my experience, we should print the version because users and developers use text-based log files containing Kani's output to discuss verification results. +In some cases, we've had to "calculate" the Kani version from the CBMC versions appearing in the log. +But we shouldn't need to in the first place. + +### Style alternatives + +It'd be great to discuss any alternatives for the concrete format. +At some point, I even thought about adding some ASCII art, but wanted to keep it short and simple. + +For example, we could: + - Replace the word `Launching` with another one. + - Prefix the version with `v` (so the version gets printed as `v0.29.0`, for example). + - Just print `Kani Rust Verifier `, nothing else. + +These are low-level details which I'd love to discuss with you all. + +## Open questions + +I'm hoping that we can answer the following questions during the RFC: + 1. Do we want to print Kani's version? + 2. If we decide to move forward, what's your preferred style? + +## Future possibilities + +No future possibilities are under consideration. + +[^cbmc-version]: The CBMC version is printed once for each harness. +That'd be the main difference between outputs from different versions, but only if the CBMC version was bumped in between.