From a03c1b4f3a75e604fe0548e086b06caffca4109e Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 24 Apr 2024 17:59:36 +0200
Subject: [PATCH] fix(test-harness): `hax-engine-names-extract` needs hax in
 PATH

This commit fixes the test harness: since
https://github.com/hacspec/hax/pull/428, the test harness silently
assumes hax is in PATH while building the crate
`hax-engine-names-extract`.

This crate `hax-engine-names-extract` is used at build time by the
engine to list and import the Rust names we rely on.

`hax-engine-names-extract` itself requires the Rust part of hax at
build time.

This PR fixes the test harness so that:
 1. it asks cargo to build `cargo-hax` and the driver
 2. it looks for the path of `cargo-hax` & driver just built (somewhere local in `target/bin/something/someting`), injects thoses paths as env vars in a `cargo build --bin hax-engine-names-extract`;
 3. it compiles the engine with the three paths mentioned above (which are required by the engine at compile time);
 4. it runs full hax (frontend + engine) on the actual tests;
 5. compare with snapshots.
---
 engine/names/extract/build.rs       |  3 ++-
 test-harness/src/command_hax_ext.rs | 22 ++++++++++++++++++----
 2 files changed, 20 insertions(+), 5 deletions(-)

diff --git a/engine/names/extract/build.rs b/engine/names/extract/build.rs
index e9482ce69..00400f27b 100644
--- a/engine/names/extract/build.rs
+++ b/engine/names/extract/build.rs
@@ -123,7 +123,8 @@ fn target_dir(suffix: &str) -> camino::Utf8PathBuf {
 }
 
 fn get_json() -> String {
-    let mut cmd = Command::new("cargo-hax");
+    let mut cmd =
+        Command::new(std::env::var("HAX_CARGO_COMMAND_PATH").unwrap_or("cargo-hax".to_string()));
     cmd.args([
         "hax",
         "-C",
diff --git a/test-harness/src/command_hax_ext.rs b/test-harness/src/command_hax_ext.rs
index ff404a25f..ff830bc8c 100644
--- a/test-harness/src/command_hax_ext.rs
+++ b/test-harness/src/command_hax_ext.rs
@@ -33,9 +33,23 @@ impl CommandHaxExt for Command {
                 let root = std::env::current_dir().unwrap();
                 let root = root.parent().unwrap();
                 let engine_dir = root.join("engine");
-                // Make sure binaries are built
+                // Make sure binaries are built. Note this doesn't
+                // include `hax-engine-names-extract`: its build
+                // script requires the driver and CLI of `hax` to be
+                // available.
                 assert!(Command::new("cargo")
-                        .args(&["build", "--workspace", "--bins"])
+                            .args(&["build", "--bins"])
+                            .status()
+                            .unwrap()
+                            .success());
+                let cargo_hax = cargo_bin(CARGO_HAX);
+                let driver = cargo_bin("driver-hax-frontend-exporter");
+                // Now the driver & CLI are installed, call `cargo
+                // build` injecting their paths
+                assert!(Command::new("cargo")
+                        .args(&["build", "--workspace", "--bin", "hax-engine-names-extract"])
+                        .env("HAX_CARGO_COMMAND_PATH", &cargo_hax)
+                        .env("HAX_RUSTC_DRIVER_BINARY", &driver)
                         .status()
                         .unwrap()
                         .success());
@@ -49,8 +63,8 @@ impl CommandHaxExt for Command {
                         .unwrap()
                         .success());
                 Some(Paths {
-                    driver: cargo_bin("driver-hax-frontend-exporter"),
-                    cargo_hax: cargo_bin(CARGO_HAX),
+                    driver,
+                    cargo_hax,
                     engine: engine_dir.join("_build/install/default/bin/hax-engine"),
                 })
             };