Added skip parameter to proof checking script

Signed-off-by: Andrew Helwer <[email protected]>
tlaplus · Nov 11, 2023 · 7d2fea7 · 7d2fea7
1 parent 6a36a86
commit 7d2fea7
Show file tree

Hide file tree

Showing 2 changed files with 30 additions and 26 deletions.
diff --git a/.github/scripts/check_proofs.py b/.github/scripts/check_proofs.py
@@ -4,51 +4,40 @@
 
 from argparse import ArgumentParser
 from os.path import dirname, join, normpath
+import logging
 import subprocess
 from timeit import default_timer as timer
 import tla_utils
 
+logging.basicConfig(level=logging.INFO)
+
 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)
+parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip checking', required=False, default=[])
 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'
-]
+skip_modules = [normpath(path) for path in args.skip]
 
 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
+        if 'proof' in module['features']
+        and normpath(module['path']) not in skip_modules
 ]
 
+for path in skip_modules:
+    logging.info(f'Skipping {path}')
+
 success = True
 tlapm_path = join(tlapm_path, 'bin', 'tlapm')
 for module_path in proof_module_paths:
-    print(module_path)
+    logging.info(module_path)
     start_time = timer()
     module_path = tla_utils.from_cwd(examples_root, module_path)
     module_dir = dirname(module_path)
@@ -59,10 +48,10 @@
         ], capture_output=True
     )
     end_time = timer()
-    print(f'Checked proofs in {end_time - start_time:.1f}s')
+    logging.info(f'Checked proofs in {end_time - start_time:.1f}s')
     if tlapm.returncode != 0:
-        print('FAILURE')
-        print(tlapm.stderr.decode('utf-8'))
+        logging.error(f'Proof checking failed in {module_path}:')
+        logging.error(tlapm.stderr.decode('utf-8'))
         success = False
 
 exit(0 if success else 1)

diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
@@ -167,9 +167,24 @@ jobs:
       - name: Check proofs
         if: matrix.os != 'windows-latest'
         run: |
+          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
+            # 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
+          )
           python $SCRIPT_DIR/check_proofs.py  \
             --tlapm_path deps/tlapm-install   \
-            --manifest_path manifest.json
+            --manifest_path manifest.json     \
+            --skip "${SKIP[@]}"
       - name: Smoke-test manifest generation script
         run: |
           rm -r deps/tree-sitter-tlaplus/build