From f540bf72c7fe6152f0ac13e1ed8832c8d489b31f Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 16 Oct 2024 13:20:34 +0200 Subject: [PATCH 1/3] feat(cli): better version information Versions were broken: `cargo hax -V` was displaying the latest tag attached to the commit. So newer commits on main were tagged `v0.1.0-alpha`. Also, if hax is built without git, the version was empty. Now we use `CARGO_PKG_VERSION` as a fallback. --- hax-types/build.rs | 57 +++++++++++++++++++++----------- hax-types/src/cli_options/mod.rs | 9 ++++- hax-types/src/lib.rs | 3 ++ 3 files changed, 49 insertions(+), 20 deletions(-) diff --git a/hax-types/build.rs b/hax-types/build.rs index b4ab527a0..bda3c1c49 100644 --- a/hax-types/build.rs +++ b/hax-types/build.rs @@ -1,24 +1,43 @@ -macro_rules! set_empty_env_var_with_git { - ($var:literal, $args: expr) => { - if let None = option_env!($var) { - println!( - "cargo:rustc-env={}={}", - $var, - std::process::Command::new("git") - .args($args) - .output() - .map(|output| String::from_utf8(output.stdout).unwrap()) - .unwrap_or("unknown".into()) - ); - } +macro_rules! set_empty_env_var_with { + ($var:literal, $f: expr) => {{ println!("cargo:rurun-if-env-changed={}", $var); - }; + match option_env!($var) { + Some(value) => value.to_string(), + None => { + let value = $f; + println!("cargo:rustc-env={}={}", $var, value); + value + } + } + }}; +} + +const UNKNOWN: &str = "unknown"; + +fn git_command(args: &[&str]) -> String { + std::process::Command::new("git") + .args(args) + .output() + .map(|output| String::from_utf8(output.stdout).unwrap().trim().to_string()) + .ok() + .filter(|s| !s.is_empty()) + .unwrap_or(UNKNOWN.to_string()) } fn main() { - set_empty_env_var_with_git!( - "HAX_GIT_DESCRIBE", - ["describe", "--tags", "--always", "--abbrev=0"] - ); - set_empty_env_var_with_git!("HAX_GIT_COMMIT_HASH", ["rev-parse", "HEAD"]); + let commit_hash = + set_empty_env_var_with!("HAX_GIT_COMMIT_HASH", git_command(&["rev-parse", "HEAD"])); + + set_empty_env_var_with!("HAX_VERSION", { + if commit_hash == UNKNOWN { + env!("CARGO_PKG_VERSION").into() + } else { + git_command(&["tag", "--contains", &commit_hash]) + .lines() + .next() + .and_then(|tag| tag.split_once("hax-v")) + .map(|(_, version)| version.trim().to_string()) + .unwrap_or_else(|| format!("untagged-git-rev-{}", &commit_hash[0..10])) + } + }); } diff --git a/hax-types/src/cli_options/mod.rs b/hax-types/src/cli_options/mod.rs index adecc485f..75b771966 100644 --- a/hax-types/src/cli_options/mod.rs +++ b/hax-types/src/cli_options/mod.rs @@ -405,7 +405,14 @@ pub enum ExportBodyKind { #[derive_group(Serializers)] #[derive(JsonSchema, Parser, Debug, Clone)] -#[command(author, version = concat!("commit=", env!("HAX_GIT_COMMIT_HASH"), " ", "describe=", env!("HAX_GIT_DESCRIBE")), name = "hax", about, long_about = None)] +#[command( + author, + version = crate::HAX_VERSION, + long_version = concat!("\nversion=", env!("HAX_VERSION"), "\n", "commit=", env!("HAX_GIT_COMMIT_HASH")), + name = "hax", + about, + long_about = None +)] pub struct ExtensibleOptions { /// Replace the expansion of each macro matching PATTERN by their /// invocation. PATTERN denotes a rust path (i.e. `A::B::c`) in diff --git a/hax-types/src/lib.rs b/hax-types/src/lib.rs index ab974d41b..b59b7b0d0 100644 --- a/hax-types/src/lib.rs +++ b/hax-types/src/lib.rs @@ -25,3 +25,6 @@ pub mod driver_api; /// The types used to communicate between `cargo-hax` and /// `hax-engine`. pub mod engine_api; + +/// Compile-time version of hax +pub const HAX_VERSION: &str = env!("HAX_VERSION"); From 476cfa3df0a6ff7a8724067c14b49a9077b636c1 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 16 Oct 2024 14:41:16 +0200 Subject: [PATCH 2/3] feat(justfile): test recipies --- justfile | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/justfile b/justfile index 1f3478f9d..0abf3bce6 100644 --- a/justfile +++ b/justfile @@ -40,6 +40,17 @@ fmt: cargo fmt cd engine && dune fmt +# Run hax tests: each test crate has a snapshot, so that we track changes in extracted code. If a snapshot changed, please review them with `just test-review`. +test: + cargo test --test toolchain + +_test: + CARGO_TESTS_ASSUME_BUILT=1 cargo test --test toolchain + +# Review snapshots +test-review: (_ensure_command_in_path "cargo-insta" "Insta (https://insta.rs)") + cargo insta review + # Check the coherency between issues labeled `marked-unimplemented` on GitHub and issues mentionned in the engine in the `Unimplemented {issue_id: ...}` errors. @check-issues: just _ensure_command_in_path jq "jq (https://jqlang.github.io/jq/)" From f5c6f4972ab569e33aedc38541e9bb9f399778fd Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 16 Oct 2024 15:52:27 +0200 Subject: [PATCH 3/3] fix(cli): invalidate cargo cache when hax version changes This commit takes into account hax version for cargo cache. Also, if hax was built from a dirty git, the version is tainted with a hash of the driver itself. --- cli/driver/src/callbacks_wrapper.rs | 10 +++++++++- cli/subcommands/build.rs | 17 +++++++++++++++++ cli/subcommands/src/cargo_hax.rs | 24 ++++++++++++++++++++++++ 3 files changed, 50 insertions(+), 1 deletion(-) diff --git a/cli/driver/src/callbacks_wrapper.rs b/cli/driver/src/callbacks_wrapper.rs index 5a5bc28a1..1ba359288 100644 --- a/cli/driver/src/callbacks_wrapper.rs +++ b/cli/driver/src/callbacks_wrapper.rs @@ -14,10 +14,18 @@ impl<'a> Callbacks for CallbacksWrapper<'a> { fn config(&mut self, config: &mut interface::Config) { let options = self.options.clone(); config.psess_created = Some(Box::new(move |parse_sess| { - parse_sess.env_depinfo.get_mut().insert(( + let depinfo = parse_sess.env_depinfo.get_mut(); + depinfo.insert(( Symbol::intern(ENV_VAR_OPTIONS_FRONTEND), Some(Symbol::intern(&serde_json::to_string(&options).unwrap())), )); + depinfo.insert(( + Symbol::intern("HAX_CARGO_CACHE_KEY"), + std::env::var("HAX_CARGO_CACHE_KEY") + .ok() + .as_deref() + .map(Symbol::intern), + )); })); self.sub.config(config) } diff --git a/cli/subcommands/build.rs b/cli/subcommands/build.rs index 224b4037c..b1a0402c2 100644 --- a/cli/subcommands/build.rs +++ b/cli/subcommands/build.rs @@ -33,7 +33,24 @@ fn json_schema_static_asset() { .unwrap(); } +fn git_dirty_env_var() { + println!("cargo:rurun-if-env-changed=HAX_GIT_IS_DIRTY"); + let dirty = { + use std::process::Command; + let _ = Command::new("git") + .args(["update-index", "-q", "--refresh"]) + .status(); + !Command::new("git") + .args(["diff-index", "--quiet", "HEAD", "--"]) + .status() + .map(|status| status.success()) + .unwrap_or(true) + }; + println!("cargo:rustc-env=HAX_GIT_IS_DIRTY={}", dirty); +} + fn main() { rustc_version_env_var(); json_schema_static_asset(); + git_dirty_env_var(); } diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs index 36d70d9a9..c3ee00316 100644 --- a/cli/subcommands/src/cargo_hax.rs +++ b/cli/subcommands/src/cargo_hax.rs @@ -362,6 +362,29 @@ fn target_dir(suffix: &str) -> PathBuf { dir.into() } +/// 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. +fn get_hax_version() -> String { + let mut version = hax_types::HAX_VERSION.to_string(); + if env!("HAX_GIT_IS_DIRTY") == "true" { + version += &std::env::current_exe() + .ok() + .and_then(|exe_path| std::fs::read(exe_path).ok()) + .map(|contents| { + use std::hash::{DefaultHasher, Hash, Hasher}; + let mut s = DefaultHasher::new(); + contents.hash(&mut s); + format!("hash-exe-{}", s.finish()) + }) + .expect("Expect read path") + } + + version +} + /// 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. @@ -393,6 +416,7 @@ fn compute_haxmeta_files(options: &Options) -> (Vec, i32) { ) .env(RUST_LOG_STYLE, rust_log_style()) .env(RUSTFLAGS, rustflags()) + .env("HAX_CARGO_CACHE_KEY", get_hax_version()) .env( ENV_VAR_OPTIONS_FRONTEND, serde_json::to_string(&options)