actually disable macros with cfg

hax-lib/Cargo.toml

@@ -9,11 +9,14 @@ repository.workspace = true
 readme = "README.md"
 description = "Hax-specific helpers for Rust programs"
 
-[dependencies]
-hax-lib-macros = { workspace = true, optional = true }
+
+[target.'cfg(hax)'.dependencies]
 num-bigint = { version = "0.4.3", default-features = false, optional = true }
 num-traits = { version = "0.2.15", default-features = false, optional = true }
 
+[dependencies]
+hax-lib-macros = { workspace = true, optional = true }
+
 [features]
 default = ["macros", "hax"]
 macros = ["dep:hax-lib-macros"]

hax-lib/macros/Cargo.toml

@@ -12,18 +12,29 @@ description = "Hax-specific proc-macros for Rust programs"
 [lib]
 proc-macro = true
 
-[dependencies]
+[target.'cfg(hax)'.dependencies]
 proc-macro-error = { version = "1.0.4", optional = true }
+hax-lib-macros-types = { workspace = true, optional = true }
+paste = { version = "1.0.15", optional = true }
+
+[dependencies]
 proc-macro2 = { workspace = true, optional = true }
 quote = { workspace = true }
 syn = { version = "2.0", features = ["full", "visit-mut"] }
-hax-lib-macros-types = { workspace = true, optional = true }
-paste = { version = "1.0.15", optional = true }
 
 [features]
-hax = [ "dep:paste", "dep:hax-lib-macros-types", "dep:proc-macro-error", "dep:proc-macro2",
-        "syn/visit", "syn/extra-traits", "syn/parsing"
-      ]
+hax = [
+    "dep:paste",
+    "dep:hax-lib-macros-types",
+    "dep:proc-macro-error",
+    "dep:proc-macro2",
+    "syn/visit",
+    "syn/extra-traits",
+    "syn/parsing",
+]
 
 [dev-dependencies]
 hax-lib = { path = ".." }
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(hax)', 'cfg(doc_cfg)'] }

hax-lib/macros/src/dummy.rs

@@ -61,7 +61,7 @@ pub fn lemma(_attr: TokenStream, _item: TokenStream) -> TokenStream {
 }
 
 fn unsafe_expr() -> TokenStream {
-    quote! { ::std::compile_error!("`hax_lib::unsafe_expr` has no meaning outside of hax extraction, please use it solely on hax only places.") }.into()
+    quote! {}.into()
 }
 
 #[proc_macro]

hax-lib/macros/src/lib.rs

@@ -1,8 +1,8 @@
 // Proc-macros must "reside in the root of the crate": whence the use
 // of `std::include!` instead of proper module declaration.
 
-#[cfg(feature = "hax")]
+#[cfg(hax)]
 std::include!("implementation.rs");
 
-#[cfg(not(feature = "hax"))]
+#[cfg(not(hax))]
 std::include!("dummy.rs");

hax-lib/src/dummy.rs

@@ -11,7 +11,7 @@ macro_rules! debug_assert {
 #[macro_export]
 macro_rules! assert {
     ($($arg:tt)*) => {
-        ::core::assert!($arg);
+        ::core::assert!($($arg)*);
     };
 }
 

hax-lib/src/lib.rs

@@ -18,11 +18,11 @@
 #[cfg(feature = "macros")]
 mod proc_macros;
 
-// hax engine relies on `hax-lib` names: to avoid clutering names with
+// hax engine relies on `hax-lib` names: to avoid cluttering names with
 // an additional `implementation` in all paths, we `include!` instead
 // of doing conditional `mod` and `pub use`.
 
-#[cfg(not(feature = "hax"))]
+#[cfg(not(hax))]
 core::include!("dummy.rs");
-#[cfg(feature = "hax")]
+#[cfg(hax)]
 core::include!("implementation.rs");

hax-lib/src/proc_macros.rs

@@ -2,10 +2,12 @@
 //! proc-macro crate cannot export anything but procedural macros.
 
 pub use hax_lib_macros::{
-    attributes, ensures, exclude, impl_fn_decoration, include, lemma, loop_invariant, opaque_type,
-    refinement_type, requires, trait_fn_decoration,
+    attributes, ensures, exclude, include, lemma, opaque_type, refinement_type, requires,
 };
 
+#[cfg(hax)]
+pub use hax_lib_macros::{impl_fn_decoration, loop_invariant, trait_fn_decoration};
+
 pub use hax_lib_macros::{
     process_init, process_read, process_write, protocol_messages, pv_constructor, pv_handwritten,
 };