Enable pervasive to be built as a dependency

verus-lang · Jul 26, 2023 · cca8318 · cca8318
1 parent 3ac9e37
commit cca8318
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 0 deletions.
diff --git a/source/pervasive/Cargo.toml b/source/pervasive/Cargo.toml
@@ -0,0 +1,12 @@
+[package]
+name = "vstd"
+version = "0.1.0"
+edition = "2018"
+
+[lib]
+name = "vstd"
+path = "vstd.rs"
+
+[dependencies]
+builtin_macros = { path = "../builtin_macros" }
+builtin = { path = "../builtin" }
diff --git a/source/pervasive/vstd.rs b/source/pervasive/vstd.rs
@@ -8,6 +8,16 @@
 
 #![feature(core_intrinsics)]
 
+#![cfg_attr(
+    not(verus_build),
+    feature(allocator_api),
+    feature(rustc_attrs),
+    feature(negative_impls),
+    feature(tuple_trait),
+    feature(unboxed_closures),
+    allow(unused)
+)]
+
 pub mod pervasive;
 pub mod bytes;
 pub mod calc_macro;

diff --git a/source/vstd_build/src/main.rs b/source/vstd_build/src/main.rs
@@ -81,6 +81,8 @@ fn main() {
         "--edition=2018".to_string(),
         "--cfg".to_string(),
         "erasure_macro_todo".to_string(),
+        "--cfg".to_string(),
+        "verus_build".to_string(),
         "--crate-type=lib".to_string(),
         "--out-dir".to_string(),
         verus_target_path.to_str().expect("invalid path").to_string(),