Add CI job to verify TLAPS proofs of *_proofs.tla modules

Adds a new `tlaps` job to both the push (main.yml) and pull
request (pr.yml) GitHub Actions workflows. The job downloads the
TLAPS 1.6.0-pre release from tlaplus/tlapm and runs `tlapm` on
every modules/*_proofs.tla file, ensuring the proofs of the
theorems in FoldsTheorems, FunctionTheorems, FiniteSetsExtTheorems
and SequencesExtTheorems remain valid as the modules evolve.

The job runs as a matrix on ubuntu-latest (x86_64-linux-gnu) and
macos-latest (arm64-darwin), the two platforms for which the
1.6.0-pre release ships a tlapm binary.  All proof files are
checked even if one fails so a single regression does not mask
others.

[CI]

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Author: lemmy

.github/workflows/main.yml

@@ -98,3 +98,38 @@ jobs:
         repository: tlaplus/tlaplus
         event-type: tlaplus-dispatch
         client-payload: '{"source": "CommunityModules"}'
+
+  tlaps:
+    name: Verify TLAPS proofs
+    runs-on: ${{ matrix.os }}
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+          - os: ubuntu-latest
+            asset: tlapm-1.6.0-pre-x86_64-linux-gnu.tar.gz
+          - os: macos-latest
+            asset: tlapm-1.6.0-pre-arm64-darwin.tar.gz
+    defaults:
+      run:
+        shell: bash
+    steps:
+    - uses: actions/checkout@v2
+    - name: Download TLAPS 1.6.0-pre
+      run: |
+        curl -fsSL -o tlapm.tar.gz \
+          "https://github.com/tlaplus/tlapm/releases/download/1.6.0-pre/${{ matrix.asset }}"
+        tar -xzf tlapm.tar.gz
+        echo "$PWD/tlapm/bin" >> "$GITHUB_PATH"
+    - name: Show tlapm version
+      run: tlapm --version
+    - name: Verify _proofs.tla modules
+      working-directory: modules
+      run: |
+        status=0
+        for proof in *_proofs.tla; do
+          echo "::group::Verifying $proof"
+          tlapm --cleanfp "$proof" || status=1
+          echo "::endgroup::"
+        done
+        exit $status

.github/workflows/pr.yml

@@ -22,3 +22,38 @@ jobs:
       run: echo "date=$(date +'%Y%m%d%H%M')" >> "$GITHUB_OUTPUT"
     - name: Build with Ant
       run: ant -noinput -buildfile build.xml -Dtimestamp=${{steps.date.outputs.date}}
+
+  tlaps:
+    name: Verify TLAPS proofs
+    runs-on: ${{ matrix.os }}
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+          - os: ubuntu-latest
+            asset: tlapm-1.6.0-pre-x86_64-linux-gnu.tar.gz
+          - os: macos-latest
+            asset: tlapm-1.6.0-pre-arm64-darwin.tar.gz
+    defaults:
+      run:
+        shell: bash
+    steps:
+    - uses: actions/checkout@v2
+    - name: Download TLAPS 1.6.0-pre
+      run: |
+        curl -fsSL -o tlapm.tar.gz \
+          "https://github.com/tlaplus/tlapm/releases/download/1.6.0-pre/${{ matrix.asset }}"
+        tar -xzf tlapm.tar.gz
+        echo "$PWD/tlapm/bin" >> "$GITHUB_PATH"
+    - name: Show tlapm version
+      run: tlapm --version
+    - name: Verify _proofs.tla modules
+      working-directory: modules
+      run: |
+        status=0
+        for proof in *_proofs.tla; do
+          echo "::group::Verifying $proof"
+          tlapm --cleanfp "$proof" || status=1
+          echo "::endgroup::"
+        done
+        exit $status