CI.yml

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