Upgrade mdbook and set global flag to disable play feature (rust-lang#1211)

* Upgrade `mdbook` version

* Set global option to disable playground feature

* Remove `noplaypen` annotation from Rust code snippets

Author: adpaco-aws

docs/book.toml

@@ -12,3 +12,6 @@ multilingual = false
 site-url = "/kani/"
 git-repository-url = "https://github.com/model-checking/kani"
 edit-url-template = "https://github.com/model-checking/kani/edit/main/docs/{path}"
+
+[output.html.playground]
+runnable = false

docs/build-docs.sh

@@ -8,9 +8,10 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" &> /dev/null && pwd )"
 cd $SCRIPT_DIR
 
 # Download mdbook release (vs spending time building it via cargo install)
-FILE="mdbook-v0.4.12-x86_64-unknown-linux-gnu.tar.gz"
-URL="https://github.com/rust-lang/mdBook/releases/download/v0.4.12/$FILE"
-EXPECTED_HASH="2a0953c50d8156e84f193f15a506ef0adbac66f1942b794de5210ca9ca73dd33"
+MDBOOK_VERSION=v0.4.18
+FILE="mdbook-${MDBOOK_VERSION}-x86_64-unknown-linux-gnu.tar.gz"
+URL="https://github.com/rust-lang/mdBook/releases/download/${MDBOOK_VERSION}/$FILE"
+EXPECTED_HASH="d276b0e594d5980de6a7917ce74c348f28d3cb8b353ca4eaae344ae8a4c40bea"
 if [ ! -x mdbook ]; then
     curl -sSL -o "$FILE" "$URL"
     echo "$EXPECTED_HASH $FILE" | sha256sum -c -

docs/src/install-guide.md

@@ -108,7 +108,7 @@ export PATH=$(pwd)/scripts:$PATH
 
 Create a test file:
 
-```rust,noplaypen
+```rust
 // File: test.rs
 #[kani::proof]
 fn main() {

docs/src/regression-testing.md

@@ -80,7 +80,7 @@ error: test failed: expected check success, got failure
 When working on a test that's expected to fail, there are two options to
 indicate an expected failure. The first one is to add a comment
 
-```rust,noplaypen
+```rust
 // kani-<stage>-fail
 ```
 at the top of the test file, where `<stage>` is the stage where the test is
@@ -100,13 +100,13 @@ predicate.
 Many tests will require passing command-line options to Kani. These options can
 be specified in single Rust files by adding a comment at the top of the file:
 
-```rust,noplaypen
+```rust
 // kani-flags: <options>
 ```
 
 For example, to use an unwinding value of 4 in a test, we can write:
 
-```rust,noplaypen
+```rust
 // kani-flags: --default-unwind 4
 ```
 

docs/src/tutorial-first-steps.md

@@ -6,7 +6,7 @@ With Kani, all the corner cases are covered from the start, and the new concern
 
 Consider this first program (which can be found under [`first-steps-v1`](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/first-steps-v1/)):
 
-```rust,noplaypen
+```rust
 {{#include tutorial/first-steps-v1/src/main.rs:code}}
 ```
 
@@ -17,7 +17,7 @@ And if this function was more complicated—for example, if some of the branches
 
 We can try to property test a function like this, but if we're naive about it (and consider all possible `u32` inputs), then it's unlikely we'll ever find the bug.
 
-```rust,noplaypen
+```rust
 {{#include tutorial/first-steps-v1/src/main.rs:proptest}}
 ```
 
@@ -31,7 +31,7 @@ There's only 1 in 4 billion inputs that fail, so it's vanishingly unlikely the p
 
 With Kani, however, we can use `kani::any()` to represent all possible `u32` values:
 
-```rust,noplaypen
+```rust
 {{#include tutorial/first-steps-v1/src/main.rs:kani}}
 ```
 
@@ -83,7 +83,7 @@ Try a few other types of errors.
 
 For example, instead of panicking we could try explicitly dereferencing a null pointer:
 
-```rust,noplaypen
+```rust
 unsafe { return *(0 as *const u32) };
 ```
 
@@ -146,7 +146,7 @@ It seems a bit odd that we can take billions of inputs when our function only ha
 Let's encode this fact about our function by asserting some reasonable bound on our input, after we've fixed our bug (code available under
 [`first-steps-v2`](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/first-steps-v2/)):
 
-```rust,noplaypen
+```rust
 {{#include tutorial/first-steps-v2/src/main.rs:code}}
 ```
 
@@ -172,7 +172,7 @@ This is the purpose of _proof harnesses_.
 Much like property testing (which would also fail in this assertion), we need to set up our preconditions, call the function in question, then assert our postconditions.
 Here's a revised example of the proof harness, one that now succeeds:
 
-```rust,noplaypen
+```rust
 {{#include tutorial/first-steps-v2/src/main.rs:kani}}
 ```
 

docs/src/tutorial-kinds-of-failure.md

@@ -10,21 +10,21 @@ In this section, we're going to expand on these additional checks, to give you a
 Rust is safe by default, and so includes dynamic (run-time) bounds checking where needed.
 Consider this Rust code (available [here](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/kinds-of-failure/src/bounds_check.rs)):
 
-```rust,noplaypen
+```rust
 {{#include tutorial/kinds-of-failure/src/bounds_check.rs:code}}
 ```
 
 We can again write a simple property test against this code:
 
-```rust,noplaypen
+```rust
 {{#include tutorial/kinds-of-failure/src/bounds_check.rs:proptest}}
 ```
 
 This property test will immediately find the failing case because of this dynamic check.
 
 But what if we change this function to use unsafe Rust?
 
-```rust,noplaypen
+```rust
 return unsafe { *a.get_unchecked(i % a.len() + 1) };
 ```
 
@@ -38,7 +38,7 @@ test bounds_check::tests::doesnt_crash ... ok
 
 But we're able to write a harness for this unsafe code:
 
-```rust,noplaypen
+```rust
 {{#include tutorial/kinds-of-failure/src/bounds_check.rs:kani}}
 ```
 
@@ -136,7 +136,7 @@ These two techniques should help you find both the nondeterministic inputs, and
 
 Consider a different variant on the function above:
 
-```rust,noplaypen
+```rust
 fn get_wrapped(i: usize, a: &[u32]) -> u32 {
     return a[i % a.len()];
 }
@@ -150,7 +150,7 @@ Kani will spot this not as a bound error, but as a mathematical error: on an emp
 Rust also performs runtime safety checks for integer overflows, much like it does for bounds checks.
 Consider this code (available [here](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/kinds-of-failure/src/overflow.rs)):
 
-```rust,noplaypen
+```rust
 {{#include tutorial/kinds-of-failure/src/overflow.rs:code}}
 ```
 
@@ -177,7 +177,7 @@ For instance, instead of `a + b` write `a.wrapping_add(b)`.
 One of the classic subtle bugs that persisted in many implementations for a very long time is finding the midpoint in quick sort.
 This often naively looks like this (code available [here](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/kinds-of-failure/src/overflow_quicksort.rs)):
 
-```rust,noplaypen
+```rust
 {{#include tutorial/kinds-of-failure/src/overflow_quicksort.rs:code}}
 ```
 
@@ -193,7 +193,7 @@ Don't add that right away, see what happens if you don't. Just keep it in mind.)
 
 A very common approach for resolving the overflow issue looks like this:
 
-```rust,noplaypen
+```rust
 return low + (high - low) / 2;
 ```
 
@@ -206,7 +206,7 @@ After all, what does "correct" even mean?
 Often we're using a good approximation of correct, such as the equivalence of two implementations (often one much "simpler" than the other somehow).
 Here's one possible assertion to make that obvious:
 
-```rust,noplaypen
+```rust
 assert!(result as u64 == (a as u64 + b as u64) / 2);
 ```
 

docs/src/tutorial-loop-unwinding.md

@@ -2,14 +2,14 @@
 
 Consider code like this (available [here](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/loops-unwinding/src/lib.rs)):
 
-```rust,noplaypen
+```rust
 {{#include tutorial/loops-unwinding/src/lib.rs:code}}
 ```
 
 This code has an off-by-one error that only occurs on the last iteration of the loop (when called with an input that will trigger it).
 We can try to find this bug with a proof harness like this:
 
-```rust,noplaypen
+```rust
 {{#include tutorial/loops-unwinding/src/lib.rs:kani}}
 ```
 
@@ -84,7 +84,7 @@ Kani is now sure we've unwound the loop enough to verify our proof harness, and
 Kani allows three options to specify the unwind value for a particular harness:
 
 1. The unwind annotation `#[kani::unwind(<num>)]`. This sets the unwind value for the harness with the annotation. Example -
-``` rust,noplaypen
+``` rust
 #[kani::proof]
 #[kani::unwind(3)]
 fn proof_harness() {

docs/src/tutorial-nondeterministic-variables.md

@@ -16,13 +16,13 @@ In this tutorial, we will show how to:
 Let's say you're developing an inventory management tool, and you would like to verify that your API to manage items is correct.
 Here is a simple implementation of this API:
 
-```rust,noplaypen
+```rust
 {{#include tutorial/arbitrary-variables/src/inventory.rs:inventory_lib}}
 ```
 
 Now we would like to verify that, no matter which combination of `id` and `quantity`, a call to `Inventory::update()` followed by a call to `Inventory::get()` using the same `id` returns some value that's equal to the one we inserted:
 
-```rust,noplaypen
+```rust
 {{#include tutorial/arbitrary-variables/src/inventory.rs:safe_update}}
 ```
 
@@ -47,7 +47,7 @@ That said, there may be cases where you want to verify your code taking into con
 
 Let's see what happens if we modify our verification harness to use the unsafe method `kani::any_raw()` to generate the updated value.
 
-```rust,noplaypen
+```rust
 {{#include tutorial/arbitrary-variables/src/inventory.rs:unsafe_update}}
 ```
 
@@ -68,7 +68,7 @@ cargo kani --harness unsafe_update
 Now you would like to add a new structure to your library that allow users to represent a review rating, which can go from 0 to 5 stars.
 Let's say you add the following implementation:
 
-```rust,noplaypen
+```rust
 {{#include tutorial/arbitrary-variables/src/rating.rs:rating_struct}}
 ```
 
@@ -77,13 +77,13 @@ The easiest way to allow users to create nondeterministic variables of the Ratin
 The implementation only requires you to define a check to your structure that returns whether its current value is valid or not.
 In our case, we have the following implementation:
 
-```rust,noplaypen
+```rust
 {{#include tutorial/arbitrary-variables/src/rating.rs:rating_invariant}}
 ```
 
 Now you can use `kani::any()` to create valid nondeterministic variables of the Rating type as shown in this harness:
 
-```rust,noplaypen
+```rust
 {{#include tutorial/arbitrary-variables/src/rating.rs:verify_rating}}
 ```
 

docs/src/verification-results.md

@@ -27,7 +27,7 @@ because the property is unreachable, or because the harness is
 _over-constrained_.
 
 Example:
-```rust,noplaypen
+```rust
 {{#include getting-started/verification-results/src/main.rs:success_example}}
 ```
 The output from Kani indicates that the assertion holds:
@@ -43,7 +43,7 @@ hold). In this case, you can examine a trace by re-running with the
 information.
 
 Example:
-```rust,noplaypen
+```rust
 {{#include getting-started/verification-results/src/main.rs:failure_example}}
 ```
 The assertion doesn't hold as Kani's output indicates:
@@ -67,7 +67,7 @@ Kani currently checks reachability for the following assertion types:
 
 Example:
 
-```rust,noplaypen
+```rust
 {{#include getting-started/verification-results/src/main.rs:unreachable_example}}
 ```
 
@@ -85,7 +85,7 @@ that is not currently supported by Kani. See
 Rust language features.
 
 Example:
-```rust,noplaypen
+```rust
 {{#include getting-started/verification-results/src/main.rs:undetermined_example}}
 ```
 The output from Kani indicates that the assertion is undetermined due to the