model-checking · tautschnig · Apr 5, 2024 · Apr 4, 2024 · Apr 5, 2024
@@ -96,39 +96,14 @@ jobs:
         env:
           RUST_TEST_THREADS: 1
 
-  bookrunner:
+  documentation:
     runs-on: ubuntu-20.04
     permissions:
       contents: write
     steps:
       - name: Checkout Kani
         uses: actions/checkout@v4
 
-      - name: Setup Kani Dependencies
-        uses: ./.github/actions/setup
-        with:
-          os: ubuntu-20.04
-
-      - name: Build Kani
-        run: cargo build-dev
-
-      - name: Install book runner dependencies
-        run: ./scripts/setup/install_bookrunner_deps.sh
-
-      - name: Generate book runner report
-        run: cargo run -p bookrunner
-        env:
-          DOC_RUST_LANG_ORG_CHANNEL: nightly
-
-      - name: Print book runner text results
-        run: cat build/output/latest/html/bookrunner.txt
-
-      - name: Print book runner failures grouped by stage
-        run: python3 scripts/ci/bookrunner_failures_by_stage.py build/output/latest/html/index.html
-
-      - name: Detect unexpected book runner failures
-        run: ./scripts/ci/detect_bookrunner_failures.sh build/output/latest/html/bookrunner.txt
-
       - name: Install book dependencies
         run: ./scripts/setup/ubuntu/install_doc_deps.sh
 

