Add scripts for CI (#1574)

* new scripts to run tests and bolts locally * add a message in scripts * echo a message when CI successfull * add timing information to CI script * final message in the CI script * new ci scripts + github actions start * recursive suvbmodules in github actions * new java options same as in jvmopts * add run tests steps * add bolts tests * new script + new ci with 2 jobs * missing checkout * add install solvers options * test solvers * wrong version of cvc54 * new cvc5 * cvc5 * run on selfhosted * cvc5 1.1.2 to work on laraquad * test soilvers are available * ,2 * new path for solvers * remove skip tests * 2 workflows: nightly, and CI for PR and pushes to main * move sbt plugin to CI
epfl-lara · Sep 4, 2024 · 1e816e6 · 1e816e6
1 parent 865b164
commit 1e816e6
Show file tree

Hide file tree

Showing 6 changed files with 276 additions and 6 deletions.
diff --git a/.github/workflows/stainless-CI.yml b/.github/workflows/stainless-CI.yml
@@ -0,0 +1,44 @@
+name: Stainless CI
+on:
+  pull_request:
+    types: [opened, synchronize, reopened, ready_for_review]
+  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: -Dsbt.io.implicit.relative.glob.conversion=allow -Xss512M -Xms1024M -Xmx12G -XX:MaxMetaspaceSize=2G -XX:+UseCodeCacheFlushing -XX:ReservedCodeCacheSize=768M
+      JVM_OPTS:  -Dsbt.io.implicit.relative.glob.conversion=allow -Xss512M -Xms1024M -Xmx12G -XX:MaxMetaspaceSize=2G -XX:+UseCodeCacheFlushing -XX:ReservedCodeCacheSize=768M
+    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: ./stainless-ci.sh --install-solvers $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: Build and Package
+      run: ./stainless-ci.sh --build-only
+    - name: Run Tests and Integration Tests
+      run: ./stainless-ci.sh --skip-build --skip-bolts --skip-sbt-plugin 
+    - name: Sbt Plugin Tests
+      run: ./stainless-ci.sh --skip-build --skip-tests --skip-bolts
+  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/.github/workflows/stainless-nightly.yml b/.github/workflows/stainless-nightly.yml
@@ -0,0 +1,31 @@
+name: Stainless CI
+on:
+  schedule:
+    - cron: '0 1 * * *'
+jobs:
+  bolts:
+    runs-on: [self-hosted, linux]
+    env:
+      # define Java options for both official sbt and sbt-extras
+      JAVA_OPTS: -Dsbt.io.implicit.relative.glob.conversion=allow -Xss512M -Xms1024M -Xmx12G -XX:MaxMetaspaceSize=2G -XX:+UseCodeCacheFlushing -XX:ReservedCodeCacheSize=768M
+      JVM_OPTS:  -Dsbt.io.implicit.relative.glob.conversion=allow -Xss512M -Xms1024M -Xmx12G -XX:MaxMetaspaceSize=2G -XX:+UseCodeCacheFlushing -XX:ReservedCodeCacheSize=768M
+    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: ./stainless-ci.sh --install-solvers $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: Build and Package
+      run: ./stainless-ci.sh --build-only
+    - name: Bolts Tests
+      run: ./stainless-ci.sh --skip-build --skip-tests --skip-sbt-plugin
diff --git a/bin/bolts-tests.sh b/bin/bolts-tests.sh
@@ -2,14 +2,17 @@
 
 set -e
 
+# TEST_DIR should exist
 TEST_DIR=$1
 echo "Moving to $TEST_DIR"
-mkdir -p "$TEST_DIR"
+# mkdir -p "$TEST_DIR"
 cd "$TEST_DIR" || exit 1
 
 if [[ -d "bolts" ]]; then
+  echo "Found bolts directory in $TEST_DIR!"
   cd bolts
-  git pull || exit 1
+  # We do not pull so that we can run the 
+  # git pull || exit 1 
 else
   git clone https://github.com/epfl-lara/bolts
   cd bolts || exit 1

diff --git a/bin/external-tests.sh b/bin/external-tests.sh
@@ -84,6 +84,7 @@ Usage: external-tests.sh [options]
 
   -h | -help         Print this message
   --skip-build       Do not build Stainless (saves time if the build is already up-to-date).
+  --bolts-dir        Directory where bolts is located (default: clones from GitHub)
 EOM
 }
 
@@ -100,6 +101,11 @@ while [[ $# -gt 0 ]]; do
       SKIP_BUILD=true
       shift # past argument
       ;;
+    --bolts-dir)
+      BOLTS_DIR="$2"
+      shift # past argument
+      shift # past value
+      ;;
     *)    # unknown option
       usage
       exit 1
@@ -139,10 +145,18 @@ fi
 export PATH="$BASE_DIR/frontends/scalac/target/universal/stage/bin:$PATH"
 export PATH="$BASE_DIR/frontends/dotty/target/universal/stage/bin:$PATH"
 
-# Create a directory for doing tests and move there
+# If the bolts directory is provided, TEST_DIR is set to its parent directory
+if [[ -n "$BOLTS_DIR" ]]; then
+  TEST_DIR=$(dirname "$BOLTS_DIR")
+else
+  # Create a directory for doing tests and move there
+  TEST_DIR="$BASE_DIR/.stainless-external-tests"
+  mkdir -p "$TEST_DIR"
+fi
+
+echo "TEST_DIR = $TEST_DIR"
+
 
