kani-verifier tracking issue

[tedinski]

Followups to #1039

Critical or urgent:

• Create a licenses-note.txt file in our release bundle, and verify we're good to go on all licensing requirements.
• Rename src/cargo-kani to src/kani-driver. Integrate kani-verifier into the workspace instead of having to keep it separate because of conflicting binary names.
• Make kani-verifier the top-level crate in our repo, with all other crates being in its workspace underneath it. Resolves problem of having a README in this crate.
• kani-verifier: cargo-kani setup support for macos #1036
• Make a kani-0.1.0 test release #1037
• Check the customer's target-triple and verify it's supported by Kani before we do anything.

Eventual:

• Consider adding hash-checking as part of the download.
• Checking of system dependencies/versions as part of first-time setup. (python3, pip, rustup, curl/tar, ctags)
• We need a single source of truth for our dependency versions. For python packages, we currently duplicate this information into kani-verifier and also in our CI setup scripts. For CBMC, we're pulling from PATH instead of downloading it correctly.
• Refactor some of the command line helpers I wrote so they're not duplicated. (By having other tools depend on kani-verifier where it lives?)
• Ability to control verbosity of Kani first-time setup output.
• Handle upgrading/uninstalling Kani. Remove old Kani release bundles and Rustup toolchains.
• Parallelize the dependency install process. No reason we can't pip install while we rustup toolchain install and while we download the release bundle. (edit: except that we don't know the necessary rust toolchain until we've downloaded the release bundle... a more compelling reason to find a way to fix this.)
• Can we install a more minimal profile of the rust toolchain to minimize download size?

[Kixunil]

I noticed kani setup calls curl which isn't present on all systems. Would it be too much to depend on reqwest to avoid having to deal with that dependency?

[tedinski]

It would be too much by default I think: we're really trying to keep the number of dependencies and build time for the kani-verifier crate to an absolute minimum.

I think this would be acceptable as an optional feature? (I'm not sure how cargo install reacts to features that aren't enabled, but if a normal install wouldn't pull down all the dependencies, but cargo install kani-verifier --locked --features downloader did, that would be ok.)

Out of curiosity, what platform is this an issue with? I really expected Python to be the bigger problem, curl seems required by the default way of getting rustup even, so I previously thought it wouldn't be an issue! :)

[Kixunil]

Yeah, I see the point. Disabled features are not compiled at all, IIRC not even downloaded. So optional feature could be fine.

what platform is this an issue with?

Actually even something quite popular: Debian stable. It has wget by default though.

curl seems required by the default way of getting rustup

Not really, one can use wget -O - https://sh.rustup.rs | sh - just fine.

What I wanted to say is falling back to wget if curl isn't present would be really great.