Various updates to CI scripts #318
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: Check Specs & Metadata | |
| on: | |
| push: | |
| branches: | |
| - master | |
| pull_request: | |
| branches: | |
| - master | |
| repository_dispatch: | |
| types: [tlaplus-dispatch] | |
| jobs: | |
| validate: | |
| name: Validate Manifest, Specs, & Models | |
| runs-on: ${{ matrix.os }} | |
| strategy: | |
| matrix: | |
| include: | |
| - { os: windows-latest } | |
| - { os: ubuntu-latest } | |
| - { os: macos-latest } | |
| fail-fast: false | |
| env: | |
| SCRIPT_DIR: .github/scripts | |
| DEPS_DIR: deps | |
| defaults: | |
| run: | |
| shell: bash | |
| steps: | |
| - name: Clone repo | |
| uses: actions/checkout@v4 | |
| - name: Install python | |
| uses: actions/setup-python@v5 | |
| with: | |
| python-version: '3.12' | |
| - name: Install Java | |
| uses: actions/setup-java@v4 | |
| with: | |
| distribution: adopt | |
| java-version: 17 | |
| - name: Download TLA⁺ dependencies (Windows) | |
| if: matrix.os == 'windows-latest' | |
| run: $SCRIPT_DIR/windows-setup.sh $SCRIPT_DIR $DEPS_DIR | |
| - name: Download TLA⁺ dependencies (Linux & macOS) | |
| if: matrix.os != 'windows-latest' | |
| run: $SCRIPT_DIR/linux-setup.sh $SCRIPT_DIR $DEPS_DIR | |
| - name: Check manifest.json format | |
| run: | | |
| source bin/activate | |
| python $SCRIPT_DIR/check_manifest_schema.py \ | |
| --manifest_path manifest.json \ | |
| --schema_path manifest-schema.json | |
| - name: Check manifest files | |
| run: | | |
| source bin/activate | |
| python $SCRIPT_DIR/check_manifest_files.py \ | |
| --manifest_path manifest.json \ | |
| --ci_ignore_path .ciignore | |
| - name: Check manifest feature flags | |
| run: | | |
| source bin/activate | |
| python $SCRIPT_DIR/check_manifest_features.py \ | |
| --manifest_path manifest.json \ | |
| --ts_path $DEPS_DIR/tree-sitter-tlaplus | |
| - name: Check README spec table | |
| run: | | |
| source bin/activate | |
| python $SCRIPT_DIR/check_markdown_table.py \ | |
| --manifest_path manifest.json \ | |
| --readme_path README.md | |
| - name: Parse all modules | |
| run: | | |
| source bin/activate | |
| python $SCRIPT_DIR/parse_modules.py \ | |
| --tools_jar_path $DEPS_DIR/tools/tla2tools.jar \ | |
| --tlapm_lib_path $DEPS_DIR/tlapm/library \ | |
| --community_modules_jar_path $DEPS_DIR/community/modules.jar \ | |
| --manifest_path manifest.json | |
| - name: Check small models | |
| run: | | |
| source bin/activate | |
| python $SCRIPT_DIR/check_small_models.py \ | |
| --tools_jar_path $DEPS_DIR/tools/tla2tools.jar \ | |
| --tlapm_lib_path $DEPS_DIR/tlapm/library \ | |
| --community_modules_jar_path $DEPS_DIR/community/modules.jar \ | |
| --manifest_path manifest.json | |
| - name: Smoke-test large models | |
| run: | | |
| source bin/activate | |
| # SimKnuthYao requires certain number of states to have been generated | |
| # before termination or else it fails. This makes it not amenable to | |
| # smoke testing. | |
| SKIP=("specifications/KnuthYao/SimKnuthYao.cfg") | |
| # SimTokenRing does not work on Windows systems. | |
| if [[ "${{ runner.os }}" == "Windows" ]]; then | |
| SKIP+=("specifications/ewd426/SimTokenRing.cfg") | |
| fi | |
| python $SCRIPT_DIR/smoke_test_large_models.py \ | |
| --tools_jar_path $DEPS_DIR/tools/tla2tools.jar \ | |
| --tlapm_lib_path $DEPS_DIR/tlapm/library \ | |
| --community_modules_jar_path $DEPS_DIR/community/modules.jar \ | |
| --manifest_path manifest.json \ | |
| --skip "${SKIP[@]}" | |
| - name: Check proofs | |
| if: matrix.os != 'windows-latest' | |
| run: | | |
| source bin/activate | |
| SKIP=( | |
| # Failing; see https://github.com/tlaplus/Examples/issues/67 | |
| specifications/Bakery-Boulangerie/Bakery.tla | |
| specifications/Bakery-Boulangerie/Boulanger.tla | |
| specifications/Paxos/Consensus.tla | |
| specifications/PaxosHowToWinATuringAward/Consensus.tla | |
| specifications/lamport_mutex/LamportMutex_proofs.tla | |
| specifications/ewd998/EWD998_proof.tla | |
| specifications/byzpaxos/VoteProof.tla | |
| # Long-running; see https://github.com/tlaplus/tlapm/issues/85 | |
| specifications/LoopInvariance/Quicksort.tla | |
| specifications/LoopInvariance/SumSequence.tla | |
| specifications/bcastByz/bcastByz.tla | |
| specifications/MisraReachability/ReachabilityProofs.tla | |
| specifications/byzpaxos/BPConProof.tla # Takes about 30 minutes | |
| ) | |
| python $SCRIPT_DIR/check_proofs.py \ | |
| --tlapm_path $DEPS_DIR/tlapm-install \ | |
| --manifest_path manifest.json \ | |
| --skip "${SKIP[@]}" | |
| - name: Smoke-test manifest generation script | |
| run: | | |
| source bin/activate | |
| rm -r $DEPS_DIR/tree-sitter-tlaplus/build | |
| python $SCRIPT_DIR/generate_manifest.py \ | |
| --manifest_path manifest.json \ | |
| --ci_ignore_path .ciignore \ | |
| --ts_path $DEPS_DIR/tree-sitter-tlaplus | |
| git diff -a | |