Merge pull request #1415 from Aurel300/user-guide-rework

User guide rework

.github/workflows/pages.yml

@@ -36,6 +36,11 @@ jobs:
         with:
           mdbook-version: "latest"
 
+      - name: Build dummy crate to get dependencies
+        run: |
+          cd repo/docs/dummy/
+          cargo build --target-dir ./target
+
       - name: Build user guide
         run: |
           cd repo/docs/user-guide
@@ -46,6 +51,16 @@ jobs:
           cd repo/docs/dev-guide
           mdbook build -d ../../../output/dev-guide
 
+      - name: Doctest user guide
+        run: |
+          cd repo/docs/user-guide
+          mdbook test -L ../dummy/target/debug/deps
+
+      - name: Doctest dev guide
+        run: |
+          cd repo/docs/dev-guide
+          mdbook test -L ../dummy/target/debug/deps
+
       - name: Set up the environment
         run: |
           cd repo

.gitignore

@@ -31,3 +31,6 @@ log/
 nll-facts/
 benchmark-output/
 oprofile_data/
+
+docs/user-guide/book/
+docs/dev-guide/book/

Cargo.toml

@@ -22,6 +22,9 @@ members = [
     "jni-gen",
     "jni-gen/systest",
 ]
+exclude = [
+    "docs/dummy"
+]
 
 [profile.dev]
 debug = 1

docs/README.md

@@ -1,3 +1,50 @@
 # Documentation
 
 This is the source directory for Prusti's GitHub page (<https://viperproject.github.io/prusti-dev/>). Modifications should consist of pushes or pull requests to the `master` branch. Deployment on the `gh-pages` branch is done automatically via GitHub actions.
