diff --git a/Cargo.lock b/Cargo.lock index 5b250b3b2..b5392eb57 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -158,6 +158,8 @@ name = "cargo-hax" version = "0.1.0-pre.1" dependencies = [ "annotate-snippets", + "camino", + "cargo_metadata", "clap", "colored", "const_format", diff --git a/cli/subcommands/Cargo.toml b/cli/subcommands/Cargo.toml index d667f9436..e0e026f9f 100644 --- a/cli/subcommands/Cargo.toml +++ b/cli/subcommands/Cargo.toml @@ -42,6 +42,8 @@ annotate-snippets.workspace = true serde-jsonlines = "0.5.0" prettyplease = "0.2.20" syn = { version = "2.*", features = ["full"] } +cargo_metadata.workspace = true +camino = "1.1" [build-dependencies] serde.workspace = true diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs index c7c77a0c7..940253e25 100644 --- a/cli/subcommands/src/cargo_hax.rs +++ b/cli/subcommands/src/cargo_hax.rs @@ -282,6 +282,14 @@ fn run_engine( error } +/// Uses `cargo metadata` to compute a derived target directory. +fn target_dir(suffix: &str) -> camino::Utf8PathBuf { + let metadata = cargo_metadata::MetadataCommand::new().exec().unwrap(); + let mut dir = metadata.target_directory; + dir.push(suffix); + dir +} + /// 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. @@ -298,6 +306,9 @@ fn compute_haxmeta_files(options: &Options) -> (Vec, i32) { cmd.args([COLOR_FLAG, "always"]); } cmd.stderr(std::process::Stdio::piped()); + if !options.no_custom_target_directory { + cmd.env("CARGO_TARGET_DIR", target_dir("hax")); + }; cmd.env( "RUSTC_WORKSPACE_WRAPPER", std::env::var("HAX_RUSTC_DRIVER_BINARY") diff --git a/hax-types/src/cli_options.rs b/hax-types/src/cli_options.rs index b8b4b87d5..8657999f7 100644 --- a/hax-types/src/cli_options.rs +++ b/hax-types/src/cli_options.rs @@ -427,6 +427,13 @@ pub struct Options { /// options like `-C -p ;`). #[arg(long = "deps")] pub deps: bool, + + /// By default, hax use `$CARGO_TARGET_DIR/hax` as target folder, + /// to avoid recompilation when working both with `cargo hax` and + /// `cargo build` (or, e.g. `rust-analyzer`). This option disables + /// this behavior. + #[arg(long)] + pub no_custom_target_directory: bool, } impl NormalizePaths for Command {