Adding move prover to status checks (MystenLabs#7961)

CelsaSimenez · Feb 1, 2023 · fe574ee · fe574ee
1 parent 552a224
commit fe574ee
Show file tree

Hide file tree

Showing 2 changed files with 42 additions and 0 deletions.
diff --git a/.github/actions/diffs/action.yml b/.github/actions/diffs/action.yml
@@ -7,6 +7,10 @@ outputs:
   isRust:
     description: True when changes happened to the Rust code
     value: "${{ steps.diff.outputs.isRust }}"
+  isMove:
+    description: True when changes happened to the Move code
+    value: "${{ steps.diff.outputs.isMove }}"
+
 runs:
   using: composite
   steps:
@@ -27,3 +31,8 @@ runs:
           - 'doc/**'
           - '*.md'
           - '.github/workflows/docs.yml'
+        isMove:
+          - 'crates/sui-framework/sources/**'
+          - 'crates/sui/src/sui_move/**'
+          - 'Cargo.toml'
+          - 'Cargo.lock'
diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml
@@ -39,6 +39,7 @@ jobs:
     runs-on: [ubuntu-latest]
     outputs:
       isRust: ${{ steps.diff.outputs.isRust }}
+      isMove: ${{ steps.diff.outputs.isMove }}
     steps:
       - uses: actions/checkout@v3
       - name: Detect Changes
@@ -248,3 +249,35 @@ jobs:
     steps:
       - uses: actions/checkout@v3
       - uses: EmbarkStudios/cargo-deny-action@v1
+
+  move-prover:
+    name: move-prover
+    needs: diff
+    timeout-minutes: 20
+    if: needs.diff.outputs.isMove == 'true'
+    runs-on: [ubuntu-ghcloud]
+
+    steps:     
+      - uses: actions/checkout@v3
+      - uses: actions-rs/toolchain@v1
+
+      - name: Prover Setup
+        run: |
+          crates/sui/scripts/prover_setup.sh
+      - name: Build
+        uses: actions-rs/cargo@v1
+        with:
+          command: build
+
+      - name: Prover Run
+        working-directory: crates/sui-framework
+        run: |
+          set -o pipefail
+          DOTNET_ROOT="$HOME/.dotnet"
+          BIN_DIR="$HOME/bin"
+          export DOTNET_ROOT="${DOTNET_ROOT}"
+          export PATH="${DOTNET_ROOT}/tools:\$PATH"
+          export Z3_EXE="${BIN_DIR}/z3"
+          export CVC5_EXE="${BIN_DIR}/cvc5"
+          export BOOGIE_EXE="${DOTNET_ROOT}/tools/boogie"
+          /home/runner/.cargo/bin/cargo run -p sui -- move prove