Various updates to CI scripts

.github/scripts/linux-setup.sh

@@ -0,0 +1,81 @@
+# 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
+#  3. Boolean true/false; whether to initialize a python virtual env
+
+main() {
+  # Validate command line parameters
+  if [ $# -ne 3 ]; then
+    echo "Usage: $0 <script dir path> <desired dependency dir path> <bool: use python venv>"
+    exit 1
+  fi
+  SCRIPT_DIR="$1"
+  DEPS_DIR="$2"
+  USE_VENV=$3
+  # Print out tool version information
+  java --version
+  python --version
+  pip --version
+  cc --version
+  cpp --version
+  # Install python packages
+  if $USE_VENV; then
+    python -m venv .
+    source bin/activate
+    pip install -r "$SCRIPT_DIR/requirements.txt"
+    deactivate
+  else
+    pip install -r "$SCRIPT_DIR/requirements.txt"
+  fi
+  # 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" == "Darwin" ]; then
+    TLAPM_BIN_TYPE=i386-darwin
+  else
+    echo "Unknown OS: $kernel"
+    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 "$@"
+

.github/scripts/parse_modules.py

@@ -16,35 +16,41 @@
 parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=True)
 parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True)
 parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip parsing', required=False, default=[])
+parser.add_argument('--only', nargs='+', help='If provided, only parse models in this space-separated list', required=False, default=[])
+parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
 args = parser.parse_args()
 
-logging.basicConfig(level=logging.INFO)
+logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)
 
 tools_jar_path = normpath(args.tools_jar_path)
 tlaps_modules = normpath(args.tlapm_lib_path)
 community_modules = normpath(args.community_modules_jar_path)
 manifest_path = normpath(args.manifest_path)
 examples_root = dirname(manifest_path)
 skip_modules = [normpath(path) for path in args.skip]
+only_modules = [normpath(path) for path in args.only]
 
 def parse_module(path):
     """
     Parse the given module using SANY.
     """
     logging.info(path)
     # Jar paths must go first
-    search_paths = pathsep.join([tools_jar_path, community_modules, dirname(path), tlaps_modules])
+    search_paths = pathsep.join([tools_jar_path, dirname(path), community_modules, tlaps_modules])
     sany = subprocess.run([
         'java',
         '-cp', search_paths,
         'tla2sany.SANY',
         '-error-codes',
         path
     ], capture_output=True)
-    if sany.returncode != 0:
-        logging.error(sany.stdout.decode('utf-8'))
+    output = ' '.join(sany.args) + '\n' + sany.stdout.decode('utf-8')
+    if 0 == sany.returncode:
+        logging.debug(output)
+        return True
+    else:
+        logging.error(output)
         return False
-    return True
 
 manifest = tla_utils.load_json(manifest_path)
 
@@ -54,13 +60,14 @@ def parse_module(path):
     for spec in manifest['specifications']
     for module in spec['modules']
         if normpath(module['path']) not in skip_modules
+        and (only_modules == [] or normpath(module['path']) in only_modules)
 ]
 
 for path in skip_modules:
     logging.info(f'Skipping {path}')
 
 # Parse specs in parallel
-thread_count = cpu_count()
+thread_count = cpu_count() if not args.verbose else 1
 logging.info(f'Parsing using {thread_count} threads')
 with ThreadPoolExecutor(thread_count) as executor:
     results = executor.map(parse_module, modules)

.github/scripts/windows-setup.sh

@@ -0,0 +1,56 @@
+# 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
+#  3. Boolean true/false; whether to initialize a python virtual env
+
+main() {
+  # Validate command line parameters
+  if [ $# -ne 3 ]; then
+    echo "Usage: $0 <script dir path> <desired dependency dir path> <bool: use python venv>"
+    exit 1
+  fi
+  SCRIPT_DIR="$1"
+  DEPS_DIR="$2"
+  USE_VENV=$3
+  # Print out tool version information
+  java --version
+  python --version
+  pip --version
+  # Install python packages
+  if $USE_VENV; then
+    python -m venv .
+    pwsh Scripts/Activate.ps1
+    pip install -r "$SCRIPT_DIR/requirements.txt"
+    deactivate
+  else
+    pip install -r "$SCRIPT_DIR/requirements.txt"
+  fi
+  # 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 -L 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 "$@"
+

.github/workflows/CI.yml

@@ -18,11 +18,11 @@ jobs:
         include:
         - { os: windows-latest }
         - { os: ubuntu-latest }
-        - { os: macos-latest }
+        - { os: macos-14 }
       fail-fast: false
     env:
       SCRIPT_DIR: .github/scripts
-      TLAPS_VERSION: 202210041448
+      DEPS_DIR: deps
     defaults:
       run:
         shell: bash
@@ -32,93 +32,18 @@ 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 false
+      - 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 false
       - name: Check manifest.json format
         run: |
           python $SCRIPT_DIR/check_manifest_schema.py \
@@ -133,25 +58,25 @@ jobs:
         run: |
           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: |
           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 \
+          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 \
+          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: |
@@ -163,11 +88,11 @@ 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'
@@ -188,16 +113,16 @@ 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
+          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
 

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                                      |    ✔     |      ✔      |    ✔    |     ✔     |          |