Added CI step to check proofs

.github/scripts/check_proofs.py

@@ -0,0 +1,69 @@
+"""
+Validate all proofs in all modules with TLAPM.
+"""
+
+from argparse import ArgumentParser
+from os.path import dirname, join, normpath
+import subprocess
+from timeit import default_timer as timer
+import tla_utils
+
+parser = ArgumentParser(description='Validate all proofs in all modules with TLAPM.')
+parser.add_argument('--tlapm_path', help='Path to TLAPM install dir; should have bin and lib subdirs', required=True)
+parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True)
+args = parser.parse_args()
+
+tlapm_path = normpath(args.tlapm_path)
+manifest_path = normpath(args.manifest_path)
+manifest = tla_utils.load_json(manifest_path)
+examples_root = dirname(manifest_path)
+
+# Tracked in https://github.com/tlaplus/Examples/issues/67
+failing_proofs = [
+    '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'
+]
+
+# Fingerprint issues; tracked in https://github.com/tlaplus/tlapm/issues/85
+long_running_proofs = [
+    'specifications/LoopInvariance/Quicksort.tla',
+    'specifications/LoopInvariance/SumSequence.tla',
+    'specifications/bcastByz/bcastByz.tla',
+    'specifications/MisraReachability/ReachabilityProofs.tla'
+]
+
+proof_module_paths = [
+    module['path']
+    for spec in manifest['specifications']
+    for module in spec['modules']
+    if 'proof' in module['features']
+        and module['path'] not in failing_proofs
+        and module['path'] not in long_running_proofs
+]
+
+success = True
+tlapm_path = join(tlapm_path, 'bin', 'tlapm')
+for module_path in proof_module_paths:
+    print(module_path)
+    start_time = timer()
+    module_path = tla_utils.from_cwd(examples_root, module_path)
+    module_dir = dirname(module_path)
+    tlapm = subprocess.run(
+        [
+            tlapm_path, module_path,
+            '-I', module_dir
+        ], capture_output=True
+    )
+    end_time = timer()
+    print(f'Checked proofs in {end_time - start_time:.1f}s')
+    if tlapm.returncode != 0:
+        print('FAILURE')
+        print(tlapm.stderr.decode('utf-8'))
+        success = False
+
+exit(0 if success else 1)
+

.github/workflows/CI.yml

@@ -63,11 +63,23 @@ jobs:
           mkdir deps/community
           wget https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar \
                 -O deps/community/modules.jar
-          # Get TLAPS
+          # Get TLAPS modules
           wget https://github.com/tlaplus/tlapm/archive/refs/tags/$TLAPS_VERSION.tar.gz
           tar -xf $TLAPS_VERSION.tar.gz
           rm $TLAPS_VERSION.tar.gz
           mv tlapm-$TLAPS_VERSION deps/tlapm
+          # Install TLAPS on non-Windows environments
+          if [[ "${{ runner.os }}" != "Windows" ]]; then
+            if [[ "${{ runner.os }}" == "Linux" ]]; then
+              TLAPM_BIN_TYPE=x86_64-linux-gnu
+            elif [[ "${{ runner.os }}" == "macOS" ]]; then
+              TLAPM_BIN_TYPE=i386-darwin
+            fi
+            TLAPM_BIN="tlaps-1.5.0-$TLAPM_BIN_TYPE-inst.bin"
+            wget https://github.com/tlaplus/tlapm/releases/download/$TLAPS_VERSION/$TLAPM_BIN
+            chmod +x $TLAPM_BIN
+            ./$TLAPM_BIN -d deps/tlapm-install
+          fi
       - name: Check manifest.json format
         shell: bash
         run: |
@@ -110,6 +122,12 @@ jobs:
             --tlapm_lib_path deps/tlapm/library                     \
             --community_modules_jar_path deps/community/modules.jar \
             --manifest_path manifest.json
+      - name: Check proofs
+        if: matrix.os != 'windows-latest'
+        run: |
+          python $SCRIPT_DIR/check_proofs.py  \
+            --tlapm_path deps/tlapm-install   \
+            --manifest_path manifest.json
       - name: Smoke-test manifest generation script
         shell: bash
         run: |

.gitignore

@@ -32,13 +32,12 @@ __tlacache__
 ## Don't ignore READMEs
 !*.md
 
-## Ignore pycache
+## Ignore Python artifacts
 __pycache__
+pyvenv.cfg
 
 ## Ignore directories used for local CI testing
-CommunityModules/
-tlapm/
-tree-sitter-tlaplus/
+deps/
 
 # Ignore TTrace specs
 *_TTrace_*.tla