CI: use JDK 25 for Apalache and JDK 17 for TLC

.github/scripts/parse_modules.py

@@ -50,7 +50,7 @@ def parse_module(path):
     ] + (['-enableassertions'] if enable_assertions else [])
     sany_parameters = ['-error-codes', path]
     sany = subprocess.run(
-        ['java'] + jvm_parameters + ['tla2sany.SANY'] + sany_parameters,
+        [tla_utils.get_java_command('TLC')] + jvm_parameters + ['tla2sany.SANY'] + sany_parameters,
         stdout=subprocess.PIPE,
         stderr=subprocess.STDOUT,
         text=True
@@ -83,4 +83,3 @@ def parse_module(path):
 with ThreadPoolExecutor(thread_count) as executor:
     results = executor.map(parse_module, modules)
     exit(0 if all(results) else 1)
-

.github/scripts/tla_utils.py

@@ -2,6 +2,7 @@
 from datetime import datetime
 from datetime import timedelta
 import json
+import os
 from os.path import join, normpath, pathsep, dirname
 from pathlib import PureWindowsPath
 import subprocess
@@ -147,6 +148,34 @@ def get_tlc_feature_flags(module_features):
         jvm_parameters.append('-Dtlc2.tool.impl.Tool.cdot=true')
     return jvm_parameters
 
+def get_java_command(tool):
+    """
+    Gets the Java executable configured for a specific tool.
+    """
+    java_executable = os.environ.get(f'{tool}_JAVA')
+    if java_executable:
+        return java_executable
+    java_home = os.environ.get(f'{tool}_JAVA_HOME')
+    if java_home:
+        executable = 'java.exe' if sys.platform == 'win32' else 'java'
+        return normpath(join(java_home, 'bin', executable))
+    return 'java'
+
+def get_java_environment(tool):
+    """
+    Gets an environment that makes a specific tool's Java the default.
+    """
+    env = os.environ.copy()
+    java_home = os.environ.get(f'{tool}_JAVA_HOME')
+    if java_home:
+        env['JAVA_HOME'] = java_home
+        env['PATH'] = pathsep.join([normpath(join(java_home, 'bin')), env.get('PATH', '')])
+    java_executable = os.environ.get(f'{tool}_JAVA')
+    if java_executable:
+        env['JAVA'] = java_executable
+        env['JAVACMD'] = java_executable
+    return env
+
 def check_model(
         tools_jar_path,
         apalache_path,
@@ -193,7 +222,8 @@ def check_model(
                 timeout=hard_timeout_in_seconds,
                 stdout=subprocess.PIPE,
                 stderr=subprocess.STDOUT,
-                text=True
+                text=True,
+                env=get_java_environment('APALACHE')
             )
             return apalache
         else:
@@ -217,7 +247,7 @@ def check_model(
                 '-cleanup'
             ] + get_run_mode(mode)
             tlc = subprocess.run(
-                ['java'] + jvm_parameters + ['tlc2.TLC'] + tlc_parameters,
+                [get_java_command('TLC')] + jvm_parameters + ['tlc2.TLC'] + tlc_parameters,
                 timeout=hard_timeout_in_seconds,
                 stdout=subprocess.PIPE,
                 stderr=subprocess.STDOUT,
@@ -286,4 +316,3 @@ def extract_state_count_info(tlc_output):
     total_states = locale.atoi(state_count_findings.group('total_states'))
     state_depth = locale.atoi(state_depth_findings.group('state_depth'))
     return (distinct_states, total_states, state_depth)
-

.github/scripts/translate_pluscal.py

@@ -48,7 +48,7 @@ def translate_module(module_path):
     jvm_parameters = ['-cp', tools_path] + (['-enableassertions'] if enable_assertions else [])
     pcal_parameters = ['-nocfg', module_path]
     pcal = subprocess.run(
-        ['java'] + jvm_parameters + ['pcal.trans'] + pcal_parameters,
+        [tla_utils.get_java_command('TLC')] + jvm_parameters + ['pcal.trans'] + pcal_parameters,
         stdout=subprocess.PIPE,
         stderr=subprocess.STDOUT,
         text=True
@@ -67,4 +67,3 @@ def translate_module(module_path):
 with ThreadPoolExecutor(thread_count) as executor:
     results = executor.map(translate_module, modules)
     exit(0 if all(results) else 1)
-

.github/workflows/CI.yml

@@ -33,11 +33,20 @@ jobs:
         uses: actions/setup-python@v5
         with:
           python-version: '3.12'
-      - name: Install Java
+      - name: Install Java 25 for Apalache
         uses: actions/setup-java@v4
         with:
-          distribution: adopt
+          distribution: temurin
+          java-version: 25
+      - name: Capture Apalache Java
+        run: echo "APALACHE_JAVA_HOME=$JAVA_HOME" >> "$GITHUB_ENV"
+      - name: Install Java 17 for TLC
+        uses: actions/setup-java@v4
+        with:
+          distribution: temurin
           java-version: 17
+      - name: Capture TLC Java
+        run: echo "TLC_JAVA_HOME=$JAVA_HOME" >> "$GITHUB_ENV"
       - name: Install timeout command
         if: matrix.os == 'macos-latest'
         run: brew install coreutils
@@ -202,4 +211,3 @@ jobs:
             --community_modules_jar_path $DEPS_DIR/community/modules.jar  \
             --examples_root .
           git diff -a
-

.github/workflows/ewd998.yml

@@ -14,6 +14,11 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - uses: actions/checkout@v1
+    - name: Install Java 17 for TLC
+      uses: actions/setup-java@v4
+      with:
+        distribution: temurin
+        java-version: 17
     - name: Get (nightly) TLC
       run: wget https://nightly.tlapl.us/dist/tla2tools.jar
     - name: Get (nightly) CommunityModules
@@ -35,4 +40,3 @@ jobs:
       with:
         name: trace.ndjson
         path: specifications/ewd998/trace.ndjson
-

.github/workflows/manual.yml

@@ -7,6 +7,11 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - uses: actions/checkout@v1
+    - name: Install Java 17 for TLC
+      uses: actions/setup-java@v4
+      with:
+        distribution: temurin
+        java-version: 17
     - name: Get (nightly) TLC
       run: wget https://nightly.tlapl.us/dist/tla2tools.jar
     - name: Get (nightly) CommunityModules
@@ -20,4 +25,4 @@ jobs:
         wget https://raw.githubusercontent.com/tlaplus/tlapm/main/library/NaturalsInduction.tla
         wget https://raw.githubusercontent.com/tlaplus/tlapm/main/library/SequenceTheorems.tla
     - name: Run
-      run: /bin/bash .github/workflows/run.sh
+      run: /bin/bash .github/workflows/run.sh

.github/workflows/run.sh

@@ -2,7 +2,8 @@
 
 set -ex
 
-TLC_COMMAND="java -ea -XX:+UseParallelGC -Dtlc2.TLC.stopAfter=180 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa70d124d0c77ffff -cp tla2tools.jar tlc2.TLC -workers auto -lncheck final -tool -deadlock"
+TLC_JAVA="${TLC_JAVA:-${TLC_JAVA_HOME:+$TLC_JAVA_HOME/bin/java}}"
+TLC_COMMAND="${TLC_JAVA:-java} -ea -XX:+UseParallelGC -Dtlc2.TLC.stopAfter=180 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa70d124d0c77ffff -cp tla2tools.jar tlc2.TLC -workers auto -lncheck final -tool -deadlock"
 
 echo Check specifications/aba-asyn-byz/aba_asyn_byz
 $TLC_COMMAND specifications/aba-asyn-byz/aba_asyn_byz