Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593use std::collections::HashSet;
use clap::Args;use clap::Parser;use clap::Subcommand;use clap::ValueEnum;
#[derive(Clone, Debug)]pub struct VargoCli { pub options: VargoOptions, pub command: VargoSubcommand,}
#[derive(Clone, Debug)]pub struct VargoOptions { pub cargo_options: CargoOptions, pub vargo_verbose: bool, pub solver_version_check: bool,}
#[derive(Clone, Debug, Args)]pub struct CargoOptions { /// Run without accessing the network #[arg(long)] pub offline: bool,
/// Use verbose output #[arg(short, long, action = clap::ArgAction::Count)] pub verbose: u8,
/// Coloring #[arg(long, value_enum, default_value_t = CargoColor::Auto)] pub color: CargoColor,}
#[derive(Clone, Debug, Args, PartialEq, Eq)]pub struct BuildOptions { /// Build artifacts in release mode, with optimizations #[arg(short, long)] pub release: bool,
/// Do not verify vstd when building #[arg(long)] pub vstd_no_verify: bool,
/// Build vstd in `no-std` mode #[arg(long)] pub vstd_no_std: bool,
/// Build vstd in `no-alloc` mode #[arg(long, requires = "vstd_no_std")] pub vstd_no_alloc: bool,
/// Turn tracing on when building vstd #[arg(long)] pub vstd_trace: bool,
/// Turn verbose logging on when building vstd #[arg(long)] pub vstd_log_all: bool,
/// Do not run lifetime checking when building vstd #[arg(long)] pub vstd_no_lifetime: bool,
/// Turn expand errors on when building vstd #[arg(long)] pub vstd_expand_errors: bool,}
#[derive(Clone, Debug, Args, PartialEq, Eq)]pub struct FeaturesOptions { /// Do not activate the default features #[arg(long)] pub no_default_features: bool,
/// Features to activate #[arg(short = 'F', long, action = clap::ArgAction::Append)] pub features: Vec<VerusFeatures>,}
#[derive(Clone, Debug, PartialEq, Eq)]pub struct VargoBuild { pub package: Option<String>, pub exclude: HashSet<String>, pub feature_options: FeaturesOptions, pub build_options: BuildOptions, pub verus_args: Vec<String>,}
#[derive(Clone, Debug, PartialEq, Eq)]pub struct VargoCheck { pub package: Option<String>, pub exclude: HashSet<String>, pub feature_options: FeaturesOptions, pub release: bool,}
#[derive(Clone, Debug, PartialEq, Eq)]pub struct VargoClean { pub package: Option<String>, pub release: bool,}
#[derive(Clone, Debug, PartialEq, Eq)]pub struct VargoClippy { pub package: Option<String>, pub exclude: HashSet<String>, pub feature_options: FeaturesOptions, pub release: bool, pub clippy_args: Vec<String>,}
#[derive(Clone, Debug, PartialEq, Eq)]pub struct VargoCmd { pub command: Vec<String>,}
#[derive(Clone, Debug, PartialEq, Eq)]pub struct VargoFmt { pub package: Option<String>, pub exclude: HashSet<String>, pub rustfmt_args: Vec<String>, pub vstd_no_verusfmt: bool,}
#[derive(Clone, Debug, PartialEq, Eq)]pub struct VargoMetadata { pub feature_options: FeaturesOptions, pub format_version: String,}
#[derive(Clone, Debug, PartialEq, Eq)]pub struct VargoNextestRun { pub package: String, pub exclude: HashSet<String>, pub feature_options: FeaturesOptions, pub build_options: BuildOptions, pub nextest_args: Vec<String>,}
#[derive(Clone, Debug, PartialEq, Eq)]pub struct VargoRun { pub package: Option<String>, pub feature_options: FeaturesOptions, pub build_options: BuildOptions, pub verus_args: Vec<String>,}
#[derive(Clone, Debug, PartialEq, Eq)]pub struct VargoTest { pub package: String, pub exclude: HashSet<String>, pub feature_options: FeaturesOptions, pub build_options: BuildOptions, pub test_args: Vec<String>,}
#[derive(Clone, Debug, PartialEq, Eq)]pub struct VargoUpdate { pub packages: Vec<String>,}
#[derive(Clone, Debug, PartialEq, Eq)]pub enum VargoSubcommand { /// Build Verus Build(VargoBuild),
/// Analyze the current package and report errors, but don't build/verify Check(VargoCheck),
/// Clean current build Clean(VargoClean),
/// Run clippy Clippy(VargoClippy),
/// Run an arbitrary command in vargo's environment Cmd(VargoCmd),
/// Run the formatter on the codebase Fmt(VargoFmt),
/// Get resolved dependencies with concrete used versions in a machine-readable format Metadata(VargoMetadata),
/// Run Verus tests using nextest NextestRun(VargoNextestRun),
/// Run a binary package Run(VargoRun),
/// Run Verus tests Test(VargoTest),
/// Update packages Update(VargoUpdate),}
impl VargoSubcommand { // if the subcommand supports a --release flag, return that // otherwise, return false pub fn release(&self) -> bool { match self { VargoSubcommand::Build(c) => c.build_options.release, VargoSubcommand::Check(c) => c.release, VargoSubcommand::Clean(c) => c.release, VargoSubcommand::Clippy(c) => c.release, VargoSubcommand::Cmd(_) => false, VargoSubcommand::Fmt(_) => false, VargoSubcommand::Metadata(_) => false, VargoSubcommand::NextestRun(c) => c.build_options.release, VargoSubcommand::Run(c) => c.build_options.release, VargoSubcommand::Test(c) => c.build_options.release, VargoSubcommand::Update(_) => false, } }
// whether a command needs to check the solver version // (if the command doesn't need to run the solver, the version check can be skipped) pub fn needs_solver_version_check(&self) -> bool { match self { VargoSubcommand::Build(_) => true, VargoSubcommand::Check(_) => false, VargoSubcommand::Clean(_) => false, VargoSubcommand::Clippy(_) => false, VargoSubcommand::Cmd(_) => true, VargoSubcommand::Fmt(_) => false, VargoSubcommand::Metadata(_) => false, VargoSubcommand::NextestRun(_) => true, VargoSubcommand::Run(_) => true, VargoSubcommand::Test(_) => true, VargoSubcommand::Update(_) => false, } }}
#[derive(Clone, Debug, Parser)]#[command(name = "vargo", arg_required_else_help = true, about)]pub struct VargoParsedCli { #[command(flatten)] pub cargo_options: CargoOptions,
/// Turn on `vargo`s verbose logging #[arg(long)] pub vargo_verbose: bool,
/// Skip checking that the server's solver version is correct #[arg(long)] pub no_solver_version_check: bool,
#[command(subcommand)] pub command: VargoParsedSubcommand,}
#[derive(Clone, Debug, ValueEnum, PartialEq, Eq, Hash, Copy)]pub enum VerusFeatures { RecordHistory, Singular,}
impl std::fmt::Display for VerusFeatures { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { VerusFeatures::RecordHistory => f.write_str("record-history"), VerusFeatures::Singular => f.write_str("singular"), } }}
#[derive(Clone, Debug, ValueEnum)]pub enum CargoColor { Always, Auto, Never,}
impl std::fmt::Display for CargoColor { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { CargoColor::Always => f.write_str("always"), CargoColor::Auto => f.write_str("auto"), CargoColor::Never => f.write_str("never"), } }}
#[derive(Clone, Debug, Subcommand)]pub enum VargoParsedSubcommand { /// Build Verus Build { /// Package to build #[arg(short, long)] package: Option<String>,
/// Exclude packages from building #[arg(long, action = clap::ArgAction::Append)] exclude: Vec<String>,
#[command(flatten)] feature_options: FeaturesOptions,
#[command(flatten)] build_options: BuildOptions,
/// Arguments to pass on to verus (in case verification is needed) #[arg(last = true, allow_hyphen_values = true)] verus_args: Vec<String>, },
/// Analyze the current package and report errors, but don't build/verify Check { /// Package to build #[arg(short, long)] package: Option<String>,
/// Exclude packages from building #[arg(long, action = clap::ArgAction::Append)] exclude: Vec<String>,
#[command(flatten)] feature_options: FeaturesOptions,
/// Check artifacts in release mode #[arg(short, long)] release: bool, },
/// Clean current build Clean { /// Package to clean #[arg(short, long)] package: Option<String>,
/// Whether to clean debug or release artifacts #[arg(short, long)] release: bool, },
/// Run cargo-clippy Clippy { /// Package to build #[arg(short, long)] package: Option<String>,
/// Exclude packages from building #[arg(long, action = clap::ArgAction::Append)] exclude: Vec<String>,
#[command(flatten)] feature_options: FeaturesOptions,
/// Check artifacts in release mode #[arg(short, long)] release: bool,
/// Options passed to clippy #[arg(last = true, allow_hyphen_values = true)] clippy_args: Vec<String>, },
/// Run an arbitrary command in vargo's environment Cmd { /// Command to run command: Vec<String>, },
/// Run the formatter on the codebase Fmt { /// Package to format #[arg(short, long)] package: Option<String>,
/// Exclude packages from formatting #[arg(long, action = clap::ArgAction::Append)] exclude: Vec<String>,
/// Whether to skip formatting vstd #[arg(long)] vstd_no_verusfmt: bool,
/// Options passed to rustfmt #[arg(last = true, allow_hyphen_values = true)] rustfmt_args: Vec<String>, },
/// Get metadata from cargo Metadata { #[command(flatten)] feature_options: FeaturesOptions,
/// Format version #[arg(long, default_value = "1")] format_version: String, },
/// Run Verus tests with nextest Nextest { /// Build and run Verus tests #[command(subcommand)] command: NexTestCommand, },
/// Run a binary package Run { /// Package to run #[arg(short, long)] package: Option<String>,
#[command(flatten)] feature_options: FeaturesOptions,
#[command(flatten)] build_options: BuildOptions,
/// Arguments to pass on to verus (in case verification is needed) #[arg(last = true, allow_hyphen_values = true)] verus_args: Vec<String>, },
/// Run Verus tests Test { /// Package to test #[arg(short, long)] package: String,
/// Exclude packages from testing #[arg(long, action = clap::ArgAction::Append)] exclude: Vec<String>,
#[command(flatten)] feature_options: FeaturesOptions,
#[command(flatten)] build_options: BuildOptions,
/// Other options (`cargo test --help` for more info) #[arg(allow_hyphen_values = true)] test_args: Vec<String>, },
/// Update dependencies Update { /// Package to update packages: Vec<String>, },}
#[derive(Clone, Debug, Subcommand)]pub enum NexTestCommand { Run { /// Package to test #[arg(short, long)] package: String,
/// Exclude packages from testing #[arg(long, action = clap::ArgAction::Append)] exclude: Vec<String>,
#[command(flatten)] feature_options: FeaturesOptions,
#[command(flatten)] build_options: BuildOptions,
/// Other options (`cargo nextest run --help` for more info) #[arg(allow_hyphen_values = true)] nextest_args: Vec<String>, },}
impl From<VargoParsedSubcommand> for VargoSubcommand { fn from(value: VargoParsedSubcommand) -> Self { match value { VargoParsedSubcommand::Build { package, exclude, feature_options, build_options, verus_args, } => VargoSubcommand::Build(VargoBuild { package, exclude: exclude.into_iter().collect(), feature_options, build_options, verus_args, }), VargoParsedSubcommand::Check { package, exclude, feature_options, release, } => VargoSubcommand::Check(VargoCheck { package, exclude: exclude.into_iter().collect(), feature_options, release, }), VargoParsedSubcommand::Clean { package, release } => { VargoSubcommand::Clean(VargoClean { package, release }) } VargoParsedSubcommand::Clippy { package, exclude, feature_options, release, clippy_args, } => VargoSubcommand::Clippy(VargoClippy { package, exclude: exclude.into_iter().collect(), feature_options, release, clippy_args, }), VargoParsedSubcommand::Cmd { command } => VargoSubcommand::Cmd(VargoCmd { command }), VargoParsedSubcommand::Fmt { package, exclude, rustfmt_args, vstd_no_verusfmt, } => VargoSubcommand::Fmt(VargoFmt { package, exclude: exclude.into_iter().collect(), vstd_no_verusfmt, rustfmt_args, }), VargoParsedSubcommand::Metadata { feature_options, format_version, } => VargoSubcommand::Metadata(VargoMetadata { feature_options, format_version, }), VargoParsedSubcommand::Nextest { command: NexTestCommand::Run { package, exclude, feature_options, build_options, nextest_args, }, } => VargoSubcommand::NextestRun(VargoNextestRun { package, exclude: exclude.into_iter().collect(), feature_options, build_options, nextest_args, }), VargoParsedSubcommand::Run { package, feature_options, build_options, verus_args, } => VargoSubcommand::Run(VargoRun { package, feature_options, build_options, verus_args, }), VargoParsedSubcommand::Test { package, exclude, feature_options, build_options, test_args, } => VargoSubcommand::Test(VargoTest { package, exclude: exclude.into_iter().collect(), feature_options, build_options, test_args, }), VargoParsedSubcommand::Update { packages } => { VargoSubcommand::Update(VargoUpdate { packages }) } } }}
impl From<VargoParsedCli> for VargoCli { fn from(value: VargoParsedCli) -> Self { VargoCli { options: VargoOptions { cargo_options: value.cargo_options, vargo_verbose: value.vargo_verbose, solver_version_check: !value.no_solver_version_check, }, command: value.command.into(), } }}