Make pcal.trans unicode-safe #211
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: 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 | |
| - name: Build tools and unit tests | |
| run: ant -f tlatools/org.lamport.tlatools/customBuild.xml compile compile-test dist | |
| - name: Run unit tests | |
| run: | | |
| set +e # Ensure UT failure does not immediately terminate CI | |
| set -o pipefail # Ensure UT failure is propagated through tee command | |
| ant -f tlatools/org.lamport.tlatools/customBuild.xml test 2>&1 | tee test-output.txt | |
| ut_exit_code=$? | |
| echo "Unit test exit code: $ut_exit_code" | |
| echo "UT_EXIT_CODE=$ut_exit_code" >> $GITHUB_ENV # Export UT result to CI env var | |
| - name: Summarize unit tests | |
| run: | | |
| echo "Unit test exit code: $UT_EXIT_CODE" | |
| python .github/scripts/parse-unit-test-output.py \ | |
| test-output.txt \ | |
| tlatools/org.lamport.tlatools/target/surefire-reports | |
| exit $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 | |
| 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.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: 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" \ | |
| --ts_path "$DEPS_DIR/tree-sitter-tlaplus" \ | |
| --manifest_path "$EXAMPLES_DIR/manifest.json" | |
| - name: Translate PlusCal | |
| if: (!matrix.unicode) | |
| 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" \ | |
| --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") | |
| fi | |
| python "$SCRIPT_DIR/check_small_models.py" \ | |
| --tools_jar_path "$DIST_DIR/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 "${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" \ | |
| --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" | |