Merge pull request #1007 from hacspec/improve-hax-version

feat(cli): better version information

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)
     }

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();
 }

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<EmitHaxMetaMessage>, 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)

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]))
+        }
+    });
 }

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<E: Extension> {
     /// Replace the expansion of each macro matching PATTERN by their
     /// invocation. PATTERN denotes a rust path (i.e. `A::B::c`) in

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");

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/)"