Merge pull request #703 from hacspec/faster-builds

feat: isolate `DefId`: faster build times

PUBLISHING.md

@@ -25,6 +25,7 @@ and `examples`):
 - `hax-phase-debug-webapp`
 - `hax-driver`
 
+
 ## hax-lib
 
 1. `hax-lib-macros-types`
@@ -34,3 +35,10 @@ and `examples`):
 ---
 
 - `hax-lint`
+
+## Supporting crates for the engine
+The crate listed below are used only by the OCaml build of the
+engine. Those should not be published on `crate.io`.
+
+1. `cargo-hax-engine-names`
+2. `cargo-hax-engine-names-extract`

cli/subcommands/src/cargo_hax.rs

@@ -63,8 +63,7 @@ fn rust_log_style() -> String {
 const RUSTFLAGS: &str = "RUSTFLAGS";
 fn rustflags() -> String {
     let rustflags = std::env::var(RUSTFLAGS).unwrap_or("".into());
-    let space = rustflags.is_empty().then_some(" ").unwrap_or("");
-    format!("{rustflags}{space}--cfg hax")
+    [rustflags, "--cfg hax".into()].join(" ")
 }
 
 fn main() {

engine/names/extract/Cargo.toml

@@ -12,10 +12,13 @@ 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
 hax-engine-names.workspace = true
 tempfile.version = "3.9"
 camino = "1.1"
+
+[features]
+default = ["extract_names_mode"]
+extract_names_mode = []

engine/names/extract/build.rs

@@ -1,8 +1,16 @@
-use hax_frontend_exporter::{DefId, DefPathItem, DisambiguatedDefPathItem};
 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::*;
+
 /// Name of the current crate
 const HAX_ENGINE_NAMES_CRATE: &str = "hax_engine_names";
 /// Path `a::b` needs to be compiled to a OCaml variant name, `::` is

frontend/exporter/src/types/copied.rs

@@ -2,32 +2,6 @@ use crate::prelude::*;
 use crate::rustc_middle::query::Key;
 use rustc_middle::ty;
 
-/// Reflects [`rustc_hir::definitions::DisambiguatedDefPathData`]
-#[derive(
-    AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
-)]
-#[args(<'a, S: BaseState<'a>>, from: rustc_hir::definitions::DisambiguatedDefPathData, state: S as s)]
-pub struct DisambiguatedDefPathItem {
-    pub data: DefPathItem,
-    pub disambiguator: u32,
-}
-
-/// Reflects [`rustc_hir::def_id::DefId`]
-#[derive(Clone, Debug, Serialize, Deserialize, JsonSchema, PartialEq, Eq, PartialOrd, Ord)]
-pub struct DefId {
-    pub krate: String,
-    pub path: Vec<DisambiguatedDefPathItem>,
-    /// Rustc's `CrateNum` and `DefIndex` raw indexes. This can be
-    /// useful if one needs to convert a [`DefId`] into a
-    /// [`rustc_hir::def_id::DefId`]; there is a `From` instance for
-    /// that purpose.
-    ///
-    /// **Warning: this `index` field might not be safe to use**. They are
-    /// valid only for one Rustc sesssion. Please do not rely on those
-    /// indexes unless you cannot do otherwise.
-    pub index: (u32, u32),
-}
-
 impl std::hash::Hash for DefId {
     fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
         let DefId {
@@ -98,28 +72,6 @@ pub enum LogicalOp {
     Or,
 }
 
-/// Reflects [`rustc_hir::definitions::DefPathData`]
-#[derive(
-    AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
-)]
-#[args(<'ctx, S: BaseState<'ctx>>, from: rustc_hir::definitions::DefPathData, state: S as state)]
-pub enum DefPathItem {
-    CrateRoot,
-    Impl,
-    ForeignMod,
-    Use,
-    GlobalAsm,
-    TypeNs(Symbol),
-    ValueNs(Symbol),
-    MacroNs(Symbol),
-    LifetimeNs(Symbol),
-    ClosureExpr,
-    Ctor,
-    AnonConst,
-    ImplTrait,
-    ImplTraitAssocTy,
-}
-
 /// Reflects [`rustc_middle::thir::LintLevel`]
 #[derive(
     AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,

