From 02c1d40bc321f15386de88b1abd962cafce205b7 Mon Sep 17 00:00:00 2001
From: Junkil Park <jkpark@fb.com>
Date: Thu, 28 Jul 2022 10:17:44 -0700
Subject: [PATCH] Update action.yaml (#2217)

- install the Prover dependencies such as Z3 and Boogie

- enable the Prover test for the move-example pacakge
---
 .github/actions/rust-setup/action.yaml           | 16 ++++++++++++++++
 .../move-examples/tests/move_prover_tests.rs     |  1 -
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/.github/actions/rust-setup/action.yaml b/.github/actions/rust-setup/action.yaml
index 22d0af3b3ef5b..d27ba08c7d053 100644
--- a/.github/actions/rust-setup/action.yaml
+++ b/.github/actions/rust-setup/action.yaml
@@ -10,3 +10,19 @@ runs:
     - uses: bmwill/rust-cache@v1
       with:
         path: ~/.cargo/registry/src/**/librocksdb-sys-*
+    - name: install Prover dependencies
+      shell: bash
+      run: scripts/dev_setup.sh -b -p -y
+    - name: prepare move lang prover tooling.
+      shell: bash
+      run: |
+        # By setting these values the dev-setup.sh script can detect already installed executables (and check versions).
+        echo 'Z3_EXE='/home/runner/bin/z3 | tee -a $GITHUB_ENV
+        echo 'CVC5_EXE='/home/runner/bin/cvc5 | tee -a $GITHUB_ENV
+        echo 'DOTNET_ROOT='/home/runner/.dotnet/ | tee -a $GITHUB_ENV
+        echo 'BOOGIE_EXE='/home/runner/.dotnet/tools/boogie | tee -a $GITHUB_ENV
+        echo 'MVP_TEST_ON_CI'='1' | tee -a $GITHUB_ENV
+        echo "/home/runner/bin" | tee -a $GITHUB_PATH
+        echo "/home/runner/.dotnet" | tee -a $GITHUB_PATH
+        echo "/home/runner/.dotnet/tools" | tee -a $GITHUB_PATH
+        echo "/home/runner/.cargo/bin" | tee -a $GITHUB_PATH
diff --git a/aptos-move/move-examples/tests/move_prover_tests.rs b/aptos-move/move-examples/tests/move_prover_tests.rs
index b6678bac1d78e..a2218b19673dc 100644
--- a/aptos-move/move-examples/tests/move_prover_tests.rs
+++ b/aptos-move/move-examples/tests/move_prover_tests.rs
@@ -37,7 +37,6 @@ pub fn run_prover_for_pkg(
     .unwrap();
 }
 
-#[ignore] // TODO: Ignored because Prover dependencies are not installed in CI.
 #[test]
 fn test_hello_prover() {
     let named_address = BTreeMap::new();