Debugger: Add support for breakpoint expressions #737
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: TLA+ PR Validation | |
| on: [pull_request] | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| tlatools-build-and-test: | |
| name: TLA+ Tools Build & Test | |
| runs-on: ${{ matrix.operating-system }} | |
| strategy: | |
| matrix: | |
| operating-system: [ubuntu-latest, macos-latest] | |
| steps: | |
| - name: Clone tlaplus/tlaplus | |
| uses: actions/checkout@v4 | |
| with: | |
| # Number of commits to fetch. 0 indicates all history. | |
| # jgit task nested in customBuild.xml fails without history. | |
| fetch-depth: 0 | |
| - name: Set up JDK 11 | |
| uses: actions/setup-java@v4 | |
| with: | |
| distribution: adopt | |
| java-version: 11 | |
| - name: Check tla+.jj grammar/code sync | |
| run: | | |
| ant -f tlatools/org.lamport.tlatools/customBuild.xml generate | |
| git status | |
| diff_count=$(git status --porcelain=v1 2>/dev/null | wc -l) | |
| exit $diff_count | |
| ## | |
| ## The following process first compiles and packages (dist) the tla2tools.jar file. Next, it | |
| ## runs the test suite in parallel, aborting the run and failing the workflow upon the first | |
| ## test failure (test.halt=true). Regardless of any test failures, a JUnitReport is generated. | |
| ## Both the report and the test results (in XML format) are uploaded as workflow artifacts for | |
| ## potential local download and further analysis. Additionally, mikepenz/action-junit-report | |
| ## publishes the stack traces from the test results. If desired, the test.halt setting can be | |
| ## removed to allow the test suite to run to completion. | |
| ## (The same sequence of steps is executed by main.yml) | |
| ## | |
| - name: Build tools and unit tests | |
| run: ant -f tlatools/org.lamport.tlatools/customBuild.xml info compile compile-test dist | |
| - name: Run unit tests | |
| run: ant -f tlatools/org.lamport.tlatools/customBuild.xml info test -Dtest.halt=true | |
| - name: Generate JUnitReport | |
| if: always() | |
| run: ant -f tlatools/org.lamport.tlatools/customBuild.xml test-report | |
| - name: Upload raw unit test results | |
| uses: actions/upload-artifact@v4 | |
| if: always() | |
| with: | |
| ## Name of the artifact to upload (discriminated by os to prevent name conflicts). | |
| name: testresults-${{ matrix.operating-system }} | |
| path: | | |
| tlatools/org.lamport.tlatools/target/surefire-reports/TEST-*.xml | |
| tlatools/org.lamport.tlatools/target/surefire-reports/TESTS-TestSuites.xml | |
| tlatools/org.lamport.tlatools/target/surefire-reports/junit-noframes.html | |
| - name: Publish unit test results | |
| uses: mikepenz/action-junit-report@v4 | |
| if: always() | |
| with: | |
| check_name: JUnit Test Report on ${{ matrix.operating-system }} | |
| report_paths: 'tlatools/org.lamport.tlatools/target/surefire-reports/TEST-*.xml' | |
| - name: Clone tlaplus/CommunityModules | |
| uses: actions/checkout@v4 | |
| with: | |
| repository: tlaplus/CommunityModules | |
| path: communitymodules/ | |
| # Number of commits to fetch. 0 indicates all history. | |
| # jgit task nested in customBuild.xml fails without history. | |
| fetch-depth: 0 | |
| - name: Build Community Modules as Integration Test | |
| run: | | |
| mkdir -p communitymodules/tlc | |
| cp tlatools/org.lamport.tlatools/dist/tla2tools.jar communitymodules/tlc/ | |
| ant -f communitymodules/build.xml -Dskip.download=true | |
| toolbox-build-and-test: | |
| name: Eclipse Toolbox Build & Test | |
| runs-on: ${{ matrix.operating-system }} | |
| strategy: | |
| matrix: | |
| include: | |
| - operating-system: ubuntu-latest | |
| MVN_COMMAND: xvfb-run mvn -Dtest.skip=true -Dmaven.test.failure.ignore=true | |
| - operating-system: macos-latest | |
| MVN_COMMAND: mvn -Dmaven.test.skip=true | |
| fail-fast: false | |
| steps: | |
| - name: Clone tlaplus/tlaplus | |
| uses: actions/checkout@v4 | |
| with: | |
| # Number of commits to fetch. 0 indicates all history. | |
| # jgit task nested in customBuild.xml fails without history. | |
| fetch-depth: 0 | |
| - name: Set up JDK 11 | |
| uses: actions/setup-java@v4 | |
| with: | |
| distribution: adopt | |
| java-version: 11 | |
| - name: Build & Test Eclipse Toolbox with Maven | |
| run: | | |
| ${{ matrix.MVN_COMMAND }} \ | |
| -Dtycho.disableP2Mirrors=true \ | |
| -Dorg.slf4j.simpleLogger.log.org.apache.maven.cli.transfer.Slf4jMavenTransferListener=warn \ | |
| -fae -B verify --file pom.xml | |
| examples-tests: | |
| name: Examples Integration Tests | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| include: | |
| - unicode: true | |
| - unicode: false | |
| env: | |
| EXAMPLES_DIR: "examples" | |
| SCRIPT_DIR: "examples/.github/scripts" | |
| DEPS_DIR: "examples/deps" | |
| DIST_DIR: "tlatools/org.lamport.tlatools/dist" | |
| steps: | |
| - name: Clone tlaplus/tlaplus | |
| uses: actions/checkout@v4 | |
| with: | |
| # Number of commits to fetch. 0 indicates all history. | |
| # jgit task nested in customBuild.xml fails without history. | |
| fetch-depth: 0 | |
| - name: Clone tlaplus/examples | |
| uses: actions/checkout@v4 | |
| with: | |
| repository: tlaplus/examples | |
| path: ${{ env.EXAMPLES_DIR }} | |
| - name: Set up JDK 11 | |
| uses: actions/setup-java@v4 | |
| with: | |
| distribution: adopt | |
| java-version: 11 | |
| - name: Build tla2tools.jar | |
| run: ant -f tlatools/org.lamport.tlatools/customBuild.xml compile compile-test dist | |
| - name: Download dependencies | |
| run: | | |
| "$SCRIPT_DIR/linux-setup.sh" "$SCRIPT_DIR" "$DEPS_DIR" false | |
| - name: Convert specs to unicode | |
| if: matrix.unicode | |
| run: | | |
| python "$SCRIPT_DIR/unicode_conversion.py" \ | |
| --tlauc_path "$DEPS_DIR/tlauc/tlauc" \ | |
| --manifest_path "$EXAMPLES_DIR/manifest.json" | |
| - name: Add unicode shims | |
| if: matrix.unicode | |
| run: | | |
| python "$SCRIPT_DIR/unicode_number_set_shim.py" \ | |
| --manifest_path "$EXAMPLES_DIR/manifest.json" | |
| - name: Translate PlusCal | |
| run: | | |
| python $SCRIPT_DIR/translate_pluscal.py \ | |
| --tools_jar_path "$DIST_DIR/tla2tools.jar" \ | |
| --manifest_path "$EXAMPLES_DIR/manifest.json" | |
| - name: Parse tlaplus/examples modules | |
| run: | | |
| # Need to have a nonempty list to pass as a skip parameter | |
| SKIP=("does/not/exist") | |
| if [ ${{ matrix.unicode }} ]; then | |
| # These redefine Nat, Int, or Real so cannot be shimmed | |
| SKIP+=( | |
| "specifications/SpecifyingSystems/Standard/Naturals.tla" | |
| "specifications/SpecifyingSystems/Standard/Peano.tla" | |
| "specifications/SpecifyingSystems/Standard/Integers.tla" | |
| "specifications/SpecifyingSystems/Standard/Reals.tla" | |
| "specifications/SpecifyingSystems/Standard/ProtoReals.tla" | |
| "specifications/SpecifyingSystems/RealTime/MCRealTime.tla" | |
| "specifications/SpecifyingSystems/RealTime/MCRealTimeHourClock.tla" | |
| ) | |
| fi | |
| python "$SCRIPT_DIR/parse_modules.py" \ | |
| --tools_jar_path "$DIST_DIR/tla2tools.jar" \ | |
| --apalache_path "$DEPS_DIR/apalache" \ | |
| --tlapm_lib_path "$DEPS_DIR/tlapm/library" \ | |
| --community_modules_jar_path "$DEPS_DIR/community/modules.jar" \ | |
| --manifest_path "$EXAMPLES_DIR/manifest.json" \ | |
| --skip "${SKIP[@]}" | |
| - name: Model-check small tlaplus/examples models | |
| run: | | |
| # https://github.com/tlaplus/Examples/issues/134 | |
| SKIP=("specifications/ewd998/EWD998ChanTrace.cfg") | |
| if [ ${{ matrix.unicode }} ]; then | |
| # This redefines Real so cannot be shimmed | |
| SKIP+=("specifications/SpecifyingSystems/RealTime/MCRealTimeHourClock.cfg") | |
| # Apalache does not yet support Unicode | |
| SKIP+=("specifications/EinsteinRiddle/Einstein.cfg") | |
| fi | |
| python "$SCRIPT_DIR/check_small_models.py" \ | |
| --tools_jar_path "$DIST_DIR/tla2tools.jar" \ | |
| --apalache_path "$DEPS_DIR/apalache" \ | |
| --tlapm_lib_path "$DEPS_DIR/tlapm/library" \ | |
| --community_modules_jar_path "$DEPS_DIR/community/modules.jar" \ | |
| --manifest_path "$EXAMPLES_DIR/manifest.json" \ | |
| --skip "${SKIP[@]}" | |
| - name: Smoke-test large tlaplus/examples models | |
| run: | | |
| # SimKnuthYao requires certain number of states to have been generated | |
| # before termination or else it fails. This makes it not amenable to | |
| # smoke testing. | |
| python "$SCRIPT_DIR/smoke_test_large_models.py" \ | |
| --tools_jar_path "$DIST_DIR/tla2tools.jar" \ | |
| --apalache_path "$DEPS_DIR/apalache" \ | |
| --tlapm_lib_path "$DEPS_DIR/tlapm/library" \ | |
| --community_modules_jar_path "$DEPS_DIR/community/modules.jar" \ | |
| --manifest_path "$EXAMPLES_DIR/manifest.json" \ | |
| --skip "specifications/KnuthYao/SimKnuthYao.cfg" | |