Move skipped models list from script to CI

Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>
tlaplus · Nov 11, 2023 · 90f9c4b · 90f9c4b
1 parent 62d104f
commit 90f9c4b
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 9 deletions.
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_models', nargs='+', help='Space-separated list of models to skip checking', required=False)
 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_models]
 
 def check_model(module_path, model):
     module_path = tla_utils.from_cwd(examples_root, module_path)
@@ -59,14 +61,6 @@ 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']
@@ -76,6 +70,9 @@ def check_model(module_path, model):
         and 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,11 +150,20 @@ 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_models "${SKIP[@]}"
       - name: Check proofs
         if: matrix.os != 'windows-latest'
         run: |