From d4c2299605d82b358acc39e57374c62a5b7df02d Mon Sep 17 00:00:00 2001
From: Samuel Chassot <14821693+samuelchassot@users.noreply.github.com>
Date: Mon, 16 Dec 2024 10:38:40 +0100
Subject: [PATCH] New CI with extracted common setup workflow, with a new CI
 with verification (#120)

---
 .github/workflows/bolts-CI-verification.yml | 25 ++++++++++
 .github/workflows/bolts-CI.yml              | 44 +++++------------
 .github/workflows/setup/action.yml          | 53 +++++++++++++++++++++
 3 files changed, 91 insertions(+), 31 deletions(-)
 create mode 100644 .github/workflows/bolts-CI-verification.yml
 create mode 100644 .github/workflows/setup/action.yml

diff --git a/.github/workflows/bolts-CI-verification.yml b/.github/workflows/bolts-CI-verification.yml
new file mode 100644
index 00000000..0898eae1
--- /dev/null
+++ b/.github/workflows/bolts-CI-verification.yml
@@ -0,0 +1,25 @@
+name: Bolts CI Verification
+on:
+  workflow_dispatch:
+  push:
+    branches:
+      - main
+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 
+  JAVA_OPTS_TMP_DIR: /tmp/tmp_${{ github.run_id }}_${{ github.run_attempt }}
+jobs:
+  bolts-verification:
+    runs-on: [self-hosted, linux]
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v4
+    - name: Setup
+      uses: ./.github/workflows/setup
+      with:
+        java-opts: ${{ env.JAVA_OPTS }}
+        java-version: 17
+        temp-dir: "/tmp/tmp_${{ github.run_id }}_${{ github.run_attempt }}"
+    - name: Bolts Tests with verification
+      run: ./run-tests.sh
\ No newline at end of file
diff --git a/.github/workflows/bolts-CI.yml b/.github/workflows/bolts-CI.yml
index e3ba58b4..2431477e 100644
--- a/.github/workflows/bolts-CI.yml
+++ b/.github/workflows/bolts-CI.yml
@@ -1,46 +1,28 @@
-name: Bolts CI
+name: Bolts CI with admit VCs
 on:
   pull_request:
   push:
     branches:
       - main
+
+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 
+  JAVA_OPTS_TMP_DIR: /tmp/tmp_${{ github.run_id }}_${{ github.run_attempt }}
 jobs:
-  tests:
-    if: github.event.pull_request.draft == false
+  bolts-admit-vcs:
     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 
-      JAVA_OPTS_TMP_DIR: /tmp/tmp_${{ github.run_id }}_${{ github.run_attempt }}
     steps:
     - name: Checkout
       uses: actions/checkout@v4
+    - name: Setup
+      uses: ./.github/workflows/setup
       with:
-        submodules: recursive
-    - name: Setup JDK
-      uses: actions/setup-java@v4
-      with:
-        distribution: temurin
+        java-opts: ${{ env.JAVA_OPTS }}
         java-version: 17
-    - name: Setup java options
-      run: |
-          echo "JAVA_OPTS=$JAVA_OPTS -Djava.io.tmpdir=$JAVA_OPTS_TMP_DIR" >> "$GITHUB_ENV" && \
-          echo "JVM_OPTS=$JVM_OPTS -Djava.io.tmpdir=$JAVA_OPTS_TMP_DIR" >> "$GITHUB_ENV" && \
-          echo "SBT_OPTS=-Djava.io.tmpdir=$JAVA_OPTS_TMP_DIR --sbt-dir $JAVA_OPTS_TMP_DIR" >> "$GITHUB_ENV"
-    - name: Creating temp folder
-      run: rm -rf $JAVA_OPTS_TMP_DIR && mkdir -p $JAVA_OPTS_TMP_DIR && chmod 777 $JAVA_OPTS_TMP_DIR
-    - name: Install stainless and solvers
-      run: ./install_stainless_and_solvers.sh $GITHUB_WORKSPACE/.local/bin $GITHUB_WORKSPACE/.local && echo "PATH=$GITHUB_WORKSPACE/.local/bin:$PATH" >> "$GITHUB_ENV"
-    - name: Add stainless to PATH
-      run: echo "$GITHUB_WORKSPACE/.local/stainless/frontends/dotty/target/universal/stage/bin" >> $GITHUB_PATH && echo "PATH=$GITHUB_WORKSPACE/.local/stainless/frontends/dotty/target/universal/stage/bin:$PATH" >> "$GITHUB_ENV"
-    - name: Test stainless availability
-      run: stainless-dotty --version
-    - 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: Bolts Tests
+        temp-dir: "/tmp/tmp_${{ github.run_id }}_${{ github.run_attempt }}"
+    - name: Bolts admit VCs tests
       run: ./run-tests.sh --admit-vcs
   fail_if_pull_request_is_draft:
     if: github.event.pull_request.draft == true
diff --git a/.github/workflows/setup/action.yml b/.github/workflows/setup/action.yml
new file mode 100644
index 00000000..2724232a
--- /dev/null
+++ b/.github/workflows/setup/action.yml
@@ -0,0 +1,53 @@
+name: Bolts Setup
+description: Setup for Bolts CI
+inputs: 
+  java-opts:
+    description: 'Java options for both official sbt and sbt-extras'
+    required: true
+    default: '-Dsbt.io.implicit.relative.glob.conversion=allow -Xss512M -Xms1024M -Xmx12G -XX:MaxMetaspaceSize=2G -XX:+UseCodeCacheFlushing -XX:ReservedCodeCacheSize=768M'
+  temp-dir:
+    description: 'Temporary directory for Java options'
+    required: true
+    default: '/tmp/tmp_${{ github.run_id }}_${{ github.run_attempt }}'
+  java-version:
+    description: 'Java version to use'
+    required: true
+    default: '17'
+runs:
+  using: 'composite'
+  steps:
+  - name: Checkout
+    uses: actions/checkout@v4
+    with:
+      submodules: recursive
+  - name: Setup JDK
+    uses: actions/setup-java@v4
+    with:
+      distribution: temurin
+      java-version: ${{ inputs.java-version }}
+  - name: Setup java options environment variables
+    run: |
+        echo "JAVA_OPTS=${{ inputs.java-opts }}" >> "$GITHUB_ENV" && \
+        echo "JVM_OPTS=${{ inputs.java-opts }}" >> "$GITHUB_ENV" && \
+        echo "JAVA_OPTS=$JAVA_OPTS -Djava.io.tmpdir=$JAVA_OPTS_TMP_DIR" >> "$GITHUB_ENV" && \
+        echo "JVM_OPTS=$JVM_OPTS -Djava.io.tmpdir=${{ inputs.temp-dir }}" >> "$GITHUB_ENV" && \
+        echo "SBT_OPTS=-Djava.io.tmpdir=${{ inputs.temp-dir }} --sbt-dir ${{ inputs.temp-dir }}" >> "$GITHUB_ENV"
+    shell: bash
+  - name: Creating temp folder
+    run: rm -rf ${{ inputs.temp-dir }} && mkdir -p ${{ inputs.temp-dir }} && chmod 777 ${{ inputs.temp-dir }}
+    shell: bash
+  - name: Install stainless and solvers
+    run: ./install_stainless_and_solvers.sh $GITHUB_WORKSPACE/.local/bin $GITHUB_WORKSPACE/.local && echo "PATH=$GITHUB_WORKSPACE/.local/bin:$PATH" >> "$GITHUB_ENV"
+    shell: bash
+  - name: Add stainless to PATH
+    run: echo "$GITHUB_WORKSPACE/.local/stainless/frontends/dotty/target/universal/stage/bin" >> $GITHUB_PATH && echo "PATH=$GITHUB_WORKSPACE/.local/stainless/frontends/dotty/target/universal/stage/bin:$PATH" >> "$GITHUB_ENV"
+    shell: bash
+  - name: Test stainless availability
+    run: stainless-dotty --version
+    shell: bash
+  - name: Add solvers to PATH
+    run: echo "$GITHUB_WORKSPACE/.local/bin" >> $GITHUB_PATH
+    shell: bash
+  - name: Test solvers availability
+    run: cvc5 --version && z3 --version && cvc4 --version
+    shell: bash
\ No newline at end of file