+
+The books in this documentation use [mdbook](https://rust-lang.github.io/mdBook/index.html).
+
+## Showing the book locally
+
+After [installing mdbook](https://rust-lang.github.io/mdBook/guide/installation.html) and cloning the docs onto your machine, go to the book directory you want to work on.
+
+By running `mdbook serve --open` (`mdbook.exe` on Windows), mdbooks will build the book and open it in your default browser.
+On a file change, mdbook will rebuild the book and the browser window should refresh.
+
+
+## Importing code files into the book
+
+Small code samples can be immediately put into a code block inline to the book.
+Larger code samples and code that should be checked by Prusti for correctness should be put into the prusti testing directory (`../prusti-tests/tests/`).
+
+There you can put them in the corresponding directory, like is already done in `/verify/pass/user-guide/`.
+These files will be automatically tested by the Prusti test-suite.
+
+Code blocks that are not supposed to be run by a user, please add `noplaypen` to the code block.
+
+To test all code imported into the documentation (in this case the user guide tutorial), you can run this command:
+- `./x.py test -p prusti-tests --test compiletest -- user-guide`
+This will attempt to verify all the Prusti examples in the `prusti-tests` directory that have the string "user-guide" in their path.
+
+
+## Doctests
+
+The final book can be tested using `mdbook test` (see [here](https://rust-lang.github.io/mdBook/cli/test.html)).
+This will compile and run your code samples using **standard rustc** (no Prusti).
+
+Code blocks that are not intended to be compiled should be marked with `ignore`.
+Code blocks that should not run during doctests should be marked with `no_run`.
+
+See more on documentation tests [here](https://doc.rust-lang.org/rustdoc/write-documentation/documentation-tests.html).
+
+Doctests should also run automatically as part of the Prusti CI.
+
+To run doctests locally with code that uses `prusti_contracts`, you will have to supply mdbook with a path containing the needed dependencies.
+One (not very nice way) to do this, is taking any Rust crate that uses `prusti_contracts`, building it, then passing the path to that crate to mdbook: `mdbook test -L "(Path_to_crate)/target/debug/deps/"`
+
+The crate `docs/dummy` is provided just to provide the dependencies.
+To run the doctests (in this case for the user guide):
+- `cd docs/dummy/`
+- `cargo build`
+- `cd ../user-guide/`
+- `mdbook test -L ../dummy/target/debug/deps/`

docs/dev-guide/book.toml

@@ -1,5 +1,5 @@
 [book]
-authors = ["Aurel Bílý"]
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 language = "en"
 multilingual = false
 src = "src"

docs/dev-guide/src/config/flags.md

@@ -260,7 +260,8 @@ Log level and filters. See [`env_logger` documentation](https://docs.rs/env_logg
 
 For example, `PRUSTI_LOG=prusti_viper=trace` enables trace logging for the prusti-viper crate, or `PRUSTI_LOG=debug` enables lighter logging everywhere. When using `trace` it is recommended to disable `jni` messages with e.g. `PRUSTI_LOG=trace,jni=warn`.
 A useful explanation of this can be found in the [rustc docs](https://rustc-dev-guide.rust-lang.org/tracing.html) (we set `PRUSTI_LOG` rather than `RUSTC_LOG`).
-Debug and trace logs are not available in release builds.
+When running `prusti-rustc` and `prusti-server`, it is possible to report log messages to stderr, however in release builds all trace and most debug logs are not available.
+
 
 ## `LOG_DIR`
 

docs/dev-guide/src/development/build.md

@@ -2,7 +2,7 @@
 
 Once the [development setup](setup.md) is complete, Prusti can be compiled. Using the Python wrapper script:
 
-```
+```bash
 $ ./x.py build
 ```
 

docs/dev-guide/src/encoding/pure.md

@@ -4,7 +4,12 @@ To encode specifications and side-effect-free functions (marked with `#[pure]`),
 
 For example, the Rust function:
 
-```rust
+```rust,noplaypen
+# // The next line is only used to enable mdBook doctests for this file to work
+# extern crate prusti_contracts;
+# 
+# use prusti_contracts::*;
+# 
 #[pure]
 fn hello(a: i32) -> i32 {
   let mut b = 10;

docs/dev-guide/src/encoding/types-heap.md

@@ -70,7 +70,10 @@ predicate Tuple_X_Y(self: Ref) {
 
 Structures are encoded similarly to tuples, except that fields names correspond to the names defined in the Rust type.
 
-```rust
+```rust,noplaypen
+# type X = ();
+# type Y = ();
+# 
 // for a Rust type, assuming types X and Y are defined
 struct SomeStruct {
   a: X,
@@ -91,7 +94,9 @@ predicate SomeStruct(self:Ref) {
 
 Enumerations (ADTs) have values corresponding to one of their variants. Each variant can hold different types of data, so the Viper encoding contains implications of the form "if the variant of the value is X, the value contains the following fields". The variant index is encoded as the `discriminant` field.
 
-```rust
+```rust,noplaypen
+# type X = ();
+# 
 // for a Rust type, assuming type X is defined
 enum SomeEnum {
   Foo,

docs/dev-guide/src/encoding/types-snap.md

@@ -22,7 +22,7 @@ The snapshot-based encoding of a Rust type, say `T`, consists of four components
 
 Consider the Rust struct declared below.
 
-```rust
+```rust,noplaypen
 struct SomeStruct {
   a: i32,
   b: i32,
@@ -104,8 +104,12 @@ Nested Rust structures are encoded as in the previous example - the main differe
 
 For instance, assume we extend the previous example with another structure that re-uses `SomeStruct`:
 
-```rust
-// assuming SomeStruct as before
+```rust,noplaypen
+# struct SomeStruct {
+#   a: i32,
+#   b: i32,
+# }
+# 
 struct BiggerStruct {
   foo: i32,
   bar: SomeStruct,
@@ -142,8 +146,12 @@ While the snapshot-based encoding of enumerations is mostly analogous to the enc
 
 For example, consider the enumeration below, which defines a custom Option type.
 
-```rust
-// assuming SomeStruct as before
+```rust,noplaypen
+# struct SomeStruct {
+#   a: i32,
+#   b: i32,
+# }
+# 
 enum MyOption {
   _Some(SomeStruct),
   _None,
@@ -226,15 +234,20 @@ If a type does not meet these criteria, it either invokes a user-supplied custom
 
 Whenever one invokes a [pure function](pure.md) with equal arguments, the function should yield the same return value, i.e., a function `f` with one argument should satisfy the following specification:
 
-```
+```rust,noplaypen,ignore
 x == y  ==> f(x) == f(y)
 ```
 
 For non-recursive types, the snapshot function `snap$type(ref)` recursively unfolds the predicate encoding the type of `ref`. Hence, the above property holds whenever equality of the type of `x` and `y` corresponds to structural equality, i.e., whenever the `Eq` trait is automatically derived. 
 
 For example, the following piece of Rust code verifies while internally using snapshots to discharge equality checks:
 
-```rust
+```rust,noplaypen
+# // The next line is only used to enable mdBook doctests for this file to work
+# extern crate prusti_contracts;
+# 
+# use prusti_contracts::*;
+# 
 // as before, but derives Eq
 #[derive(PartialEq, Eq)]
 struct SomeStruct {
@@ -245,7 +258,7 @@ struct SomeStruct {
 #[pure]
 #[requires(x == y)]
 #[ensures(result == y.a)]
-fn foo(x: SomeStruct, y: SomeStruct) -> i32 {
+fn foo(x: SomeStruct) -> i32 {
   x.a
 }
 
@@ -283,7 +296,7 @@ At the moment, only types implementing the [`Copy`](https://doc.rust-lang.org/co
 As an example, assume both the struct `BiggerStruct` and the struct `SomeStruct` from previous examples derive the traits `Copy` and `Eq`.
 Moreover, consider the following pure function `get` mapping every instance of `BiggerStruct` to its wrapped instance of `SomeStruct`:
 
-```rust
+```rust,noplaypen,ignore
 #[pure]
 fn get(x: BiggerStruct) -> SomeStruct {
   x.bar

docs/dummy/.cargo/config.toml

@@ -0,0 +1,2 @@
+[registries.crates-io]
+protocol = "sparse"

docs/dummy/Cargo.toml

@@ -0,0 +1,12 @@
+[package]
+name = "dummy"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+# This crate is just used to provide the needed dependencies
+# for the mdbook documentation tests
+
+[dependencies]
+prusti-contracts = { path = "../../prusti-contracts/prusti-contracts/" }

docs/dummy/README.md

@@ -0,0 +1 @@
+This crate is only used to provide the needed dependencies for the mdbook documentation tests.

docs/dummy/src/lib.rs

@@ -0,0 +1,8 @@
+use prusti_contracts::*;
+
+// This crate is just used to provide the needed dependencies
+// for the mdbook documentation tests
+
+#[requires(true)]
+#[ensures(true)]
+fn _dummy() {}

docs/user-guide/book.toml

@@ -1,5 +1,5 @@
 [book]
-authors = ["Aurel Bílý"]
+authors = ["Prusti Devs <prusti_developers@sympa.ethz.ch>"]
 language = "en"
 multilingual = false
 src = "src"

docs/user-guide/src/SUMMARY.md

@@ -4,17 +4,19 @@
 - [Installation](install.md)
 - [Basic Usage](basic.md)
 - [Guided Tour](tour/summary.md)
+  - [Setup](tour/setup.md)
   - [Getting Started](tour/getting-started.md)
   - [New](tour/new.md)
   - [Push](tour/push.md)
   - [Pop](tour/pop.md)
   - [Testing](tour/testing.md)
-  - [A Bad Stack](tour/bad-stack.md)
-  - [Options](tour/options.md)
+  - [Option](tour/option.md)
   - [Generics](tour/generics.md)
   - [Peek](tour/peek.md)
+  - [Pledges (mutable peek)](tour/pledges.md)
   - [Final Code](tour/final.md)
-  - [Pledges](tour/pledges.md)
+  - [Loop Invariants](tour/loop_invariants.md)
+  - [Counterexamples](tour/counterexamples.md)
 - [Verification Features](verify/summary.md)
   - [Absence of panics](verify/panic.md)
   - [Overflow checks](verify/overflow.md)
@@ -30,5 +32,6 @@
   - [Closures](verify/closure.md)
   - [Specification entailments](verify/spec_ent.md)
   - [Type models](verify/type-models.md)
-  - [Customizable counterexample](verify/print_counterexample.md)
+  - [Counterexamples](verify/counterexample.md)
+  - [Specifications in trait `impl` blocks](verify/impl_block_specs.md)
 - [Specification Syntax](syntax.md)

docs/user-guide/src/basic.md

@@ -9,21 +9,33 @@ When the Prusti Assistant extension is active, Rust files can be verified in one
 - By saving a Rust document, if "Verify on save" is enabled.
 - By opening a Rust document, if "Verify on open" is enabled.
 
-See the [following chapter](verify/summary.md) for a list of verification features available in Prusti.
+See the [Verification Features chapter](verify/summary.md) for a list of verification features available in Prusti.
 
 ## Command line
 
 To run Prusti on a file using the command-line setup:
 
-```bash
-$ prusti-rustc --edition=2018 path/to/file.rs
+```sh
+prusti-rustc --edition=2018 path/to/file.rs
+```
+
+Run this command from a crate or workspace root directory to verify it:
+
+```sh
+cargo-prusti
+```
+
+If Prusti is in `$PATH`, it can also be run as a [Cargo subcommand](https://doc.rust-lang.org/stable/book/ch14-05-extending-cargo.html):
+
+```sh
+cargo prusti
 ```
 
 ## Introductory example
 
 Let us verify that the function `max` below, which takes two integers and returns the greater one, is implemented correctly.
 
-```rust
+```rust,noplaypen
 fn max(a: i32, b: i32) -> i32 {
     if a > b {
         a
@@ -42,7 +54,9 @@ This tells us that
 To also verify that `max` indeed always returns the maximum of its two inputs, we have to add a corresponding specification, which states
 that the return value of `max` is at least as large as both `a` and `b` and, additionally, coincides with `a` or `b`:
 
-```rust
+```rust,noplaypen
+# // The next line is only required for doctests, you can ignore/remove it
+# extern crate prusti_contracts;
 use prusti_contracts::*;
 
 #[ensures(result >= a && result >= b)]
@@ -68,7 +82,9 @@ Notice that Prusti assumes by default that integer types are bounded; it thus pe
 
 Next, we add a second function `max3` which returns the maximum of three instead of two integers; we reuse the already verified function `max` in the new function's specification to show that this function is implemented correctly.
 
-```rust
+```rust,noplaypen
+# // The next line is only required for doctests, you can ignore/remove it
+# extern crate prusti_contracts;
 use prusti_contracts::*;
 
 #[pure]
@@ -103,7 +119,11 @@ If we omit this annotation, Prusti will complain that the postcondition of funct
 So far, we only considered programs that meet their specification and that, consequently, Prusti successfully verified.
 To conclude this example, assume we accidentally return `c` instead of `b` if `b > c` holds:
 
-```rust
+```rust,noplaypen
+# // The next line is only required for doctests, you can ignore/remove it
+# extern crate prusti_contracts;
+# use prusti_contracts::*;
+#
 #[ensures(result == max(a, max(b, c)))]
 fn max3(a: i32, b: i32, c: i32) -> i32 {
     if a > b && a > c {
@@ -122,7 +142,9 @@ In this case, Prusti will highlight the line with the error and report that the
 
 For debugging purposes, it is often useful to add `assert!(...)` macros to our code to locate the issue. For example, in the code below, we added an assertion that fails because `b > c` and thus the maximum of `b` and `c` is `b` instead of `c`. 
 
-```rust
+```rust,noplaypen
+# // The next line is only required for doctests, you can ignore/remove it
+# extern crate prusti_contracts;
 use prusti_contracts::*;
 
 #[pure]