kani icon indicating copy to clipboard operation
kani copied to clipboard

crates.io stub and docs.rs documentation

Open GrigorenkoPV opened this issue 2 years ago • 3 comments

I really wish it was possible to view documentation for kani-the-lib, the one that provides all the any, assume, and proof stuff. However, since the kani crate on crates.io is a stub, docs.rs doesn't have any useful documentation.

So now if I want to read the docs, I have to

cd $KANI_HOME/kani-0.46.0/library/kani
cargo +nightly doc

which is not that convinient.

Could you please consider publishing an actual version of the lib to crates.io? If the reason for having it as a stub is to prevent users from downloading the wrong thing, maybe adding something like

#[cfg(not(docs)]
compile_error!("This is an internal crate. You were probably looking for `kani-verifier` instead.");

to the published version could be used?

GrigorenkoPV avatar Feb 14 '24 21:02 GrigorenkoPV

Hi @GrigorenkoPV. Thanks for opening the issue. The documentation for the Kani library is currently available here:

https://model-checking.github.io/kani/crates/doc/kani/

This can be accessed from the Kani documentation page:

https://model-checking.github.io/kani/crates/index.html

We plan to publish the documentation on crates.io once we publish the kani crate.

zhassan-aws avatar Feb 14 '24 22:02 zhassan-aws

Thank you for the response!

The documentation for the Kani library is currently available here: https://model-checking.github.io/kani/crates/doc/kani/

We plan to publish the documentation on crates.io once we publish the kani crate.

Would it be feasible to update the stub in the meantime to feature a link to where the actual documentation can be found?

GrigorenkoPV avatar Feb 15 '24 23:02 GrigorenkoPV

That's a good idea.

celinval avatar Feb 27 '24 16:02 celinval