diff --git a/.github/workflows/inox-CI.yml b/.github/workflows/inox-CI.yml new file mode 100644 index 000000000..66b8edd82 --- /dev/null +++ b/.github/workflows/inox-CI.yml @@ -0,0 +1,40 @@ +name: Inox CI +on: + pull_request: + push: + branches: + - main +jobs: + tests: + if: github.event.pull_request.draft == false + runs-on: [self-hosted, linux] + env: + # define Java options for both official sbt and sbt-extras + JAVA_OPTS: -J-Xss64M -J-Xms1024M -J-Xmx8G + JVM_OPTS: -J-Xss64M -J-Xms1024M -J-Xmx8G + steps: + - name: Checkout + uses: actions/checkout@v4 + with: + submodules: recursive + - name: Setup JDK + uses: actions/setup-java@v3 + with: + distribution: temurin + java-version: 17 + - name: Install solvers + run: ./install_solvers.sh $GITHUB_WORKSPACE/.local/bin + - name: Add solvers to PATH + run: echo "$GITHUB_WORKSPACE/.local/bin" >> $GITHUB_PATH + - name: Test solvers availability + run: cvc5 --version && z3 --version && cvc4 --version + - name: Run Tests + run: sbt -Dtest-parallelism=10 -batch test + - name: Run integration tests + run: sbt -Dtest-parallelism=10 -batch it:test + fail_if_pull_request_is_draft: + if: github.event.pull_request.draft == true + runs-on: [self-hosted, linux] + steps: + - name: Fails in order to indicate that pull request needs to be marked as ready to review and tests workflows need to pass. + run: exit 1 diff --git a/install_solvers.sh b/install_solvers.sh new file mode 100755 index 000000000..62c13ea42 --- /dev/null +++ b/install_solvers.sh @@ -0,0 +1,28 @@ +TEMP_DIR="temp" +SOLVERS_DIR="$1" + +mkdir -p "$SOLVERS_DIR" +mkdir -p "$TEMP_DIR" +# cvc5 +wget https://github.com/cvc5/cvc5/releases/download/cvc5-1.1.2/cvc5-Linux-static.zip -O "$TEMP_DIR/downloaded.zip" -q +unzip "$TEMP_DIR/downloaded.zip" -d "$TEMP_DIR" +CVC5_DIR=$(ls "$TEMP_DIR" | grep cvc5) +mv "$TEMP_DIR/$CVC5_DIR/bin/cvc5" "$SOLVERS_DIR/cvc5" +chmod +x "$SOLVERS_DIR/cvc5" +rm -rf "$TEMP_DIR" + +# CVC4 +wget https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.8-x86_64-linux-opt -O "$SOLVERS_DIR/cvc4" -q +chmod +x "$SOLVERS_DIR/cvc4" + +# z3 +mkdir -p "$TEMP_DIR" +wget https://github.com/Z3Prover/z3/releases/download/z3-4.13.0/z3-4.13.0-x64-glibc-2.35.zip -O "$TEMP_DIR/downloaded.zip" -q +unzip "$TEMP_DIR/downloaded.zip" -d "$TEMP_DIR" +Z3_DIR=$(ls "$TEMP_DIR" | grep z3) +mv "$TEMP_DIR/$Z3_DIR/bin/z3" "$SOLVERS_DIR/z3" +chmod +x "$SOLVERS_DIR/z3" +rm -rf "$TEMP_DIR" + +echo "************** Solvers Installed **************" +exit 0 \ No newline at end of file