Start stabilizing --jobs and list; deprecate default memory checks

kani-driver/src/args/autoharness_args.rs

@@ -31,7 +31,7 @@ pub struct CommonAutoharnessArgs {
     #[arg(long = "exclude-pattern", num_args(1), value_name = "PATTERN")]
     pub exclude_pattern: Vec<String>,
 
-    /// Run the `list` subcommand after generating the automatic harnesses. Requires -Z list. Note that this option implies --only-codegen.
+    /// Run the `list` subcommand after generating the automatic harnesses. Note that this option implies --only-codegen.
     #[arg(long)]
     pub list: bool,
 
@@ -85,15 +85,6 @@ impl ValidateArgs for CargoAutoharnessArgs {
             ));
         }
 
-        if self.common_autoharness_args.list
-            && !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::List)
-        {
-            return Err(Error::raw(
-                ErrorKind::MissingRequiredArgument,
-                format!("The `list` feature is unstable and requires -Z {}", UnstableFeature::List),
-            ));
-        }
-
         if self.common_autoharness_args.list
             && self.common_autoharness_args.format == Format::Pretty
             && self.verify_opts.common_args.quiet
@@ -133,15 +124,6 @@ impl ValidateArgs for StandaloneAutoharnessArgs {
             ));
         }
 
-        if self.common_autoharness_args.list
-            && !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::List)
-        {
-            return Err(Error::raw(
-                ErrorKind::MissingRequiredArgument,
-                format!("The `list` feature is unstable and requires -Z {}", UnstableFeature::List),
-            ));
-        }
-
         if self.common_autoharness_args.list
             && self.common_autoharness_args.format == Format::Pretty
             && self.verify_opts.common_args.quiet

kani-driver/src/args/common.rs

@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! Define arguments that should be common to all subcommands in Kani.
-use crate::args::ValidateArgs;
+use crate::args::{ValidateArgs, print_stabilized_feature_warning};
 use clap::{error::Error, error::ErrorKind};
 pub use kani_metadata::{EnabledUnstableFeatures, UnstableFeature};
 
@@ -40,6 +40,21 @@ impl ValidateArgs for CommonArgs {
                 "The `--dry-run` option is obsolete. Use --verbose instead.",
             ));
         }
+        if self.enable_unstable {
+            return Err(Error::raw(
+                ErrorKind::ValueValidation,
+                "The `--enable-unstable` option is obsolete. Enable the appropriate unstable feature(s) with `-Z {feature}` instead.",
+            ));
+        }
+
+        // Warn if a deprecated unstable feature is enabled.
+        for feature in self.unstable_features.iter() {
+            let stabilization_version = feature.stabilization_version();
+            if let Some(version) = stabilization_version {
+                print_stabilized_feature_warning(self, *feature, &version);
+            }
+        }
+
         Ok(())
     }
 }
@@ -52,22 +67,13 @@ impl CommonArgs {
         required: UnstableFeature,
     ) -> Result<(), Error> {
         if enabled && !self.unstable_features.contains(required) {
-            let z_feature = format!("-Z {required}");
-            if self.enable_unstable {
-                return Err(Error::raw(
-                    ErrorKind::ValueValidation,
-                    format!(
-                        "The `--enable-unstable` option is obsolete. Use `{z_feature}` instead.",
-                    ),
-                ));
-            } else {
-                return Err(Error::raw(
-                    ErrorKind::MissingRequiredArgument,
-                    format!(
-                        "The `{argument}` argument is unstable and requires `{z_feature}` to be used.",
-                    ),
-                ));
-            }
+            return Err(Error::raw(
+                ErrorKind::MissingRequiredArgument,
+                format!(
+                    "The `--{argument}` option is unstable and requires `{}` to be used.",
+                    required.as_argument_string()
+                ),
+            ));
         }
         Ok(())
     }

kani-driver/src/args/list_args.rs

@@ -6,7 +6,6 @@ use std::path::PathBuf;
 
 use crate::args::{CommonArgs, ValidateArgs, validate_std_path};
 use clap::{Error, Parser, ValueEnum, error::ErrorKind};
-use kani_metadata::UnstableFeature;
 
 /// List information relevant to verification
 #[derive(Debug, Parser)]
@@ -57,12 +56,6 @@ pub enum Format {
 impl ValidateArgs for CargoListArgs {
     fn validate(&self) -> Result<(), Error> {
         self.common_args.validate()?;
-        if !self.common_args.unstable_features.contains(UnstableFeature::List) {
-            return Err(Error::raw(
-                ErrorKind::MissingRequiredArgument,
-                "The `list` subcommand is unstable and requires -Z list",
-            ));
-        }
 
         if self.format == Format::Pretty && self.common_args.quiet {
             return Err(Error::raw(
@@ -78,12 +71,6 @@ impl ValidateArgs for CargoListArgs {
 impl ValidateArgs for StandaloneListArgs {
     fn validate(&self) -> Result<(), Error> {
         self.common_args.validate()?;
-        if !self.common_args.unstable_features.contains(UnstableFeature::List) {
-            return Err(Error::raw(
-                ErrorKind::MissingRequiredArgument,
-                "The `list` subcommand is unstable and requires -Z list",
-            ));
-        }
 
         if self.format == Format::Pretty && self.common_args.quiet {
             return Err(Error::raw(