refactor: feature gate all implementations with full

.github/workflows/charon.yml

@@ -12,5 +12,4 @@ jobs:
       - run: |
           cd charon
           cargo update -p hax-frontend-exporter --precise ${{ github.sha }}
-          cargo update -p hax-frontend-exporter-options --precise ${{ github.sha }}
       - run: nix build -L

Cargo.toml

@@ -1,7 +1,6 @@
 [workspace]
 members = [
      "frontend/exporter",
-     "frontend/exporter/options",
      "frontend/diagnostics",
      "frontend/lint",
      "cli/options",
@@ -22,7 +21,6 @@ members = [
 exclude = ["tests"]
 default-members = [
      "frontend/exporter",
-     "frontend/exporter/options",
      "frontend/diagnostics",
      "frontend/lint",
      "cli/options",
@@ -83,7 +81,6 @@ hax-frontend-exporter = { path = "frontend/exporter", version = "=0.1.0-pre.1" }
 hax-adt-into = { path = "frontend/exporter/adt-into", version = "=0.1.0-pre.1" }
 hax-cli-options = { path = "cli/options", version = "=0.1.0-pre.1" }
 hax-cli-options-engine = { path = "cli/options/engine", version = "=0.1.0-pre.1" }
-hax-frontend-exporter-options = { path = "frontend/exporter/options", version = "=0.1.0-pre.1" }
 hax-diagnostics = { path = "frontend/diagnostics", version = "=0.1.0-pre.1" }
 hax-lint = { path = "frontend/lint", version = "=0.1.0-pre.1" }
 hax-phase-debug-webapp = { path = "engine/utils/phase-debug-webapp", version = "=0.1.0-pre.1" }

cli/driver/Cargo.toml

@@ -24,7 +24,6 @@ colored.workspace = true
 hax-frontend-exporter.workspace = true
 hax-cli-options.workspace = true
 hax-cli-options-engine.workspace = true
-hax-frontend-exporter-options.workspace = true
 hax-lint.workspace = true
 hax-diagnostics.workspace = true
 hax-lib-macros-types.workspace = true

cli/driver/src/exporter.rs

@@ -157,7 +157,7 @@ fn precompute_local_thir_bodies<'tcx>(
 /// (I call "THIR'" the AST described in this crate)
 #[tracing::instrument(skip_all)]
 fn convert_thir<'tcx, Body: hax_frontend_exporter::IsBody>(
-    options: &hax_frontend_exporter_options::Options,
+    options: &hax_frontend_exporter::options::Options,
     macro_calls: HashMap<hax_frontend_exporter::Span, hax_frontend_exporter::Span>,
     tcx: TyCtxt<'tcx>,
 ) -> (
@@ -278,9 +278,9 @@ pub(crate) struct ExtractionCallbacks {
     pub macro_calls: HashMap<hax_frontend_exporter::Span, hax_frontend_exporter::Span>,
 }
 
-impl From<ExtractionCallbacks> for hax_frontend_exporter_options::Options {
-    fn from(opts: ExtractionCallbacks) -> hax_frontend_exporter_options::Options {
-        hax_frontend_exporter_options::Options {
+impl From<ExtractionCallbacks> for hax_frontend_exporter::options::Options {
+    fn from(opts: ExtractionCallbacks) -> hax_frontend_exporter::options::Options {
+        hax_frontend_exporter::options::Options {
             inline_macro_calls: opts.inline_macro_calls,
         }
     }
@@ -323,7 +323,7 @@ impl Callbacks for ExtractionCallbacks {
                     include_extra,
                 } => {
                     struct Driver<'tcx> {
-                        options: hax_frontend_exporter_options::Options,
+                        options: hax_frontend_exporter::options::Options,
                         macro_calls:
                             HashMap<hax_frontend_exporter::Span, hax_frontend_exporter::Span>,
                         tcx: TyCtxt<'tcx>,
@@ -452,7 +452,7 @@ impl Callbacks for ExtractionCallbacks {
                             )
                         });
                     let options_frontend =
-                        hax_frontend_exporter_options::Options::from(self.clone());
+                        hax_frontend_exporter::options::Options::from(self.clone());
                     let state =
                         hax_frontend_exporter::state::State::new(tcx, options_frontend.clone());
                     report_diagnostics(

cli/options/Cargo.toml

@@ -15,5 +15,5 @@ serde.workspace = true
 serde_json.workspace = true
 schemars.workspace = true
 clap.workspace = true
-hax-frontend-exporter-options.workspace = true
+hax-frontend-exporter = { workspace = true, features = [] }
 path-clean = "1.0.1"

cli/options/engine/Cargo.toml

@@ -17,7 +17,6 @@ itertools.workspace = true
 clap.workspace = true
 hax-diagnostics.workspace = true
 hax-cli-options.workspace = true
-hax-frontend-exporter.workspace = true
-hax-frontend-exporter-options.workspace = true
+hax-frontend-exporter = { workspace = true, features = [] }
 path-clean = "1.0.1"
 

cli/options/src/lib.rs

@@ -4,7 +4,7 @@ use serde::{Deserialize, Serialize};
 use std::fmt;
 use std::path::{Path, PathBuf};
 
-pub use hax_frontend_exporter_options::*;
+pub use hax_frontend_exporter::options::{self, Namespace};
 
 #[derive(JsonSchema, Debug, Clone, Serialize, Deserialize)]
 pub enum DebugEngineMode {
@@ -449,9 +449,9 @@ impl NormalizePaths for Options {
     }
 }
 
-impl From<Options> for hax_frontend_exporter_options::Options {
-    fn from(opts: Options) -> hax_frontend_exporter_options::Options {
-        hax_frontend_exporter_options::Options {
+impl From<Options> for options::Options {
+    fn from(opts: Options) -> options::Options {
+        options::Options {
             inline_macro_calls: opts.inline_macro_calls,
         }
     }

cli/subcommands/Cargo.toml

@@ -30,7 +30,7 @@ itertools.workspace = true
 clap.workspace = true
 paste = "1.0.11"
 hax-cli-options.workspace = true
-hax-frontend-exporter-options.workspace = true
+hax-frontend-exporter = { workspace = true, features = [] }
 hax-diagnostics.workspace = true
 path-clean = "1.0.1"
 tempfile = "3.8"

engine/names/extract/Cargo.toml

@@ -12,6 +12,7 @@ description = "Helper binary generating an OCaml module"
 
 [build-dependencies]
 hax-cli-options-engine.workspace = true
+hax-frontend-exporter.workspace = true
 serde.workspace = true
 serde_json.workspace = true
 cargo_metadata.workspace = true

engine/names/extract/build.rs

@@ -2,14 +2,7 @@ use serde_json;
 use serde_json::Value;
 use std::process::{Command, Stdio};
 
-/// Instead of depending on `hax_frontend_exporter` (that links to
-/// rustc and exposes a huge number of type definitions and their
-/// impls), we just inline a small module here that contains the three
-/// type definition we need. See the module for complementary
-/// informations.
-#[path = "../../../frontend/exporter/src/types/def_id.rs"]
-mod hax_frontend_exporter_def_id;
-use hax_frontend_exporter_def_id::*;
+use hax_frontend_exporter::{DefId, DefPathItem, DisambiguatedDefPathItem};
 
 /// Name of the current crate
 const HAX_ENGINE_NAMES_CRATE: &str = "hax_engine_names";
@@ -149,9 +142,6 @@ fn get_json() -> String {
     .stderr(Stdio::piped());
 
     cmd.env("CARGO_TARGET_DIR", target_dir("hax"));
-    for env in ["DYLD_FALLBACK_LIBRARY_PATH", "LD_LIBRARY_PATH"] {
-        cmd.env_remove(env);
-    }
     let out = cmd.output().unwrap();
     let stdout = String::from_utf8(out.stdout).unwrap();
     let stderr = String::from_utf8(out.stderr).unwrap();

frontend/exporter/Cargo.toml

@@ -13,13 +13,18 @@ description = "Provides mirrors of the algebraic data types used in the Rust com
 rustc_private=true
 
 [dependencies]
-hax-adt-into.workspace = true
 serde.workspace = true
 serde_json.workspace = true
 schemars.workspace = true
-itertools.workspace = true
-hax-frontend-exporter-options.workspace = true
-tracing.workspace = true
+hax-adt-into.workspace = true
 paste = "1.0.11"
-extension-traits = "1.0.1"
-lazy_static = "1.4.0"
+
+tracing = { workspace = true, optional = true }
+itertools = { workspace = true, optional = true }
+extension-traits = { version = "1.0.1", optional = true }
+lazy_static = { version = "1.4.0", optional = true }
+cfg-if = "1.0.0"
+
+[features]
+default = ["full"]
+full = ["dep:tracing", "dep:itertools", "dep:extension-traits", "dep:lazy_static"]

frontend/exporter/adt-into/src/lib.rs

@@ -384,6 +384,7 @@ pub fn adt_into(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
     };
 
     quote! {
+        #[cfg(feature = "full")]
         const _ : () = {
             use #from as FROM_TYPE;
             use #to as TO_TYPE;