Remove assess subcommand

Cargo.toml

@@ -67,7 +67,6 @@ exclude = [
   "tests/cargo-ui",
   "tests/slow",
   "tests/std-checks",
-  "tests/assess-scan-test-scaffold",
   "tests/script-based-pre",
   "tests/script-based-pre/build-cache-bin/target/new_dep",
   "tests/script-based-pre/build-cache-dirty/target/new_dep",

docs/src/SUMMARY.md

@@ -36,10 +36,8 @@
   - [Working with `rustc`](./rustc-hacks.md)
   - [Migrating to StableMIR](./stable-mir.md)
   - [Command cheat sheets](./cheat-sheets.md)
-  - [cargo kani assess](./dev-assess.md)
   - [Testing](./testing.md)
     - [Regression testing](./regression-testing.md)
-    - [(Experimental) Testing with a Large Number of Repositories](./repo-crawl.md)
   - [Performance comparisons](./performance-comparisons.md)
     - [`benchcomp` command line](./benchcomp-cli.md)
     - [`benchcomp` configuration file](./benchcomp-conf.md)

docs/src/testing.md

@@ -15,5 +15,4 @@ 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. To run kani on a large number of remotely
-hosted crates, please see [Repository Crawl](./repo-crawl.md).
+development.

kani-compiler/src/args.rs

@@ -28,8 +28,6 @@ pub enum ReachabilityType {
     None,
     /// Start the cross-crate reachability analysis from all public functions in the local crate.
     PubFns,
-    /// Start the cross-crate reachability analysis from all *test* (i.e. `#[test]`) harnesses in the local crate.
-    Tests,
     /// Start the cross-crate reachability analysis from all functions in the local crate.
     /// Currently, this mode is only used for automatic harness generation.
     AllFns,

kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs

@@ -253,7 +253,7 @@ impl CodegenBackend for LlbcCodegenBackend {
                     units.store_modifies(&modifies_instances);
                     units.write_metadata(&queries, tcx);
                 }
-                ReachabilityType::Tests | ReachabilityType::AllFns => todo!(),
+                ReachabilityType::AllFns => todo!(),
                 ReachabilityType::None => {}
                 ReachabilityType::PubFns => {
                     let unit = CodegenUnit::default();