Lightly revise the rest of the documentation #1396
Conversation
|
|
||
| ## Usage on a single crate | ||
|
|
||
| For small examples or initial learning, it's very common to run Kani on just one source file. |
There was a problem hiding this comment.
Or crates that don't have external dependencies.
docs/src/usage.md
Outdated
|
|
||
| This will ensure that a normal build of your code will be completely unaffected by anything Kani-related. | ||
|
|
||
| Unfortunately, this is still required for code under `tests/` as this code might be built by `cargo test` normally and would still be unaware of the `kani` crate. |
There was a problem hiding this comment.
I don't know what you are trying to say here
There was a problem hiding this comment.
I've revised this paragraph.
I'm getting at "the kani crate isn't yet published in crates.io, so you can't add it as a dev-dependency" without actually saying that. Just mentioning the implications of it.
| When Kani builds your code, it does two important things: | ||
|
|
||
| 1. It sets `cfg(kani)`. | ||
| 2. It injects the `kani` crate. |
There was a problem hiding this comment.
It might be nice if we start at least publishing the crate doc so we can reference here
|
|
||
| Run `cargo kani --help` to see a complete list of arguments. | ||
|
|
||
| ## Usage on a single crate |
There was a problem hiding this comment.
IMO, this should be at the top. It is easier to explain. It should at least come before the common options part.
There was a problem hiding this comment.
That's deliberate. Almost everyone is going to use cargo kani, so that's what I'm talking about first. It's what most customers will care about.
|
|
||
| This conditional compilation with `cfg(kani)` is still required for code under `tests/`. | ||
| (Unlike normal test code, which can unconditinoally make use `dev-depenencies` under `tests/`.) | ||
| When this code is built by `cargo test`, the `kani` crate is not available, and so it would otherwise cause build failures. |
There was a problem hiding this comment.
Can you add a snippet of an example?
There was a problem hiding this comment.
Isn't the code above it an example? I'm not sure what else?
There was a problem hiding this comment.
I meant an example of when [kani::proof] is used under tests/ to clarify why cfg(kani) is needed to not break cargo test.
There was a problem hiding this comment.
I'm still not sure what you mean. But I realized my phrasing was probably still confusing, so I made another revision.
| However, if you plan to integrate Kani in your projects, the recommended | ||
| approach is to use [Kani on a package](./cargo-kani.md) because of its ability | ||
| to handle external dependencies. | ||
| If you plan to integrate Kani in your projects, the recommended approach is to use `cargo kani`. |
There was a problem hiding this comment.
Can we add this sentence back:
This is due to its ability to handle external dependencies and the option add configurations via the Cargo.toml file.
Co-authored-by: Zyad Hassan <[email protected]>
Co-authored-by: Zyad Hassan <[email protected]>
Co-authored-by: Zyad Hassan <[email protected]>
Co-authored-by: Zyad Hassan <[email protected]>
Co-authored-by: Zyad Hassan <[email protected]>
Description of changes:
This is a smattering of revisions to the Kani docs. Most prominently, it collapses "Usage" down to one page instead of having two, and I expand on using
cfga bit there.Resolved issues:
Resolves #1320
Resolves #1390
This completes the last remaining task in that issue.
Call-outs:
Testing:
How is this change tested?
Is this a refactor change?
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.