From f83a14a6c666aeadc4964f91804a4582b8953a3b Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 5 Aug 2026 10:28:08 -0700 Subject: [PATCH] CI: use JDK 25 for Apalache and JDK 17 for TLC Apalache now requires JDK 25 as of https://github.com/apalache-mc/apalache/pull/3432. Install both JDKs in the main CI workflow, preserve JDK 25 for Apalache via APALACHE_JAVA_HOME, and keep JDK 17 for TLC, SANY, PlusCal, and the TLC-only workflows. Co-authored-by: GPT-5 Signed-off-by: Markus Alexander Kuppe --- .github/scripts/parse_modules.py | 3 +-- .github/scripts/tla_utils.py | 35 +++++++++++++++++++++++++--- .github/scripts/translate_pluscal.py | 3 +-- .github/workflows/CI.yml | 14 ++++++++--- .github/workflows/ewd998.yml | 6 ++++- .github/workflows/manual.yml | 7 +++++- .github/workflows/run.sh | 3 ++- 7 files changed, 58 insertions(+), 13 deletions(-) diff --git a/.github/scripts/parse_modules.py b/.github/scripts/parse_modules.py index 68ea5bf8..d5b0641f 100644 --- a/.github/scripts/parse_modules.py +++ b/.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) - diff --git a/.github/scripts/tla_utils.py b/.github/scripts/tla_utils.py index 1c755211..e152fcb6 100644 --- a/.github/scripts/tla_utils.py +++ b/.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) - diff --git a/.github/scripts/translate_pluscal.py b/.github/scripts/translate_pluscal.py index 71582922..2a98f10f 100644 --- a/.github/scripts/translate_pluscal.py +++ b/.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) - diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 3126e95b..2156131c 100644 --- a/.github/workflows/CI.yml +++ b/.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 - diff --git a/.github/workflows/ewd998.yml b/.github/workflows/ewd998.yml index b47fc6f1..f9e3e737 100644 --- a/.github/workflows/ewd998.yml +++ b/.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 - diff --git a/.github/workflows/manual.yml b/.github/workflows/manual.yml index 7f57319a..67e72c83 100644 --- a/.github/workflows/manual.yml +++ b/.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 \ No newline at end of file + run: /bin/bash .github/workflows/run.sh diff --git a/.github/workflows/run.sh b/.github/workflows/run.sh index 64557520..c224f5cb 100755 --- a/.github/workflows/run.sh +++ b/.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