Skip to content

Commit

Permalink
fix(test-harness): hax-engine-names-extract needs hax in PATH
Browse files Browse the repository at this point in the history
This commit fixes the test harness: since
#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.
  • Loading branch information
W95Psp committed Apr 25, 2024
1 parent 3eb14e3 commit a03c1b4
Show file tree
Hide file tree
Showing 2 changed files with 20 additions and 5 deletions.
3 changes: 2 additions & 1 deletion engine/names/extract/build.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
22 changes: 18 additions & 4 deletions test-harness/src/command_hax_ext.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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());
Expand All @@ -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"),
})
};
Expand Down

0 comments on commit a03c1b4

Please sign in to comment.