Parallelize unit tests #195
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] | |
| jobs: | |
| tlatools-build-and-test: | |
| name: TLA+ Tools Build & Test | |
| runs-on: ubuntu-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.0.3 | |
| - name: Build & Test Tools | |
| run: | | |
| ant -f tlatools/org.lamport.tlatools/customBuild.xml \ | |
| compile compile-test test dist \ | |
| 2>&1 | tee test-output.txt | |
| echo "export BUILD_UT_EXIT_CODE=$?" >> $GITHUB_ENV | |
| - name: Summarize Unit Tests | |
| run: | | |
| python .github/scripts/parse-unit-test-output.py \ | |
| test-output.txt \ | |
| tlatools/org.lamport.tlatools/target/surefire-reports | |
| exit $BUILD_UT_EXIT_CODE | |
| - 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.os }} | |
| strategy: | |
| matrix: | |
| include: | |
| - os: ubuntu-latest | |
| MVN_COMMAND: xvfb-run mvn -Dtest.skip=true -Dmaven.test.failure.ignore=true | |
| - os: 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.0.3 | |
| - 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 | |
| env: | |
| EXAMPLES_DIR: examples | |
| SCRIPT_DIR: examples/.github/scripts | |
| DEPS_DIR: examples/deps | |
| 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.0.3 | |
| - 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: Parse tlaplus/examples modules | |
| run: | | |
| python "$SCRIPT_DIR/parse_modules.py" \ | |
| --tools_jar_path tlatools/org.lamport.tlatools/dist/tla2tools.jar \ | |
| --tlapm_lib_path "$DEPS_DIR/tlapm/library" \ | |
| --community_modules_jar_path "$DEPS_DIR/community/modules.jar" \ | |
| --manifest_path "$EXAMPLES_DIR/manifest.json" | |
| - name: Model-check small tlaplus/examples models | |
| run: | | |
| python "$SCRIPT_DIR/check_small_models.py" \ | |
| --tools_jar_path tlatools/org.lamport.tlatools/dist/tla2tools.jar \ | |
| --tlapm_lib_path "$DEPS_DIR/tlapm/library" \ | |
| --community_modules_jar_path "$DEPS_DIR/community/modules.jar" \ | |
| --manifest_path "$EXAMPLES_DIR/manifest.json" | |
| - 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 tlatools/org.lamport.tlatools/dist/tla2tools.jar \ | |
| --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" | |