model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.11k stars 83 forks source link

Simplify installation #2832

Open stefnotch opened 10 months ago

stefnotch commented 10 months ago

Requested feature: Kani currently has Python as a dependency (on Windows and other not-directly-supported OSes at least). And Kani also has the following dependencies. Since that adds dependencies that are not automatically installed by Cargo to a Rust project, it'd be worthwhile to improve this sometime in the future.

Use case: If I develop an open source library, then I want it to be as easy as possible for people to contribute to it. cargo run is amazing in that regard. Saying "install Python if you're on Windows" is obviously less beautiful, especially considering how un-fun Python installations on Windows can be.

Solution ideas:

And of course I wouldn't request this feature anytime soon. I'd just love it if the team were to consider it at some unspecified point in the far future, when Kani is becoming even more popular!

celinval commented 10 months ago

Hi @stefnotch, thank you for the issue. Another possibility would be to make the --visualize feature optional. That is the only reason we depend on Python today.

celinval commented 2 months ago

We're now deprecating --visualize and we will soon remove the python dependency. :smiley:

stefnotch commented 2 months ago

That's amazing, I look forward to verification tools being more accessible! It is insanely nice when the entry barrier is as low as possible, because it makes it so much easier to kani to certain projects, without causing a lot of extra effort for other contributors.