From 338a4443705bd70ede956908f2d37ab0f0b999db Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.dev>
Date: Tue, 2 Jul 2024 08:18:31 +0200
Subject: [PATCH] feat(cli): use a hax-specific target directory

---
 Cargo.lock                       |  2 ++
 cli/subcommands/Cargo.toml       |  2 ++
 cli/subcommands/src/cargo_hax.rs | 11 +++++++++++
 hax-types/src/cli_options.rs     |  7 +++++++
 4 files changed, 22 insertions(+)

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<EmitHaxMetaMessage>, 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 <PKG> ;`).
     #[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 {