Documentation: Structural changes #969

adpaco-aws · 2022-03-21T18:19:42Z

Description of changes:

Basically re-organizes the main chapters of the Kani documentation by grouping them into a few parts, which I think achieves a cleaner look and makes it easier to find information a particular topics. Reviews a few section names and moves files accordingly.

The left bar now looks like this:

Resolved issues:

Part of #700
Creates #966, #967 and #968

Call-outs:

There may be more changes coming to the overall structure but this contribution brings us a step closer to it.

Testing:

How is this change tested? Running mdbook locally.
Is this a refactor change? No.

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

tedinski · 2022-03-21T18:29:25Z

docs/src/SUMMARY.md


- [Limitations](./limitations.md)
+- [Comparison with other tools](./tool-comparison.md)


IMO this belongs with "getting started," the purpose is mostly to answer what Kani is and why people should be interested.

I think of "getting started" as a section that you can read in a few minutes to get a quick understanding of the project. The comparison with other tools goes a bit deeper somehow and is linked in many sections around (including the introduction). In my opinion, this is an article that will be read by people who want to know more, but right after "Introduction" may cause potential users lose interest.

tedinski · 2022-03-21T18:29:44Z

docs/src/SUMMARY.md

-  - [Debugging failures]()
-  - [Debugging non-termination]()
-  - [Debugging coverage]()
+  - [Usage](./usage.md)


I don't see the need for this page, or putting the below in a sublist.

I think splitting into subsections here (and in the next case) provides a much cleaner and organized look to our documentation. In my opinion, the previous version was a little "too flat", so adding subsections where we can may help with readability and navigation.

tedinski · 2022-03-21T18:30:27Z

docs/src/SUMMARY.md

+# Developer documentation
+  - [Command cheat sheets](./cheat-sheets.md)
+  - [Working with `rustc`](./rustc-hacks.md)
+  - [Testing](./testing.md)


I similarly don't think this page and nesting is adding anything here

celinval · 2022-03-23T19:40:11Z

docs/src/usage.md

+ * [On a single file](./kani-single-file.md) with the `kani` command.
+ * [On a package](./cargo-kani.md) with the `cargo-kani` command.
+
+Running [Kani on a single file](./kani-single-file.md) is quite useful for small examples.


or projects that don't use cargo... like Rust for Linux. :)

celinval · 2022-03-23T19:40:11Z

docs/src/usage.md

+ * [On a single file](./kani-single-file.md) with the `kani` command.
+ * [On a package](./cargo-kani.md) with the `cargo-kani` command.
+
+Running [Kani on a single file](./kani-single-file.md) is quite useful for small examples.


or projects that don't use cargo... like Rust for Linux. :)

celinval · 2022-03-23T19:43:36Z

docs/src/usage.md

+However, if you plan to integrate Kani in your projects, the recommended
+approach is to use [Kani on a package](./cargo-kani.md) because it includes
+utilities for tagging, extracting and running all proof harnesses in your
+package without making changes to its codebase.


It's not clear to me which changes users would have to make to their codebase. I would say that the main difference today between kani and cargo kani is the ability to handle external dependencies.

celinval · 2022-03-23T19:43:36Z

docs/src/usage.md

+However, if you plan to integrate Kani in your projects, the recommended
+approach is to use [Kani on a package](./cargo-kani.md) because it includes
+utilities for tagging, extracting and running all proof harnesses in your
+package without making changes to its codebase.


It's not clear to me which changes users would have to make to their codebase. I would say that the main difference today between kani and cargo kani is the ability to handle external dependencies.

I mean, the ability to build more than a single .rs file at all. I don't think kani is even useful for customers, really.

You are able to verify a full crate with standalone kani, independent on the number of files, as long as it doesn't have any external dependency.

For example, you can verify the rectangle example inside tests/cargo-kani/rectangle-example with the following command:

kani src/lib.rs --function stretched_rectangle_can_hold_original

Note that the crate has two files: src/lib.rs and src/rectangle.rs.

Oh neat. TIL

Oh neat. TIL

+1

Let's just write that then, no?

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.

adpaco-aws · 2022-03-23T22:57:42Z

Updated with feedback from PR and discussion.

zhassan-aws

LGTM

zhassan-aws · 2022-03-24T00:27:59Z

docs/src/SUMMARY.md


- [Limitations](./limitations.md)
+- [Limitations](./rust-feature-support.md)


Should this be called "Rust feature support"?

Renamed it, although it is likely that I write a main "Limitations" section when I review this part later.

* Documentation: Structural changes * Rename "Verification results" examples * Revert some changes * Add suggestions on usage * Rename: "Limitations"->"Rust feature support" * Undo example path renaming to introduction

adpaco-aws requested a review from a team as a code owner March 21, 2022 18:19

tedinski reviewed Mar 21, 2022

View reviewed changes

adpaco-aws mentioned this pull request Mar 21, 2022

Add section on Kani guarantees and TCB #949

Closed

4 tasks

celinval reviewed Mar 23, 2022

View reviewed changes

adpaco-aws force-pushed the docs-struct branch from cf7f25e to f22629e Compare March 23, 2022 22:56

zhassan-aws approved these changes Mar 24, 2022

View reviewed changes

adpaco-aws added 6 commits March 24, 2022 18:00

Documentation: Structural changes

946d925

Rename "Verification results" examples

91c3f92

Revert some changes

7e2910d

Add suggestions on usage

c4a82bf

Rename: "Limitations"->"Rust feature support"

e5e5148

Undo example path renaming to introduction

52db3ae

adpaco-aws force-pushed the docs-struct branch from 464a129 to 52db3ae Compare March 24, 2022 18:00

adpaco-aws merged commit 37bd70f into model-checking:main Mar 24, 2022

adpaco-aws mentioned this pull request Mar 29, 2022

Documentation: Updates for "Failures that Kani can spot" #985

Merged

4 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Documentation: Structural changes #969

Documentation: Structural changes #969

adpaco-aws commented Mar 21, 2022 •

edited

Loading

tedinski Mar 21, 2022

adpaco-aws Mar 21, 2022

tedinski Mar 21, 2022

adpaco-aws Mar 21, 2022

tedinski Mar 21, 2022

celinval Mar 23, 2022

celinval Mar 23, 2022

celinval Mar 23, 2022

celinval Mar 23, 2022

tedinski Mar 23, 2022

celinval Mar 23, 2022

tedinski Mar 23, 2022

adpaco-aws Mar 23, 2022 •

edited

Loading

adpaco-aws commented Mar 23, 2022

zhassan-aws left a comment

zhassan-aws Mar 24, 2022

adpaco-aws Mar 24, 2022


		- [Limitations](./limitations.md)
		- [Comparison with other tools](./tool-comparison.md)


		- [Limitations](./limitations.md)
		- [Limitations](./rust-feature-support.md)

Documentation: Structural changes #969

Documentation: Structural changes #969

Conversation

adpaco-aws commented Mar 21, 2022 • edited Loading

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

adpaco-aws Mar 23, 2022 • edited Loading

Choose a reason for hiding this comment

adpaco-aws commented Mar 23, 2022

zhassan-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

adpaco-aws commented Mar 21, 2022 •

edited

Loading

adpaco-aws Mar 23, 2022 •

edited

Loading