Merge branch 'main' into iss3079

.github/workflows/bench.yml

@@ -55,12 +55,6 @@ jobs:
           os: ubuntu-20.04
           kani_dir: new
 
-      - name: Build Kani (new variant)
-        run: pushd new && cargo build-dev
-
-      - name: Build Kani (old variant)
-        run: pushd old && cargo build-dev
-
       - name: Copy benchmarks from new to old
         run: rm -rf ./old/tests/perf ; cp -r ./new/tests/perf ./old/tests/
 

.github/workflows/cbmc-latest.yml

@@ -32,10 +32,6 @@ jobs:
           os: ${{ matrix.os }}
           kani_dir: 'kani'
 
-      - name: Build Kani
-        working-directory: ./kani
-        run: cargo build-dev
-
       - name: Checkout CBMC under "cbmc"
         uses: actions/checkout@v4
         with:

.github/workflows/kani-m1.yml

@@ -23,8 +23,5 @@ jobs:
         with:
           os: macos-13-xlarge
 
-      - name: Build Kani
-        run: cargo build-dev
-
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh

.github/workflows/kani.yml

@@ -27,9 +27,6 @@ jobs:
         with:
           os: ${{ matrix.os }}
 
-      - name: Build Kani
-        run: cargo build-dev
-
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
 
@@ -88,47 +85,19 @@ jobs:
         with:
           os: ubuntu-20.04
 
-      - name: Build Kani using release mode
-        run: cargo build-dev -- --release
-
       - name: Execute Kani performance tests
         run: ./scripts/kani-perf.sh
         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
 

.gitignore

@@ -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

.gitmodules

@@ -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

Cargo.lock

@@ -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"

Cargo.toml

@@ -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

docs/src/SUMMARY.md

@@ -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)

docs/src/cheat-sheets.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

docs/src/rust-feature-support/intrinsics.md

@@ -220,6 +220,7 @@ truncf64 | Yes | |
 try | No | [#267](https://github.com/model-checking/kani/issues/267) |
 type_id | Yes | |
 type_name | Yes | |
+typed_swap | Yes | |
 unaligned_volatile_load | No | See [Notes - Concurrency](#concurrency) |
 unaligned_volatile_store | No | See [Notes - Concurrency](#concurrency) |
 unchecked_add | Yes | |

docs/src/testing.md

@@ -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).