RFC: Print Kani version #2571
RFC: Print Kani version #2571
Conversation
adpaco-aws
force-pushed
the
rfc-kani-version
branch
from
372a393
to
4f9425a
Compare
| ## 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. |
There was a problem hiding this comment.
I'd even include the branch the commit came from (makes it easier to find) in the development version.
|
|
||
| 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. |
There was a problem hiding this comment.
I we care strongly about being accommodating here, the printing of the version could be a feature flag that is on by default so people can toggle it off in a custom build.
Another option would be to check (e.g. atty) whether the user is running a TTY, and only print the version if it isn't a tty.
| - Prefix the version with `v` (so the version gets printed as `v0.29.0`, for example). | ||
| - Just print `Kani Rust Verifier <version>`, nothing else. | ||
|
|
||
| These are low-level details which I'd love to discuss with you all. |
There was a problem hiding this comment.
I don't feel super strongly about Launching or v, though one might argue they are redundant.
However it might makes sense to print whether it is running the cargo plugin or the standalone Kani. Maybe Kani Rust Verifier (Cargo Plugin) 1.29.0 and vice versa with standalone.
| ## Open questions | ||
|
|
||
| I'm hoping that we can answer the following questions during the RFC: | ||
| 1. Do we want to print Kani's version? |
There was a problem hiding this comment.
Yes. Especially because of the VSCode extension.
| ``` | ||
|
|
||
| where `<version>` is the version of Kani under use, which follows the semantic versioning format `MAJOR.MINOR.PATCH`, | ||
| and `<commit>` is the short hash (i.e., 7 hexadecimal digits with format `hhhhhhh`) of the `HEAD` commit. |
There was a problem hiding this comment.
If we wanted to be super extra we could also print (dirty) if your worktree has uncommitted changes or add a hash for all files in src 😂
|
Also I think the version should be included in the header when printing |
| The first line to be printed will be: | ||
|
|
||
| ``` | ||
| Launching the Kani Rust Verifier <version> |
There was a problem hiding this comment.
Do we need the "the" here?
Agreed, I'll close this RFC and we can continue the discussion in the (to-be-developed) PR. Thanks @JustusAdam for the suggestions, I'll consider them for the implementation! |
Description of changes:
This RFC proposes printing the Kani version at the beginning of a run.
Rendered version available here.
Resolved issues:
Resolves #2570
Testing:
How is this change tested? N/A
Is this a refactor change? N/A
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.