Moved CI setup out into scripts

Signed-off-by: Andrew Helwer <[email protected]>
tlaplus · Feb 6, 2024 · 12a57ff · 12a57ff
1 parent 789a653
commit 12a57ff
Show file tree

Hide file tree

Showing 4 changed files with 159 additions and 101 deletions.
diff --git a/.github/scripts/linux-setup.sh b/.github/scripts/linux-setup.sh
@@ -0,0 +1,75 @@
+# This script downloads all necessary dependencies to run the CI on Linux.
+# It can also be run locally, as long as you have the following dependencies:
+#  - python 3.1x
+#  - java
+#  - C & C++ compiler (aliased to cc and cpp commands respectively)
+#  - wget
+#  - tar
+#
+# The script takes the following positional command line parameters:
+#  1. Path to this script directory from the current working directory
+#  2. Path to the desired dependencies directory
+
+main() {
+  # Validate command line parameters
+  if [ $# -ne 2 ]; then
+    echo "Usage: $0 <script dir path> <desired dependency dir path>"
+    exit 1
+  fi
+  SCRIPT_DIR="$1"
+  DEPS_DIR="$2"
+  # Print out tool version information
+  java --version
+  python --version
+  pip --version
+  cc --version
+  cpp --version
+  # Install python packages in virtual environment
+  python -m venv .
+  source bin/activate
+  pip install -r "$SCRIPT_DIR/requirements.txt"
+  deactivate
+  # Put all dependencies in their own directory to ensure they aren't included implicitly
+  mkdir -p "$DEPS_DIR"
+  # Get tree-sitter-tlaplus
+  wget -nv https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/main.tar.gz -O /tmp/tree-sitter-tlaplus.tar.gz
+  tar -xzf /tmp/tree-sitter-tlaplus.tar.gz --directory "$DEPS_DIR"
+  mv "$DEPS_DIR/tree-sitter-tlaplus-main" "$DEPS_DIR/tree-sitter-tlaplus"
+  # Get TLA⁺ tools
+  mkdir -p "$DEPS_DIR/tools"
+  wget -nv http://nightly.tlapl.us/dist/tla2tools.jar -P "$DEPS_DIR/tools"
+  # Get TLA⁺ community modules
+  mkdir -p "$DEPS_DIR/community"
+  wget -nv https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar \
+        -O "$DEPS_DIR/community/modules.jar"
+  # Get TLAPS modules
+  wget -nv https://github.com/tlaplus/tlapm/archive/main.tar.gz -O /tmp/tlapm.tar.gz
+  tar -xzf /tmp/tlapm.tar.gz --directory "$DEPS_DIR"
+  mv "$DEPS_DIR/tlapm-main" "$DEPS_DIR/tlapm"
+  # Install TLAPS
+  kernel=$(uname -s)
+  if [ "$kernel" == "Linux" ]; then
+    TLAPM_BIN_TYPE=x86_64-linux-gnu
+  elif [ "$kernel" == "macOS" ]; then
+    TLAPM_BIN_TYPE=i386-darwin
+  else
+    echo "Unknown OS"
+    exit 1
+  fi
+  TLAPM_BIN="tlaps-1.5.0-$TLAPM_BIN_TYPE-inst.bin"
+  wget -nv "https://github.com/tlaplus/tlapm/releases/latest/download/$TLAPM_BIN" -O /tmp/tlapm-installer.bin
+  chmod +x /tmp/tlapm-installer.bin
+  # Workaround for https://github.com/tlaplus/tlapm/issues/88
+  set +e
+  for ((attempt = 1; attempt <= 5; attempt++)); do
+    rm -rf "$DEPS_DIR/tlapm-install"
+    /tmp/tlapm-installer.bin -d "$DEPS_DIR/tlapm-install"
+    if [ $? -eq 0 ]; then
+      exit 0
+    fi
+  done
+  exit 1
+}
+
+main "$@"
+
diff --git a/.github/scripts/windows-setup.sh b/.github/scripts/windows-setup.sh
@@ -0,0 +1,50 @@
+# This script downloads all necessary dependencies to run the CI on Windows.
+# It can also be run locally, as long as you have the following dependencies:
+#  - python 3.1x
+#  - java
+#  - curl
+#  - 7-zip
+#
+# The script takes the following positional command line parameters:
+#  1. Path to this script directory from the current working directory
+#  2. Path to the desired dependencies directory
+
+main() {
+  # Validate command line parameters
+  if [ $# -ne 2 ]; then
+    echo "Usage: $0 <script dir path> <desired dependency dir path>"
+    exit 1
+  fi
+  SCRIPT_DIR="$1"
+  DEPS_DIR="$2"
+  # Print out tool version information
+  java --version
+  python --version
+  pip --version
+  # Install python packages
+  python -m venv .
+  source bin/activate
+  pip install -r "$SCRIPT_DIR/requirements.txt"
+  deactivate
+  # Put all dependencies in their own directory to ensure they aren't included implicitly
+  mkdir -p "$DEPS_DIR"
+  # Get tree-sitter-tlaplus
+  curl -L https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/main.zip --output tree-sitter-tlaplus.zip
+  7z x tree-sitter-tlaplus.zip
+  mv tree-sitter-tlaplus-main "$DEPS_DIR/tree-sitter-tlaplus"
+  rm tree-sitter-tlaplus.zip
+  # Get TLA⁺ tools
+  mkdir -p "$DEPS_DIR/tools"
+  curl http://nightly.tlapl.us/dist/tla2tools.jar --output "$DEPS_DIR/tools/tla2tools.jar"
+  # Get TLA⁺ community modules
+  mkdir -p "$DEPS_DIR/community"
+  curl https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar --output "$DEPS_DIR/community/modules.jar"
+  # Get TLAPS modules
+  curl -L https://github.com/tlaplus/tlapm/archive/main.zip --output tlapm.zip
+  7z x tlapm.zip
+  mv tlapm-main "$DEPS_DIR/tlapm"
+  rm tlapm.zip
+}
+
+main "$@"
+
diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
@@ -22,7 +22,7 @@ jobs:
       fail-fast: false
     env:
       SCRIPT_DIR: .github/scripts
-      TLAPS_VERSION: 202210041448
+      DEPS_DIR: deps
     defaults:
       run:
         shell: bash
@@ -32,129 +32,61 @@ jobs:
       - name: Install python
         uses: actions/setup-python@v5
         with:
-          python-version: '3.11'
+          python-version: '3.12'
       - name: Install Java
         uses: actions/setup-java@v4
         with:
           distribution: adopt
           java-version: 17
-      - name: Download TLA⁺ dependencies
+      - name: Download TLA⁺ dependencies (Windows)
         if: matrix.os == 'windows-latest'
-        run: |
-          # Print out tool version information
-          java --version
-          python --version
-          pip --version
-          # Install python packages
-          pip install -r $SCRIPT_DIR/requirements.txt
-          # Put all dependencies in their own directory to ensure they aren't included implicitly
-          mkdir deps
-          # Get tree-sitter-tlaplus
-          curl -LO https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/main.zip
-          7z x main.zip
-          rm main.zip
-          mv tree-sitter-tlaplus-main deps/tree-sitter-tlaplus
-          # Get TLA⁺ tools
-          mkdir deps/tools
-          curl -LO http://nightly.tlapl.us/dist/tla2tools.jar
-          mv tla2tools.jar deps/tools/tla2tools.jar
-          # Get TLA⁺ community modules
-          mkdir deps/community
-          curl -LO https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar
-          mv CommunityModules-deps.jar deps/community/modules.jar
-          # Get TLAPS modules
-          curl -LO https://github.com/tlaplus/tlapm/archive/refs/tags/$TLAPS_VERSION.zip
-          7z x $TLAPS_VERSION.zip
-          rm $TLAPS_VERSION.zip
-          mv tlapm-$TLAPS_VERSION deps/tlapm
-      - name: Download TLA⁺ dependencies
+        run: $SCRIPT_DIR/windows-setup.sh $SCRIPT_DIR $DEPS_DIR
+      - name: Download TLA⁺ dependencies (Linux & macOS)
         if: matrix.os != 'windows-latest'
-        run: |
-          # Print out tool version information
-          java --version
-          python --version
-          pip --version
-          cc --version
-          cpp --version
-          # Install python packages
-          pip install -r $SCRIPT_DIR/requirements.txt
-          # Put all dependencies in their own directory to ensure they aren't included implicitly
-          mkdir deps
-          # Get tree-sitter-tlaplus
-          wget -nv https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/main.tar.gz
-          tar -xf main.tar.gz
-          rm main.tar.gz
-          mv tree-sitter-tlaplus-main deps/tree-sitter-tlaplus
-          # Get TLA⁺ tools
-          mkdir deps/tools
-          wget -nv http://nightly.tlapl.us/dist/tla2tools.jar -O deps/tools/tla2tools.jar
-          # Get TLA⁺ community modules
-          mkdir deps/community
-          wget -nv https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar \
-                -O deps/community/modules.jar
-          # Get TLAPS modules
-          wget -nv https://github.com/tlaplus/tlapm/archive/refs/tags/$TLAPS_VERSION.tar.gz
-          tar -xf $TLAPS_VERSION.tar.gz
-          rm $TLAPS_VERSION.tar.gz
-          mv tlapm-$TLAPS_VERSION deps/tlapm
-          # Install TLAPS
-          if [[ "${{ runner.os }}" == "Linux" ]]; then
-            TLAPM_BIN_TYPE=x86_64-linux-gnu
-          elif [[ "${{ runner.os }}" == "macOS" ]]; then
-            TLAPM_BIN_TYPE=i386-darwin
-          else
-            echo "Unknown OS"
-            exit 1
-          fi
-          TLAPM_BIN="tlaps-1.5.0-$TLAPM_BIN_TYPE-inst.bin"
-          wget -nv https://github.com/tlaplus/tlapm/releases/download/$TLAPS_VERSION/$TLAPM_BIN
-          chmod +x $TLAPM_BIN
-          # Workaround for https://github.com/tlaplus/tlapm/issues/88
-          set +e
-          for ((attempt = 1; attempt <= 5; attempt++)); do
-            rm -rf deps/tlapm-install
-            ./$TLAPM_BIN -d deps/tlapm-install
-            if [ $? -eq 0 ]; then
-              exit 0
-            fi
-          done
-          exit 1
+        run: $SCRIPT_DIR/linux-setup.sh $SCRIPT_DIR $DEPS_DIR
       - name: Check manifest.json format
         run: |
+          source bin/activate
           python $SCRIPT_DIR/check_manifest_schema.py \
             --manifest_path manifest.json             \
             --schema_path manifest-schema.json
       - name: Check manifest files
         run: |
+          source bin/activate
           python $SCRIPT_DIR/check_manifest_files.py  \
             --manifest_path manifest.json             \
             --ci_ignore_path .ciignore
       - name: Check manifest feature flags
         run: |
+          source bin/activate
           python $SCRIPT_DIR/check_manifest_features.py \
             --manifest_path manifest.json               \
-            --ts_path deps/tree-sitter-tlaplus
+            --ts_path $DEPS_DIR/tree-sitter-tlaplus
       - name: Check README spec table
         run: |
+          source bin/activate
           python $SCRIPT_DIR/check_markdown_table.py  \
             --manifest_path manifest.json             \
             --readme_path README.md
       - name: Parse all modules
         run: |
-          python $SCRIPT_DIR/parse_modules.py                       \
-            --tools_jar_path deps/tools/tla2tools.jar               \
-            --tlapm_lib_path deps/tlapm/library                     \
-            --community_modules_jar_path deps/community/modules.jar \
+          source bin/activate
+          python $SCRIPT_DIR/parse_modules.py                            \
+            --tools_jar_path $DEPS_DIR/tools/tla2tools.jar               \
+            --tlapm_lib_path $DEPS_DIR/tlapm/library                     \
+            --community_modules_jar_path $DEPS_DIR/community/modules.jar \
             --manifest_path manifest.json
       - name: Check small models
         run: |
-          python $SCRIPT_DIR/check_small_models.py                  \
-            --tools_jar_path deps/tools/tla2tools.jar               \
-            --tlapm_lib_path deps/tlapm/library                     \
-            --community_modules_jar_path deps/community/modules.jar \
+          source bin/activate
+          python $SCRIPT_DIR/check_small_models.py                       \
+            --tools_jar_path $DEPS_DIR/tools/tla2tools.jar               \
+            --tlapm_lib_path $DEPS_DIR/tlapm/library                     \
+            --community_modules_jar_path $DEPS_DIR/community/modules.jar \
             --manifest_path manifest.json
       - name: Smoke-test large models
         run: |
+          source bin/activate
           # SimKnuthYao requires certain number of states to have been generated
           # before termination or else it fails. This makes it not amenable to
           # smoke testing.
@@ -163,15 +95,16 @@ jobs:
           if [[ "${{ runner.os }}" == "Windows" ]]; then
             SKIP+=("specifications/ewd426/SimTokenRing.cfg")
           fi
-          python $SCRIPT_DIR/smoke_test_large_models.py             \
-            --tools_jar_path deps/tools/tla2tools.jar               \
-            --tlapm_lib_path deps/tlapm/library                     \
-            --community_modules_jar_path deps/community/modules.jar \
-            --manifest_path manifest.json                           \
+          python $SCRIPT_DIR/smoke_test_large_models.py                  \
+            --tools_jar_path $DEPS_DIR/tools/tla2tools.jar               \
+            --tlapm_lib_path $DEPS_DIR/tlapm/library                     \
+            --community_modules_jar_path $DEPS_DIR/community/modules.jar \
+            --manifest_path manifest.json                                \
             --skip "${SKIP[@]}"
       - name: Check proofs
         if: matrix.os != 'windows-latest'
         run: |
+          source bin/activate
           SKIP=(
             # Failing; see https://github.com/tlaplus/Examples/issues/67
             specifications/Bakery-Boulangerie/Bakery.tla
@@ -188,16 +121,17 @@ jobs:
             specifications/MisraReachability/ReachabilityProofs.tla
             specifications/byzpaxos/BPConProof.tla # Takes about 30 minutes
           )
-          python $SCRIPT_DIR/check_proofs.py  \
-            --tlapm_path deps/tlapm-install   \
-            --manifest_path manifest.json     \
+          python $SCRIPT_DIR/check_proofs.py       \
+            --tlapm_path $DEPS_DIR/tlapm-install   \
+            --manifest_path manifest.json          \
             --skip "${SKIP[@]}"
       - name: Smoke-test manifest generation script
         run: |
-          rm -r deps/tree-sitter-tlaplus/build
+          source bin/activate
+          rm -r $DEPS_DIR/tree-sitter-tlaplus/build
           python $SCRIPT_DIR/generate_manifest.py \
             --manifest_path manifest.json         \
             --ci_ignore_path .ciignore            \
-            --ts_path deps/tree-sitter-tlaplus
+            --ts_path $DEPS_DIR/tree-sitter-tlaplus
           git diff -a
 
diff --git a/README.md b/README.md
@@ -16,7 +16,6 @@ All specs in this repository are subject to CI validation to ensure quality.
 
 ## Examples Included Here
 Here is a list of specs included in this repository, with links to the relevant directory and flags for various features:
-<<<<<<< HEAD
 | Name                                                                                                | Author(s)                                           | Beginner | TLAPS Proof | PlusCal | TLC Model | Apalache |
 | --------------------------------------------------------------------------------------------------- | --------------------------------------------------- | :------: | :---------: | :-----: | :-------: | :------: |
 | [Teaching Concurrency](specifications/TeachingConcurrency)                                          | Leslie Lamport                                      |    ✔     |      ✔      |    ✔    |     ✔     |          |