frontend/exporter/src/types/def_id.rs

@@ -0,0 +1,65 @@
+//! This module contains the type definition for `DefId` and the types
+//! `DefId` depends on.
+//!
+//! This is purposely a very small isolated module:
+//! `hax-engine-names-extract` uses those types, but we don't want
+//! `hax-engine-names-extract` to have a build dependency on the whole
+//! frontend, that double the build times for the Rust part of hax.
+//!
+//! The feature `extract_names_mode` exists only in the crate
+//! `hax-engine-names-extract`, and is used to turn off the derive
+//! attributes `AdtInto` and `JsonSchema`.
+
+pub use serde::{Deserialize, Serialize};
+
+#[cfg(not(feature = "extract_names_mode"))]
+use crate::{AdtInto, BaseState, JsonSchema, SInto};
+
+pub type Symbol = String;
+
+#[derive(Clone, Debug, Serialize, Deserialize, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[cfg_attr(not(feature = "extract_names_mode"), derive(AdtInto, JsonSchema))]
+#[cfg_attr(not(feature = "extract_names_mode"), args(<'a, S: BaseState<'a>>, from: rustc_hir::definitions::DisambiguatedDefPathData, state: S as s))]
+/// Reflects [`rustc_hir::definitions::DisambiguatedDefPathData`]
+pub struct DisambiguatedDefPathItem {
+    pub data: DefPathItem,
+    pub disambiguator: u32,
+}
+
+/// Reflects [`rustc_hir::def_id::DefId`]
+#[derive(Clone, Debug, Serialize, Deserialize, PartialEq, Eq, PartialOrd, Ord)]
+#[cfg_attr(not(feature = "extract_names_mode"), derive(JsonSchema))]
+pub struct DefId {
+    pub krate: String,
+    pub path: Vec<DisambiguatedDefPathItem>,
+    /// Rustc's `CrateNum` and `DefIndex` raw indexes. This can be
+    /// useful if one needs to convert a [`DefId`] into a
+    /// [`rustc_hir::def_id::DefId`]; there is a `From` instance for
+    /// that purpose.
+    ///
+    /// **Warning: this `index` field might not be safe to use**. They are
+    /// valid only for one Rustc sesssion. Please do not rely on those
+    /// indexes unless you cannot do otherwise.
+    pub index: (u32, u32),
+}
+
+/// Reflects [`rustc_hir::definitions::DefPathData`]
+#[derive(Clone, Debug, Serialize, Deserialize, Hash, PartialEq, Eq, PartialOrd, Ord)]
+#[cfg_attr(not(feature = "extract_names_mode"), derive(AdtInto, JsonSchema))]
+#[cfg_attr(not(feature = "extract_names_mode"), args(<'ctx, S: BaseState<'ctx>>, from: rustc_hir::definitions::DefPathData, state: S as state))]
+pub enum DefPathItem {
+    CrateRoot,
+    Impl,
+    ForeignMod,
+    Use,
+    GlobalAsm,
+    TypeNs(Symbol),
+    ValueNs(Symbol),
+    MacroNs(Symbol),
+    LifetimeNs(Symbol),
+    ClosureExpr,
+    Ctor,
+    AnonConst,
+    ImplTrait,
+    ImplTraitAssocTy,
+}

frontend/exporter/src/types/mod.rs

@@ -2,6 +2,7 @@
 #![allow(ambiguous_glob_reexports)]
 
 mod copied;
+mod def_id;
 mod index;
 mod mir;
 mod mir_traits;
@@ -10,6 +11,7 @@ mod replaced;
 mod todo;
 
 pub use copied::*;
+pub use def_id::*;
 pub use index::*;
 pub use mir::*;
 pub use mir_traits::*;

frontend/exporter/src/types/replaced.rs

@@ -2,7 +2,6 @@ use crate::prelude::*;
 
 pub type Path = Vec<String>;
 
-pub type Symbol = String;
 impl<'t, S> SInto<S, Symbol> for rustc_span::symbol::Symbol {
     fn sinto(&self, _s: &S) -> Symbol {
         self.to_ident_string()