Enum ToolsCommand 

pub enum ToolsCommand {
    Install {
        spec: Option<String>,
        force: bool,
    },
    List {
        tool: Option<String>,
        installed: bool,
        all: bool,
    },
    Show,
    Remove {
        spec: String,
    },
    Clean,
    Pin {
        spec: Option<String>,
    },
}

Subcommands of cargo hax tools.

Variants

Install

Download and cache the tool versions the current project resolves to, or a specific <tool>@<version>.

Fields

spec: Option<String>

A <tool>@<version> specification (e.g. charon@nightly-2026.07.01) to install into the machine-wide cache. When absent, installs what the current project’s configuration resolves to.

force: bool

Re-download and verify even if the version is already cached (e.g. to verify a copy installed before its checksum shipped).

List

List the tool versions this release of hax can install with checksum verification.

Fields

tool: Option<String>

Restrict the listing to one tool.

installed: bool

Only show versions present in the local cache.

all: bool

Show every version instead of only the most recent ones.

Show

Show which tool versions are active in the current project, and where each one comes from.

Remove

Remove a tool version from the machine-wide cache.

Fields

spec: String

The <tool>@<version> specification (e.g. charon@nightly-2026.07.01) to remove from the cache.

Clean

Delete the entire tool cache. Later runs download what they need again.

Pin

Write version pins into the project’s hax.toml, creating the file when missing.

Fields

spec: Option<String>

A <name>@<version> specification to write as one entry, accepting managed tools (e.g. charon@nightly-2026.07.01) and declared versions (e.g. lean@leanprover/lean4:v4.31.0). When absent, pins the built-in defaults of this release.

Trait Implementations

impl Clone for ToolsCommand

fn clone(&self) -> ToolsCommand

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ToolsCommand

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for ToolsCommand

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl FromArgMatches for ToolsCommand

fn from_arg_matches(__clap_arg_matches: &ArgMatches) -> Result<Self, Error>

Instantiate Self from ArgMatches, parsing the arguments as needed.

fn from_arg_matches_mut( __clap_arg_matches: &mut ArgMatches, ) -> Result<Self, Error>

Instantiate Self from ArgMatches, parsing the arguments as needed.

fn update_from_arg_matches( &mut self, __clap_arg_matches: &ArgMatches, ) -> Result<(), Error>

Assign values from ArgMatches to self.

fn update_from_arg_matches_mut<'b>( &mut self, __clap_arg_matches: &mut ArgMatches, ) -> Result<(), Error>

Assign values from ArgMatches to self.

impl JsonSchema for ToolsCommand

fn schema_name() -> String

The name of the generated JSON Schema.

fn schema_id() -> Cow<'static, str>

Returns a string that uniquely identifies the schema produced by this type.

fn json_schema(generator: &mut SchemaGenerator) -> Schema

Generates a JSON Schema for this type.

fn is_referenceable() -> bool

Whether JSON Schemas generated for this type should be re-used where possible using the $ref keyword.

impl PartialEq for ToolsCommand

fn eq(&self, other: &ToolsCommand) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for ToolsCommand

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Subcommand for ToolsCommand

fn augment_subcommands<'b>(__clap_app: Command) -> Command

Append to Command so it can instantiate Self via FromArgMatches::from_arg_matches_mut

fn augment_subcommands_for_update<'b>(__clap_app: Command) -> Command

Append to Command so it can instantiate self via FromArgMatches::update_from_arg_matches_mut

fn has_subcommand(__clap_name: &str) -> bool

Test whether Self can parse a specific subcommand

impl Eq for ToolsCommand

impl StructuralPartialEq for ToolsCommand