@@ -74,10 +74,8 @@ package-lock.json
 tests/rustdoc-gui/src/**.lock
 
 # Before adding new lines, see the comment at the top.
-/.litani_cache_dir
 /.ninja_deps
 /.ninja_log
-/tests/bookrunner
 *Cargo.lock
 tests/kani-dependency-test/diamond-dependency/build
 tests/kani-multicrate/type-mismatch/mismatch/target

@@ -1,12 +1,3 @@
-[submodule "src/doc/nomicon"]
-	path = tools/bookrunner/rust-doc/nomicon
-	url = https://github.com/rust-lang/nomicon.git
-[submodule "src/doc/reference"]
-	path = tools/bookrunner/rust-doc/reference
-	url = https://github.com/rust-lang/reference.git
-[submodule "src/doc/rust-by-example"]
-	path = tools/bookrunner/rust-doc/rust-by-example
-	url = https://github.com/rust-lang/rust-by-example.git
 [submodule "firecracker"]
 	path = firecracker
 	url = https://github.com/firecracker-microvm/firecracker.git

@@ -2,16 +2,6 @@
 # It is not intended for manual editing.
 version = 3
 
-[[package]]
-name = "Inflector"
-version = "0.11.4"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "fe438c63458706e03479442743baae6c88256498e6431708f6dfc520a26515d3"
-dependencies = [
- "lazy_static",
- "regex",
-]
-
 [[package]]
 name = "ahash"
 version = "0.8.11"
@@ -105,20 +95,6 @@ version = "2.5.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "cf4b9d6a944f767f8e5e0db018570623c85f3d925ac718db4e06d0187adb21c1"
 
-[[package]]
-name = "bookrunner"
-version = "0.1.0"
-dependencies = [
- "Inflector",
- "pulldown-cmark",
- "pulldown-cmark-escape",
- "rustdoc",
- "serde",
- "serde_json",
- "toml",
- "walkdir",
-]
-
 [[package]]
 name = "build-kani"
 version = "0.48.0"
@@ -764,23 +740,6 @@ dependencies = [
  "unicode-ident",
 ]
 
-[[package]]
-name = "pulldown-cmark"
-version = "0.10.2"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5f0530d13d87d1f549b66a3e8d0c688952abe5994e204ed62615baaf25dc029c"
-dependencies = [
- "bitflags 2.5.0",
- "memchr",
- "unicase",
-]
-
-[[package]]
-name = "pulldown-cmark-escape"
-version = "0.10.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d5d8f9aa0e3cbcfaf8bf00300004ee3b72f74770f9cbac93f6928771f613276b"
-
 [[package]]
 name = "quote"
 version = "1.0.35"
@@ -899,13 +858,6 @@ version = "0.1.23"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d626bb9dae77e28219937af045c257c28bfd3f69333c512553507f5f9798cb76"
 
-[[package]]
-name = "rustdoc"
-version = "0.0.0"
-dependencies = [
- "pulldown-cmark",
-]
-
 [[package]]
 name = "rustix"
 version = "0.38.32"
@@ -1272,15 +1224,6 @@ dependencies = [
  "tracing-serde",
 ]
 
-[[package]]
-name = "unicase"
-version = "2.7.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f7d2d4dafb69621809a81864c9c1b864479e1235c0dd4e199924b9742439ed89"
-dependencies = [
- "version_check",
-]
-
 [[package]]
 name = "unicode-ident"
 version = "1.0.12"

@@ -38,14 +38,11 @@ strip = "debuginfo"
 members = [
   "library/kani",
   "library/std",
-  "tools/bookrunner",
   "tools/compiletest",
   "tools/build-kani",
   "kani-driver",
   "kani-compiler",
   "kani_metadata",
-  # `librustdoc` is still needed by bookrunner.
-  "tools/bookrunner/librustdoc",
 ]
 
 # This indicates what package to e.g. build with 'cargo build' without --workspace

@@ -31,7 +31,6 @@
   - [cargo kani assess](./dev-assess.md)
   - [Testing](./testing.md)
     - [Regression testing](./regression-testing.md)
-    - [Book runner](./bookrunner.md)
     - [(Experimental) Testing with a Large Number of Repositories](./repo-crawl.md)
   - [Performance comparisons](./performance-comparisons.md)
     - [`benchcomp` command line](./benchcomp-cli.md)

@@ -19,7 +19,7 @@ cargo build-dev
 ### Test
 
 ```bash
-# Full regression suite (does not run bookrunner)
+# Full regression suite
 ./scripts/kani-regression.sh
 ```
 
@@ -39,12 +39,6 @@ rm -r build/x86_64-apple-darwin/tests/
 cargo run -p compiletest -- --suite kani --mode kani
 ```
 
-```bash
-# Run bookrunner
-./scripts/setup/install_bookrunner_deps.sh
-cargo run -p bookrunner
-```
-
 ```bash
 # Build documentation
 cd docs

@@ -15,6 +15,5 @@ two very good reasons to do it:
 
 We recommend reading our section on [Regression
 Testing](./regression-testing.md) if you're interested in Kani
-development. At present, we obtain metrics based on the [book
-runner](./bookrunner.md). To run kani on a large number of remotely
+development. To run kani on a large number of remotely
 hosted crates, please see [Repository Crawl](./repo-crawl.md).
@@ -15,5 +15,4 @@ ignore = [
     # For some reason, this is not working without the directory wildcard.
     "**/firecracker",
     "**/tests/perf/s2n-quic/",
-    "**/tools/bookrunner/rust-doc/",
 ]
@@ -32,33 +32,12 @@ else
   MDBOOK=${SCRIPT_DIR}/mdbook
 fi
 
-# Publish bookrunner report into our documentation
 KANI_DIR=$SCRIPT_DIR/..
 DOCS_DIR=$KANI_DIR/docs
 RFC_DIR=$KANI_DIR/rfc
-HTML_DIR=$KANI_DIR/build/output/latest/html/
 
 cd $DOCS_DIR
 
-if [ -d $HTML_DIR ]; then
-    # Litani run is copied into `src` to avoid deletion by `mdbook`
-    cp -r $HTML_DIR src/bookrunner/
-    # Replace artifacts by examples under test
-    BOOKS_DIR=$KANI_DIR/tests/bookrunner/books
-    rm -r src/bookrunner/artifacts
-    # Remove any json files that Kani might've left behind due to crash or timeout.
-    find $BOOKS_DIR -name '*.json' -exec rm {} \;
-    find $BOOKS_DIR -name '*.out' -exec rm {} \;
-    cp -r $BOOKS_DIR src/bookrunner/artifacts
-    # Update paths in HTML report
-    python $KANI_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 bookrunner run."
-fi
-
 echo "Building user documentation..."
 # Generate benchcomp documentation from source code
 mkdir -p gen_src