feat(cli): split cli options to isolate the ones for the exporter

W95Psp · W95Psp · commit 141f7785a83d · 2025-09-29T10:37:58.000+02:00
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -30,6 +30,9 @@ Changes to the frontend:
 - Add infrastructure to get a monomorphized `FullDef`; this is used in charon to monomorphize a crate graph (#1559)
 - Fix a regression affecting projection predicates (#1678)
 
+Change to cargo-hax:
+- Improve the caching of rustc when using `cargo hax` commands (#1719)
+
 Changes to hax-lib:
 - New behavior for `hax_lib::include`: it now forces inclusion when in contradiction with `-i` flag.
 
diff --git a/cli/driver/src/callbacks_wrapper.rs b/cli/driver/src/callbacks_wrapper.rs
@@ -1,4 +1,4 @@
-use hax_types::cli_options::{Command, ENV_VAR_OPTIONS_FRONTEND, Options};
+use hax_types::cli_options::{ENV_VAR_OPTIONS_FRONTEND, ExporterOptions};
 
 use rustc_ast::Crate;
 use rustc_driver::{Callbacks, Compilation};
@@ -10,7 +10,7 @@ use rustc_span::symbol::Symbol;
 /// configuration in the `config` phase of rustc
 pub struct CallbacksWrapper<'a> {
     pub sub: &'a mut (dyn Callbacks + Send + 'a),
-    pub options: Options,
+    pub options: ExporterOptions,
 }
 impl<'a> Callbacks for CallbacksWrapper<'a> {
     fn config(&mut self, config: &mut interface::Config) {
diff --git a/cli/driver/src/driver.rs b/cli/driver/src/driver.rs
@@ -37,7 +37,7 @@ mod features;
 use callbacks_wrapper::*;
 use features::*;
 
-use hax_types::cli_options::{BackendOptions, Command, ENV_VAR_OPTIONS_FRONTEND};
+use hax_types::cli_options::{ENV_VAR_OPTIONS_FRONTEND, ExporterOptions};
 
 use rustc_driver::{Callbacks, Compilation};
 use rustc_interface::interface;
@@ -74,7 +74,7 @@ const HAX_VANILLA_RUSTC: &str = "HAX_VANILLA_RUSTC";
 fn main() {
     setup_logging();
 
-    let options: hax_types::cli_options::Options = serde_json::from_str(
+    let options: ExporterOptions = serde_json::from_str(
         &std::env::var(ENV_VAR_OPTIONS_FRONTEND).unwrap_or_else(|_| {
             panic!(
                 "Cannot find environnement variable {}",
@@ -124,7 +124,7 @@ fn main() {
         !vanilla_rustc && !is_build_script && (options.deps || is_primary_package);
     let mut callbacks: Box<dyn Callbacks + Send> = if translate_package {
         Box::new(exporter::ExtractionCallbacks {
-            body_types: options.command.body_kinds(),
+            body_kinds: options.body_kinds.clone(),
         })
     } else {
         struct CallbacksNoop;
@@ -149,11 +149,9 @@ fn main() {
                 "--cfg".into(),
                 hax_lib_macros_types::HAX_CFG_OPTION_NAME.into(),
             ])
-            .chain(match &options.command {
-                Command::Backend(BackendOptions { backend, .. }) => {
-                    vec!["--cfg".into(), format!("hax_backend_{backend}")]
-                }
-                _ => vec![],
+            .chain(match &options.backend {
+                Some(backend) => vec!["--cfg".into(), format!("hax_backend_{backend}")],
+                None => vec![],
             })
             .chain(features.into_iter().map(|s| format!("-Zcrate-attr={}", s)))
             .chain(rustc_args[1..].iter().cloned())
diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs
@@ -1,6 +1,6 @@
 use hax_frontend_exporter::SInto;
 use hax_frontend_exporter::state::LocalContextS;
-use hax_types::cli_options::{Backend, ENV_VAR_OPTIONS_FRONTEND, PathOrDash};
+use hax_types::cli_options::PathOrDash;
 use rustc_driver::{Callbacks, Compilation};
 use rustc_interface::interface;
 use rustc_interface::interface::Compiler;
@@ -64,7 +64,7 @@ fn convert_thir<'tcx, Body: hax_frontend_exporter::IsBody>(
 /// Callback for extraction
 #[derive(Debug, Clone, Serialize)]
 pub(crate) struct ExtractionCallbacks {
-    pub body_types: Vec<hax_types::cli_options::ExportBodyKind>,
+    pub body_kinds: Vec<hax_types::cli_options::ExportBodyKind>,
 }
 
 impl From<ExtractionCallbacks> for hax_frontend_exporter_options::Options {
@@ -122,7 +122,7 @@ impl Callbacks for ExtractionCallbacks {
 
         use hax_types::driver_api::{HaxMeta, with_kind_type};
         with_kind_type!(
-            self.body_types.clone(),
+            self.body_kinds.clone(),
             <Body>|| {
                 let (spans, def_ids, impl_infos, items, cache_map) =
                     convert_thir(&self.clone().into(), tcx);
diff --git a/cli/driver/src/features.rs b/cli/driver/src/features.rs
@@ -79,7 +79,10 @@ impl Features {
     }
     /// Runs Rustc with a driver that only collects which unstable
     /// Rustc features are enabled
-    pub fn detect(options: &hax_types::cli_options::Options, rustc_args: &Vec<String>) -> Self {
+    pub fn detect(
+        options: &hax_types::cli_options::ExporterOptions,
+        rustc_args: &Vec<String>,
+    ) -> Self {
         struct CollectFeatures {
             features: Features,
         }
diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs
@@ -510,6 +510,7 @@ fn get_hax_rustc_driver_path() -> PathBuf {
 /// in `TARGET`. One `haxmeta` file is produced by crate. Each
 /// `haxmeta` file contains the full AST of one crate.
 fn compute_haxmeta_files(options: &Options) -> (Vec<EmitHaxMetaMessage>, i32) {
+    let frontend_options = ExporterOptions::from(options);
     let mut cmd = {
         let mut cmd = process::Command::new("cargo");
         if let Some(toolchain) = toolchain() {
@@ -536,7 +537,7 @@ fn compute_haxmeta_files(options: &Options) -> (Vec<EmitHaxMetaMessage>, i32) {
             .env("HAX_CARGO_CACHE_KEY", get_hax_version())
             .env(
                 ENV_VAR_OPTIONS_FRONTEND,
-                serde_json::to_string(&options)
+                serde_json::to_string(&frontend_options)
                     .expect("Options could not be converted to a JSON string"),
             );
         cmd
@@ -660,20 +661,20 @@ fn run_command(options: &Options, haxmeta_files: Vec<EmitHaxMetaMessage>) -> boo
 fn main() {
     let args: Vec<String> = get_args("hax");
     let mut options = match &args[..] {
-        [_, kw] if kw == "__json" => serde_json::from_str(
-            &std::env::var(ENV_VAR_OPTIONS_FRONTEND).unwrap_or_else(|_| {
+        [_, kw] if kw == "__json" => {
+            serde_json::from_str(&std::env::var(ENV_VAR_OPTIONS_FULL).unwrap_or_else(|_| {
                 panic!(
                     "Cannot find environnement variable {}",
-                    ENV_VAR_OPTIONS_FRONTEND
+                    ENV_VAR_OPTIONS_FULL
                 )
-            }),
-        )
-        .unwrap_or_else(|_| {
-            panic!(
-                "Invalid value for the environnement variable {}",
-                ENV_VAR_OPTIONS_FRONTEND
-            )
-        }),
+            }))
+            .unwrap_or_else(|_| {
+                panic!(
+                    "Invalid value for the environnement variable {}",
+                    ENV_VAR_OPTIONS_FULL
+                )
+            })
+        }
         _ => Options::parse_from(args.iter()),
     };
     options.normalize_paths();
diff --git a/hax-types/src/cli_options/mod.rs b/hax-types/src/cli_options/mod.rs
@@ -195,16 +195,7 @@ pub enum Backend<E: Extension> {
 
 impl fmt::Display for Backend<()> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        match self {
-            Backend::Fstar { .. } => write!(f, "fstar"),
-            Backend::Coq { .. } => write!(f, "coq"),
-            Backend::Ssprove { .. } => write!(f, "ssprove"),
-            Backend::Easycrypt { .. } => write!(f, "easycrypt"),
-            Backend::ProVerif { .. } => write!(f, "proverif"),
-            Backend::Lean { .. } => write!(f, "lean"),
-            Backend::Rust { .. } => write!(f, "rust"),
-            Backend::GenerateRustEngineNames { .. } => write!(f, "generate_rust_engine_names"),
-        }
+        BackendName::from(self).fmt(f)
     }
 }
 
@@ -537,4 +528,75 @@ impl From<Options> for hax_frontend_exporter_options::Options {
     }
 }
 
+/// The subset of `Options` the frontend is sensible to.
+#[derive_group(Serializers)]
+#[derive(JsonSchema, Debug, Clone)]
+pub struct ExporterOptions {
+    pub deps: bool,
+    pub force_cargo_build: ForceCargoBuild,
+    pub backend: Option<BackendName>,
+    pub body_kinds: Vec<ExportBodyKind>,
+}
+
+#[derive_group(Serializers)]
+#[derive(JsonSchema, Debug, Clone, Copy)]
+pub enum BackendName {
+    Fstar,
+    Coq,
+    Ssprove,
+    Easycrypt,
+    ProVerif,
+    Lean,
+    Rust,
+    GenerateRustEngineNames,
+}
+
+impl fmt::Display for BackendName {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        let name = match self {
+            BackendName::Fstar => "fstar",
+            BackendName::Coq => "coq",
+            BackendName::Ssprove => "ssprove",
+            BackendName::Easycrypt => "easycrypt",
+            BackendName::ProVerif => "proverif",
+            BackendName::Lean => "lean",
+            BackendName::Rust => "rust",
+            BackendName::GenerateRustEngineNames => "generate_rust_engine_names",
+        };
+        write!(f, "{name}")
+    }
+}
+
+impl From<&Options> for ExporterOptions {
+    fn from(options: &Options) -> Self {
+        let backend = match &options.command {
+            Command::Backend(backend_options) => Some((&backend_options.backend).into()),
+            _ => None,
+        };
+        let body_kinds = options.command.body_kinds();
+        ExporterOptions {
+            deps: options.deps,
+            force_cargo_build: options.force_cargo_build.clone(),
+            backend,
+            body_kinds,
+        }
+    }
+}
+
+impl From<&Backend<()>> for BackendName {
+    fn from(backend: &Backend<()>) -> Self {
+        match backend {
+            Backend::Fstar { .. } => BackendName::Fstar,
+            Backend::Coq { .. } => BackendName::Coq,
+            Backend::Ssprove { .. } => BackendName::Ssprove,
+            Backend::Easycrypt { .. } => BackendName::Easycrypt,
+            Backend::ProVerif { .. } => BackendName::ProVerif,
+            Backend::Lean { .. } => BackendName::Lean,
+            Backend::Rust { .. } => BackendName::Rust,
+            Backend::GenerateRustEngineNames { .. } => BackendName::GenerateRustEngineNames,
+        }
+    }
+}
+
 pub const ENV_VAR_OPTIONS_FRONTEND: &str = "DRIVER_HAX_FRONTEND_OPTS";
+pub const ENV_VAR_OPTIONS_FULL: &str = "DRIVER_HAX_FRONTEND_FULL_OPTS";

Original file line number	Diff line number	Diff line change
`@@ -79,7 +79,10 @@ impl Features {`
`79`	`79`	`}`
`80`	`80`	`/// Runs Rustc with a driver that only collects which unstable`
`81`	`81`	`/// Rustc features are enabled`
`82`		`- pub fn detect(options: &hax_types::cli_options::Options, rustc_args: &Vec<String>) -> Self {`
	`82`	`+ pub fn detect(`
	`83`	`+ options: &hax_types::cli_options::ExporterOptions,`
	`84`	`+ rustc_args: &Vec<String>,`
	`85`	`+ ) -> Self {`
`83`	`86`	`struct CollectFeatures {`
`84`	`87`	`features: Features,`
`85`	`88`	`}`