Install Kani's runtime dependencies and fix Rust CI

celinval · Jun 11, 2024 · 8d18976 · 8d18976
1 parent f7269e2
commit 8d18976
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 3 deletions.
diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
@@ -26,6 +26,11 @@ jobs:
       matrix:
         # Kani does not support windows.
         os: [ubuntu-latest, macos-latest]
+        include:
+          - os: ubuntu-latest
+            base: ubuntu
+          - os: macos-latest
+            base: macos
     steps:
       - name: Checkout Library
         uses: actions/checkout@v4
@@ -41,6 +46,11 @@ jobs:
           path: kani
           ref: features/verify-rust-std
 
+      - name: Setup Dependencies
+        working-directory: kani
+        run: |
+          ./scripts/setup/${{ matrix.base }}/install_deps.sh
+
       - name: Build `Kani`
         working-directory: kani
         run: |

diff --git a/.github/workflows/rustc.yml b/.github/workflows/rustc.yml
@@ -61,6 +61,9 @@ jobs:
 
       - name: Run tests
         working-directory: upstream
+        env:
+          # Avoid error due to unexpected `cfg`
+          RUSTFLAGS: "--check-cfg=cfg(kani_host,kani)"
         run: |
           ./configure --set=llvm.download-ci-llvm=true
           ./x test --stage 0 library/std
diff --git a/library/contracts/safety/src/runtime.rs b/library/contracts/safety/src/runtime.rs
@@ -1,6 +1,4 @@
-use proc_macro::{TokenStream};
-use quote::{quote, format_ident};
-use syn::{ItemFn, parse_macro_input};
+use proc_macro::TokenStream;
 
 /// For now, runtime requires is a no-op.
 ///