Crate cargo_hax

Modules

engine_debug_webapp 🔒

Constants

ENGINE_BINARY_NAME 🔒

ENGINE_BINARY_NOT_FOUND 🔒

RUSTFLAGS 🔒

We set cfg(hax) so that client crates can include dependencies or cfg-gate pieces of code.

RUST_ENGINE_BINARY_NAME 🔒

RUST_ENGINE_BINARY_NOT_FOUND 🔒

RUST_LOG_STYLE 🔒

Our custom rustc driver will not be run in an proper terminal, thus logs would appear uncolored. When no RUST_LOG_STYLE env. var. is set, rust_log_style checks wether the cargo hax command was run inside a terminal. If it was inside a terminal, rust_log_style returns "always", which is the usual default behavior. Otherwise we return "never". When RUST_LOG_STYLE is set, we just return its value.

Traits

ExtHaxMessage 🔒

Functions

compute_haxmeta_files 🔒

Calls cargo with a custom driver which computes haxmeta files in TARGET. One haxmeta file is produced by crate. Each haxmeta file contains the full AST of one crate.

find_hax_engine 🔒

Dynamically looks for binary ENGINE_BINARY_NAME. First, we check whether [HAX_ENGINE_BINARY] is set, and use that if it is. Then, we try to find ENGINE_BINARY_NAME in PATH. If not found, detect whether nodejs is available, download the JS-compiled engine and use it.

find_rust_hax_engine 🔒

get_args

get_args is a wrapper of std::env::args that strips a possible cargo subcommand. This allows for a binary BINARY to be called both with cargo BINARY args... and cargo-BINARY args....

get_hax_rustc_driver_path 🔒

Returns the path to the custom rustc driver used by cargo-hax.

get_hax_version 🔒

Gets hax version: if hax is being compiled from a dirty git repo, then this function taints the hax version with the hash of the current executable. This makes sure cargo doesn’t cache across different versions of hax, for more information see https://github.com/hacspec/hax/issues/801.

main 🔒

run_command 🔒

Run the command given by the user

run_engine 🔒

Runs hax-engine

rust_log_style 🔒

rustflags 🔒

target_dir 🔒

Uses cargo metadata to compute a derived target directory.

toolchain 🔒

Return a toolchain argument to pass to cargo: when the correct nightly is already present, this is None, otherwise we (1) ensure rustup is available (2) install the nightly (3) return the toolchain