Move dashboard under developer documentation (#715)

* Rename - Works as usual

* Changes in `build-docs.sh`

* Changes to docs

* Update workflow

* Update remaining refs to dashboard

.github/workflows/rmc.yml

@@ -57,17 +57,17 @@ jobs:
       - name: Execute RMC regression
         run: ./scripts/rmc-regression.sh
 
-      - name: Install dashboard dependencies
+      - name: Install book runner dependencies
         if: ${{ matrix.os == 'ubuntu-20.04' }}
-        run: ./scripts/setup/install_dashboard_deps.sh
+        run: ./scripts/setup/install_bookrunner_deps.sh
 
-      - name: Generate RMC dashboard
+      - name: Generate book runner report
         if: ${{ matrix.os == 'ubuntu-20.04' }}
-        run: ./x.py run -i --stage 1 dashboard
+        run: ./x.py run -i --stage 1 bookrunner
 
-      - name: Print RMC dashboard results
+      - name: Print book runner text results
         if: ${{ matrix.os == 'ubuntu-20.04' }}
-        run: cat build/output/latest/html/dashboard.txt
+        run: cat build/output/latest/html/bookrunner.txt
 
       # On one OS only, build the documentation, too.
       - name: Build Documentation

.gitignore

@@ -79,7 +79,7 @@ src/test/rustdoc-gui/src/**.lock
 /.litani_cache_dir
 /.ninja_deps
 /.ninja_log
-/src/test/dashboard
+/src/test/bookrunner
 *Cargo.lock
 src/test/rmc-dependency-test/diamond-dependency/build
 src/test/rmc-multicrate/type-mismatch/mismatch/target

Cargo.lock

@@ -186,6 +186,19 @@ dependencies = [
  "byte-tools",
 ]
 
+[[package]]
+name = "bookrunner"
+version = "0.1.0"
+dependencies = [
+ "Inflector",
+ "pulldown-cmark",
+ "rustdoc",
+ "serde",
+ "serde_json",
+ "toml",
+ "walkdir",
+]
+
 [[package]]
 name = "bootstrap"
 version = "0.0.0"
@@ -987,19 +1000,6 @@ dependencies = [
  "winapi",
 ]
 
-[[package]]
-name = "dashboard"
-version = "0.1.0"
-dependencies = [
- "Inflector",
- "pulldown-cmark",
- "rustdoc",
- "serde",
- "serde_json",
- "toml",
- "walkdir",
-]
-
 [[package]]
 name = "datafrog"
 version = "2.0.1"

Cargo.toml

@@ -7,11 +7,11 @@ members = [
   "library/rmc",
   "library/rmc_restrictions",
   "src/rustdoc-json-types",
+  "src/tools/bookrunner",
   "src/tools/cargotest",
   "src/tools/clippy",
   "src/tools/clippy/clippy_dev",
   "src/tools/compiletest",
-  "src/tools/dashboard",
   "src/tools/error_index_generator",
   "src/tools/linkchecker",
   "src/tools/lint-docs",

rmc-docs/build-docs.sh

@@ -17,24 +17,24 @@ if [ ! -x mdbook ]; then
     tar zxf $FILE
 fi
 
-# Publish dashboard into our documentation
+# Publish bookrunner report into our documentation
 RMC_DIR=$SCRIPT_DIR/..
 HTML_DIR=$RMC_DIR/build/output/latest/html/
 
 if [ -d $HTML_DIR ]; then
     # Litani run is copied into `src` to avoid deletion by `mdbook`
-    cp -r $HTML_DIR src/dashboard/
+    cp -r $HTML_DIR src/bookrunner/
     # Replace artifacts by examples under test
-    BOOKS_DIR=$RMC_DIR/src/test/dashboard/books
-    rm -r src/dashboard/artifacts
-    cp -r $BOOKS_DIR src/dashboard/artifacts
-    # Update paths in HTML dashboard
-    python $RMC_DIR/scripts/ci/update_dashboard.py src/dashboard/index.html new_index.html
-    mv new_index.html src/dashboard/index.html
-
-    rm src/dashboard/run.json
+    BOOKS_DIR=$RMC_DIR/src/test/bookrunner/books
+    rm -r src/bookrunner/artifacts
+    cp -r $BOOKS_DIR src/bookrunner/artifacts
+    # Update paths in HTML report
+    python $RMC_DIR/scripts/ci/update_bookrunner_report.py src/bookrunner/index.html new_index.html
+    mv new_index.html src/bookrunner/index.html
+
+    # rm src/bookrunner/run.json
 else
-    echo "WARNING: Could not find the latest dashboard run."
+    echo "WARNING: Could not find the latest bookrunner run."
 fi
 
 # Build the book into ./book/

rmc-docs/src/SUMMARY.md

@@ -17,5 +17,4 @@
 
 - [RMC developer documentation](./dev-documentation.md)
   - [Testing](./rmc-testing.md)
-
-- [RMC dashboard](./dashboard.md)
+  - [Book runner](./bookrunner.md)

rmc-docs/src/dashboard.md → rmc-docs/src/bookrunner.md

@@ -1,8 +1,8 @@
-# RMC Dashboard
+# Book runner
 
-The [RMC Dashboard](./dashboard/index.html) is a testing tool based on [Litani](https://github.com/awslabs/aws-build-accumulator).
+The [book runner](./bookrunner/index.html) is a testing tool based on [Litani](https://github.com/awslabs/aws-build-accumulator).
 
-The purpose of the dashboard to show the level of support in RMC for all Rust features.
+The purpose of the book runner is to get data about feature coverage in RMC.
 To this end, we use Rust code snippet examples from the following general Rust documentation books:
  * The Rust Reference
  * The Rustonomicon
@@ -12,7 +12,7 @@ To this end, we use Rust code snippet examples from the following general Rust d
 However, not all examples from these books are suited for verification.
 For instance, some of them are only included to show what is valid Rust code (or what is not).
 
-Because of that, we run up to three different types of jobs when generating the dashboard:
+Because of that, we run up to three different types of jobs when generating the report:
  * `check` jobs: This check uses the Rust front-end to detect if the example is valid Rust code.
  * `codegen` jobs: This check uses the RMC back-end to determine if we can generate GotoC code.
  * `verification` jobs: This check uses CBMC to obtain a verification result.
@@ -22,9 +22,10 @@ Similary, a `codegen` job depends on a `check` job.
 
 > **Warning:** [Litani](https://github.com/awslabs/aws-build-accumulator) does
 > not support hierarchical views at the moment. For this reason, we are
-> publishing a [text version of the dashboard](./dashboard/dashboard.txt) which
-> displays the same results in a hierarchical way while we work on adding more
-> features to [Litani](https://github.com/awslabs/aws-build-accumulator).
+> publishing a [text version of the book runner
+> report](./bookrunner/bookrunner.txt) which displays the same results in a
+> hierarchical way while we work on adding more features to
+> [Litani](https://github.com/awslabs/aws-build-accumulator).
 
 Before running the above mentioned jobs, we pre-process the examples to:
  1. Set the expected output according to flags present in the code snippet.
@@ -35,41 +36,41 @@ The results are summarized as follows: If the obtained and expected outputs diff
 the color of the stage bar will be red. Otherwise, it will be blue.
 If an example shows one red bar, it is considered a failed example that cannot be handled by RMC.
 
-The [RMC Dashboard](./dashboard/index.html) and [its text version](./dashboard/dashboard.txt) are
+The [book runner report](./bookrunner/index.html) and [its text version](./bookrunner/bookrunner.txt) are
 automatically updated whenever a PR gets merged into RMC.
 
-## The dashboard procedure
+## The book running procedure
 
-This section describes how the dashboard operates at a high level.
+This section describes how the book runner operates at a high level.
 
-To kick off the dashboard process use
+To kick off the book runner process use
 
 ```
-./x.py run -i --stage 1 dashboard
+./x.py run -i --stage 1 bookrunner
 ```
 
-The main function of the dashboard is `generate_dashboard()` in
-[`src/tools/dashboard/src/books.rs`](https://github.com/model-checking/rmc/blob/main/src/tools/dashboard/src/books.rs),
+The main function of the bookrunner is `generate_run()` in
+[`src/tools/bookrunner/src/books.rs`](https://github.com/model-checking/rmc/blob/main/src/tools/bookrunner/src/books.rs),
 which follows these steps:
  * First, it calls the different `parse_..._hierarchy()` functions which parse
    the summary files for each book.
  * The `extract_examples(...)` function uses `rustdoc` to extract all examples
    from the books.
  * Then for each example it will check if there is a corresponding `.props` file
-   in `src/tools/dashboard/configs/`. The contents of these files (e.g.,
+   in `src/tools/bookrunner/configs/`. The contents of these files (e.g.,
    command-line options) are prepended to the example.
- * All examples are written in the `src/test/dashboard/books/` folder.
+ * All examples are written in the `src/test/bookrunner/books/` folder.
 
    In general, the path to a given example is
-   `src/test/dashboard/books/<book>/<chapter>/<section>/<subsection>/<line>.rs`
+   `src/test/bookrunner/books/<book>/<chapter>/<section>/<subsection>/<line>.rs`
    where `<line>` is the line number where the example appears in the
    documentation. The `.props` files mentioned above follow the same naming
    scheme in order to match them and detect conflicts.
 
  * Then all examples are run using
    [Litani](https://github.com/awslabs/aws-build-accumulator).
  * Finally, the Litani log is used to generate the [text version of the
-   dashboard](./dashboard/dashboard.txt).
+   bookrunner](./bookrunner/bookrunner.txt).
 
 > **Warning:** Note that any changes done to the examples in
-> `src/test/dashboard/books/` may be gone if the dashboard is executed.
+> `src/test/bookrunner/books/` may be gone if the bookrunner is executed.

rmc-docs/src/dev-documentation.md

@@ -28,9 +28,9 @@ rm -r build/x86_64-unknown-linux-gnu/test/
 ./x.py test -i --stage 1 rmc firecracker prusti smack expected cargo-rmc rmc-docs
 ```
 ```bash
-# Dashboard run
-./scripts/setup/install_dashboard_deps.sh
-./x.py run -i --stage 1 dashboard
+# Book runner run
+./scripts/setup/install_bookrunner_deps.sh
+./x.py run -i --stage 1 bookrunner
 ```
 ```bash
 # Documentation build

rmc-docs/src/getting-started.md

@@ -9,7 +9,7 @@ But RMC is also useful for finding panics in safe Rust, and it can check user-de
 
 RMC is currently in the initial development phase, and has not yet made an official release.
 It is under active development, but it does not yet support all Rust language features.
-(The [RMC dashboard](./dashboard.md) can help you understand our current progress.)
+(The [Book runner](./bookrunner.md) can help you understand our current progress.)
 If you encounter issues when using RMC we encourage you to [report them to us](https://github.com/model-checking/rmc/issues/new/choose).
 
 RMC usually syncs with the main branch of Rust every week, and so is generally up-to-date with the latest Rust language features.

rmc-docs/src/rmc-testing.md

@@ -15,7 +15,7 @@ two very good reasons to do it:
 
 We recommend reading our section on [Regression Testing](#regression-testing)
 if you are interested in RMC development. At present, we obtain metrics based
-on the [RMC dashboard](./dashboard.md).
+on the [book runner](./bookrunner.md).
 
 # Regression testing
 

scripts/ci/update_dashboard.py → scripts/ci/update_bookrunner_report.py

@@ -11,14 +11,14 @@ def update_path(run, path):
 
     By default, the path to an example follows this pattern:
 
-    `src/test/dashboard/books/<book>/<chapter>/<section>/<subsection>/<line>.rs`
+    `src/test/bookrunner/books/<book>/<chapter>/<section>/<subsection>/<line>.rs`
 
     However, only the first part is shown since these paths are enclosed
     in paragraph markers (`<p>` and `</p>`). So they are often rendered as:
 
-    `src/test/dashboard/books/<book>/<chapter>/...
+    `src/test/bookrunner/books/<book>/<chapter>/...
 
-    This update removes `src/test/dashboard/books/` from the path (common to
+    This update removes `src/test/bookrunner/books/` from the path (common to
     all examples) and transforms them into anchor elements with a link to
     the example, so the path to the example is shown as:
 
@@ -34,7 +34,7 @@ def update_path(run, path):
 
 def main():
     parser = argparse.ArgumentParser(
-        description='Produces an updated HTML dashboard file from the '
+        description='Produces an updated HTML report file from the '
                     'contents of an HTML file generated with `litani`')
     parser.add_argument('input')
     parser.add_argument('output')

scripts/setup/install_dashboard_deps.sh → scripts/setup/install_bookrunner_deps.sh

@@ -4,7 +4,7 @@
 
 set -eu
 
-# The RMC Dashboard is generated using [Litani](https://github.com/awslabs/aws-build-accumulator)
+# The book runner report is generated using [Litani](https://github.com/awslabs/aws-build-accumulator)
 
 # Litani's dependencies:
 DEPS=(
@@ -15,7 +15,7 @@ DEPS=(
 sudo DEBIAN_FRONTEND=noninteractive apt-get install --no-install-recommends --yes "${DEPS[@]}"
 
 PYTHON_DEPS=(
-  bs4 # Used for dashboard updates
+  bs4 # Used for report updates
   jinja2
 )
 

src/bootstrap/builder.rs

@@ -381,7 +381,7 @@ impl<'a> Builder<'a> {
                 tool::Linkchecker,
                 tool::CargoTest,
                 tool::Compiletest,
-                tool::Dashboard,
+                tool::BookRunner,
                 tool::RemoteTestServer,
                 tool::RemoteTestClient,
                 tool::RustInstaller,
@@ -471,7 +471,7 @@ impl<'a> Builder<'a> {
                 test::SMACK,
                 test::CargoRMC,
                 test::Expected,
-                test::Dashboard,
+                test::BookRunner,
                 test::Stub,
                 test::RmcDocs,
                 test::RmcFixme,
@@ -538,7 +538,7 @@ impl<'a> Builder<'a> {
                 install::Rustc
             ),
             Kind::Run => describe!(
-                run::Dashboard,
+                run::BookRunner,
                 run::ExpandYamlAnchors,
                 run::BuildManifest,
                 run::BumpStage0

src/bootstrap/run.rs

@@ -6,35 +6,35 @@ use build_helper::output;
 use std::process::Command;
 
 #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
-pub struct Dashboard {
+pub struct BookRunner {
     pub compiler: Compiler,
 }
 
-impl Step for Dashboard {
+impl Step for BookRunner {
     type Output = ();
 
-    /// Runs the `dashboard` tool.
+    /// Runs the `bookrunner` tool.
     ///
     /// This tool in `src/tools` extracts examples from books, runs them through
     /// RMC, and displays their results.
     fn run(self, builder: &Builder<'_>) {
-        // Before running the dashboard, we need to ensure that it is already
+        // Before running `bookrunner`, we need to ensure that it is already
         // built.
-        let dashboard = builder.ensure(tool::Dashboard { compiler: self.compiler });
+        let book_runner = builder.ensure(tool::BookRunner { compiler: self.compiler });
         // We also need to ensure that stage n standard library is built for
         // rmc-rustc.
         builder.ensure(compile::Std { compiler: self.compiler, target: self.compiler.host });
         let target = builder.config.build.triple;
-        builder.info("Generating confidence dashboard");
-        try_run(builder, Command::new(dashboard).env("TRIPLE", target));
+        builder.info("Launching book runner...");
+        try_run(builder, Command::new(book_runner).env("TRIPLE", target));
     }
 
     fn should_run(run: ShouldRun<'_>) -> ShouldRun<'_> {
-        run.path("src/tools/dashboard")
+        run.path("src/tools/bookrunner")
     }
 
     fn make_run(run: RunConfig<'_>) {
-        run.builder.ensure(Dashboard {
+        run.builder.ensure(BookRunner {
             compiler: run.builder.compiler(run.builder.top_stage, run.target),
         });
     }

src/bootstrap/test.rs

@@ -1227,7 +1227,7 @@ default_test!(CargoRMC { path: "src/test/cargo-rmc", mode: "cargo-rmc", suite: "
 
 default_test!(Expected { path: "src/test/expected", mode: "expected", suite: "expected" });
 
-default_test!(Dashboard { path: "src/test/dashboard", mode: "rmc", suite: "dashboard" });
+default_test!(BookRunner { path: "src/test/bookrunner", mode: "rmc", suite: "bookrunner" });
 
 default_test!(RmcDocs { path: "src/test/rmc-docs", mode: "rmc", suite: "rmc-docs" });