-TEST_DIR="$BASE_DIR/.stainless-external-tests"
-mkdir -p "$TEST_DIR"
 
 # Stainless Actors are currently disabled: https://github.com/epfl-lara/stainless/issues/970
 # "$BIN_DIR/stainless-actors-tests.sh" "$TEST_DIR" "$STAINLESS_VERSION"

diff --git a/inox b/inox
diff --git a/stainless-ci.sh b/stainless-ci.sh
@@ -0,0 +1,178 @@
+#!/usr/bin/env bash
+
+# Run the complete CI pipeline
+
+# Record the time to compute the total duration
+TIME_BEFORE=$(date +%s)
+
+BUILD_ONLY=false
+SKIP_BOLTS=false
+SKIP_BUILD=false
+SKIP_SBT_PLUGIN=false
+SKIP_TESTS=false
+
+# First parse the options
+while [[ $# -gt 0 ]]; do
+  key="$1"
+
+  case $key in
+    -h|--help)
+      usage
+      exit 0
+      ;;
+    --bolts-dir)
+      BOLTS_DIR="$2"
+      shift # past argument
+      shift # past value
+      ;;
+    --build-only)
+      BUILD_ONLY=true
+      shift # past argument
+      ;;
+    --skip-bolts)
+      SKIP_BOLTS=true
+      shift # past argument
+      ;;
+    --skip-build)
+      SKIP_BUILD=true
+      shift # past argument
+      ;;
+    --skip-sbt-plugin)
+      SKIP_SBT_PLUGIN=true
+      shift # past argument
+      ;;
+    --skip-tests)
+      SKIP_TESTS=true
+      shift # past argument
+      ;;
+    --install-solvers)
+      SOLVERS_DIR="$2"
+      shift # past argument
+      shift # past value
+      ;;
+    *)    # unknown option
+      usage
+      exit 1
+      ;;
+  esac
+done
+
+usage() {
+ cat <<EOM
+Usage: external-tests.sh [options]
+
+  -h | -help               Print this message
+  --bolts-dir       <DIR>  Directory where bolts is located (default: clones from GitHub).
+  --build-only             Only build the project, do not run tests.
+  --skip-build             Do not build the project (saves time if the build is already up-to-date).
+  --skip-bolts             Do not run the Bolts benchmarks.
+  --skip-sbt-plugin        Do not run the sbt plugin tests.
+  --skip-tests             Do not run the unit and integration tests.
+  --install-solvers <DIR>  Install the solvers required for the tests (cvc5, CVC4, and z3) FOR LINUX.
+
+EOM
+}
+
+# Download the solvers
+if [ -n "$SOLVERS_DIR" ]; then
+  TEMP_DIR="temp"
+  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"
+  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"
+  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"
+  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
+fi
+
+if [ "$SKIP_BUILD" = true ]; then
+  echo "************** Skipping build **************"
+else
+  sbt universal:stage
+  if [ $? -ne 0 ]; then
+    echo "************** Failed to build the universal package **************"
+    exit 1
+  fi
+  if [ "$BUILD_ONLY" = true ]; then
+    echo "************** Build only done **************"
+    exit 0
+  fi
+fi
+
+if [ "$SKIP_TESTS" = true ]; then
+  echo "************** Skipping tests **************"
+else
+  # Run the tests
+  sbt -batch -Dtestsuite-parallelism=5 test
+  if [ $? -ne 0 ]; then
+    echo "************** Unit tests failed **************"
+    exit 1
+  fi
+
+  # Run the integration tests
+  sbt -batch -Dtestsuite-parallelism=3 -Dtestcase-parallelism=5 it:test
+  if [ $? -ne 0 ]; then
+    echo "************** Integration tests failed **************"
+    exit 1
+  fi
+
+fi
+
+# Run the Bolts benchmarks
+# if BOLTS_DIR is set, pass it to the script
+if [ "$SKIP_BOLTS" = true ]; then
+  echo "************** Skipping Bolts tests **************"
+else
+  if [ -z "$BOLTS_DIR" ]; then
+    bash bin/external-tests.sh --skip-build 
+  else
+    bash bin/external-tests.sh --skip-build --bolts-dir $BOLTS_DIR
+  fi
+  if [ $? -ne 0 ]; then
+    echo "Bolts benchmarks failed"
+    exit 1
+  fi
+fi
+
+# Run sbt scripted 
+if [ "$SKIP_SBT_PLUGIN" = true ]; then
+  echo "************** Skipping sbt plugin tests **************"
+else
+  sbt -batch scripted
+  if [ $? -ne 0 ]; then
+    echo "sbt scripted failed"
+    exit 1
+  fi
+fi
+
+# bash bin/build-slc-lib.sh
+# if [ $? -ne 0 ]; then
+#   echo "build-slc-lib.sh failed"
+#   exit 1
+# fi
+
+TIME_AFTER=$(date +%s)
+DURATION=$((TIME_AFTER - TIME_BEFORE))
+
+echo ""
+echo "********************************* CI PASSED! *********************************"
+
+echo "Total time: $DURATION seconds"