Add skip parameter to python scripts (#96)

* Move skipped models list from script to CI * Normalize before comparing skip paths * Added skip parameter to parse and small model scripts * Added skip parameter to proof checking script Signed-off-by: Andrew Helwer <[email protected]>
tlaplus · Nov 14, 2023 · 68aec27 · 68aec27
1 parent 62d104f
commit 68aec27
Show file tree

Hide file tree

Showing 5 changed files with 64 additions and 47 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/scripts/check_small_models.py b/.github/scripts/check_small_models.py
@@ -16,6 +16,7 @@
 parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=True)
 parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', 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 models to skip checking', required=False, default=[])
 args = parser.parse_args()
 
 logging.basicConfig(level=logging.INFO)
@@ -25,6 +26,7 @@
 community_jar_path = normpath(args.community_modules_jar_path)
 manifest_path = normpath(args.manifest_path)
 examples_root = dirname(manifest_path)
+skip_models = [normpath(path) for path in args.skip]
 
 def check_model(module_path, model, expected_runtime):
     module_path = tla_utils.from_cwd(examples_root, module_path)
@@ -68,12 +70,17 @@ def check_model(module_path, model, expected_runtime):
         (module['path'], model, tla_utils.parse_timespan(model['runtime']))
         for spec in manifest['specifications']
         for module in spec['modules']
-        for model in module['models'] if model['size'] == 'small'
+        for model in module['models']
+            if model['size'] == 'small'
+            and normpath(model['path']) not in skip_models
     ],
     key = lambda m: m[2],
     reverse=True
 )
 
+for path in skip_models:
+    logging.info(f'Skipping {path}')
+
 success = all([check_model(*model) for model in small_models])
 exit(0 if success else 1)
 
diff --git a/.github/scripts/parse_modules.py b/.github/scripts/parse_modules.py
@@ -15,14 +15,17 @@
 parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=True)
 parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', 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 parsing', required=False, default=[])
 args = parser.parse_args()
 
+logging.basicConfig(level=logging.INFO)
+
 tools_jar_path = normpath(args.tools_jar_path)
 tlaps_modules = normpath(args.tlapm_lib_path)
 community_modules = normpath(args.community_modules_jar_path)
 manifest_path = normpath(args.manifest_path)
 examples_root = dirname(manifest_path)
-logging.basicConfig(level=logging.INFO)
+skip_modules = [normpath(path) for path in args.skip]
 
 def parse_module(path):
     """
@@ -45,20 +48,17 @@ def parse_module(path):
 
 manifest = tla_utils.load_json(manifest_path)
 
-# Skip these specs and modules as they do not currently parse
-skip_specs = [
-    # https://github.com/tlaplus/Examples/issues/66
-    'specifications/ewd998'
-]
-skip_modules = []
-
 # List of all modules to parse and whether they should use TLAPS imports
 modules = [
     tla_utils.from_cwd(examples_root, module['path'])
-    for spec in manifest['specifications'] if spec['path'] not in skip_specs
-    for module in spec['modules'] if module['path'] not in skip_modules
+    for spec in manifest['specifications']
+    for module in spec['modules']
+        if normpath(module['path']) not in skip_modules
 ]
 
+for path in skip_modules:
+    logging.info(f'Skipping {path}')
+
 # Parse specs in parallel
 thread_count = cpu_count()
 logging.info(f'Parsing using {thread_count} threads')

diff --git a/.github/scripts/smoke_test_large_models.py b/.github/scripts/smoke_test_large_models.py
@@ -16,13 +16,15 @@
 parser.add_argument('--tlapm_lib_path', help='Path to the TLA+ proof manager module directory; .tla files should be in this directory', required=True)
 parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', 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 models to skip checking', required=False, default=[])
 args = parser.parse_args()
 
 tools_jar_path = normpath(args.tools_jar_path)
 tlapm_lib_path = normpath(args.tlapm_lib_path)
 community_jar_path = normpath(args.community_modules_jar_path)
 manifest_path = normpath(args.manifest_path)
 examples_root = dirname(manifest_path)
+skip_models = [normpath(path) for path in args.skip]
 
 def check_model(module_path, model):
     module_path = tla_utils.from_cwd(examples_root, module_path)
@@ -59,23 +61,18 @@ def check_model(module_path, model):
 
 manifest = tla_utils.load_json(manifest_path)
 
-skip_models = [
-    # SimKnuthYao requires certain number of states to have been generated
-    # before termination or else it fails. This makes it not amenable to
-    # smoke testing.
-    'specifications/KnuthYao/SimKnuthYao.cfg',
-    # SimTokenRing does not work on Windows systems.
-] + (['specifications/ewd426/SimTokenRing.cfg'] if os.name == 'nt' else [])
-
 large_models = [
     (module['path'], model)
     for spec in manifest['specifications']
     for module in spec['modules']
     for model in module['models']
         if model['size'] != 'small'
-        and model['path'] not in skip_models
+        and normpath(model['path']) not in skip_models
 ]
 
+for path in skip_models:
+    logging.info(f'Skipping {path}')
+
 success = all([check_model(*model) for model in large_models])
 exit(0 if success else 1)
 
diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
@@ -150,17 +150,41 @@ jobs:
             --manifest_path manifest.json
       - name: Smoke-test large models
         run: |
+          # 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/tools/tla2tools.jar               \
             --tlapm_lib_path deps/tlapm/library                     \
             --community_modules_jar_path deps/community/modules.jar \
-            --manifest_path manifest.json
+            --manifest_path manifest.json                           \
+            --skip "${SKIP[@]}"
       - 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