docs: add conc playback docs to getting started tutorial#1537
docs: add conc playback docs to getting started tutorial#1537sanjit-bhat merged 29 commits intomodel-checking:mainfrom
Conversation
celinval
left a comment
There was a problem hiding this comment.
Great job. I added a few comments. Let me know what you think.
|
@celinval I added an example, but I decided to only explain a couple parts of the unit test that I thought would be most relevant to the user. Here, I define relevance as "info that's helpful if the user wants to try a different concrete value without regenerating the unit test". |
celinval
left a comment
There was a problem hiding this comment.
That's great! Minor comments but not blockers.
|
|
||
| * `error[E0425]: cannot find function x in this scope`: | ||
| this is usually caused by having `#[cfg(kani)]` somewhere in the control flow path of the user's proof harness. | ||
| To fix this, remove `#[cfg(kani)]` from those paths. |
There was a problem hiding this comment.
I think it's better to recommend adding --cfg=kani to your rustflags.
There was a problem hiding this comment.
I'm unclear how to do this? I tried adding this to Cargo.toml, but it didn't work:
[build]
rustflags = ["--cfg=kani"]| which differ depending on what version of the Kani library you would like to use: | ||
| * The latest version: | ||
| ```toml | ||
| [dev-dependencies] |
There was a problem hiding this comment.
Maybe change this to [target.'cfg(Kani)'.dependencies]
So this only gets pulled when user sets --cfg kani.
There was a problem hiding this comment.
This might make things tricky to use. Right now, the default user flow is to click on the "Run Test" button in their IDE, which just runs under default Rust unit test configurations. So we would have to either 1) override these IDE configs or 2) conditionally add these on the test config.
There was a problem hiding this comment.
There are ways around that, but we can tune that later. Thanks
Description of changes:
See the title. This PR only adds doc sections.
Note that there are other sections where we could potentially add info about this feature (e.g., 5 sections name the
--visualizefeature). However, as per @tedinski's suggestion, we should save those changes for later once we figure out more details about how the overall tutorial flow would be impacted.Callouts:
Some of the names used in this PR rely on the renames in #1548.
Resolved issues:
Resolves #1439, adding a doc section.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.