CI: use bash instead of python for proof checking

Signed-off-by: Andrew Helwer <ahelwer@pm.me>

Author: ahelwer

.github/scripts/check_proofs.py

@@ -26,24 +26,21 @@
 
 logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)
 
-proof_module_paths = sorted(
-    [
-        (manifest_dir, spec, module, tla_utils.parse_timespan(module['proof']['runtime']))
-        for manifest_dir, spec in manifest
-        for module in spec['modules']
-        if 'proof' in module
-            and module['path'] not in skip_modules
-            and (only_modules == [] or module['path'] in only_modules)
-    ],
-    key = lambda m : m[3]
-)
+proof_module_paths = [
+    (manifest_dir, spec, module)
+    for manifest_dir, spec in manifest
+    for module in spec['modules']
+    if 'proof' in module
+        and module['path'] not in skip_modules
+        and (only_modules == [] or module['path'] in only_modules)
+]
 
 for path in skip_modules:
     logging.info(f'Skipping {path}')
 
 success = True
 tlapm_path = join(tlapm_path, 'bin', 'tlapm')
-for manifest_dir, spec, module, expected_runtime in proof_module_paths:
+for manifest_dir, spec, module in proof_module_paths:
     module_path = module['path']
     logging.info(module_path)
     start_time = timer()
@@ -63,16 +60,12 @@
         end_time = timer()
         actual_runtime = timedelta(seconds = end_time - start_time)
         output = ' '.join(tlapm_result.args) + '\n' + tlapm_result.stdout
-        logging.info(f'Checked proofs in {tla_utils.format_timespan(actual_runtime)} vs. {tla_utils.format_timespan(expected_runtime)} expected')
+        logging.info(f'Checked proofs in {tla_utils.format_timespan(actual_runtime)}')
         if tlapm_result.returncode != 0:
             logging.error(f'Proof checking failed for {module_path}:')
             logging.error(output)
             success = False
         else:
-            if 'proof' not in module or module['proof']['runtime'] == 'unknown':
-                module['proof'] = { 'runtime' : tla_utils.format_timespan(actual_runtime) }
-                manifest_path = join(manifest_dir, 'manifest.json')
-                tla_utils.write_json(spec, manifest_path)
             logging.debug(output)
     except subprocess.TimeoutExpired as tlapm_result:
         # stdout is a string on Windows, byte array everywhere else

.github/scripts/linux-setup.sh

@@ -48,6 +48,7 @@ main() {
   mkdir -p "$DEPS_DIR/community"
   wget -nv https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar \
         -O "$DEPS_DIR/community/modules.jar"
+  unzip "$DEPS_DIR/community/modules.jar" -d "$DEPS_DIR/community/"
   # Get TLAPS modules
   wget -nv https://github.com/tlaplus/tlapm/archive/main.tar.gz -O /tmp/tlapm.tar.gz
   tar -xzf /tmp/tlapm.tar.gz --directory "$DEPS_DIR"

.github/workflows/CI.yml

@@ -135,9 +135,40 @@ jobs:
       - name: Check proofs
         if: matrix.os != 'windows-latest' && !matrix.unicode
         run: |
-          python $SCRIPT_DIR/check_proofs.py       \
-            --tlapm_path $DEPS_DIR/tlapm           \
-            --examples_root .
+          # Exempting specs for various reasons:
+          # - Use of RECURSIVE, which TLAPM cannot currently handle (many)
+          # - Pre-module text bug (MCDistributedReplicatedLog.tla)
+          # - Unresolved ToString operator (ewd840)
+          # - Use of nonstandard TLCExt module (SimKnuthYao.tla)
+          # - Use of nonstandard Randomization module (SpanTreeTest.tla)
+          # - Nonstandard multi-module (BufferedRandomAccessFile.tla)
+          # - Nested module identifier bug (diskpaxos, Composing, RealTime)
+          # - TLAPM level-checking failure (YoYoPruning.tla)
+          # - Use of Apalache module (Einstein.tla)
+          # - Very long-running proof (BPConProof.tla)
+          find specifications -type f -iname "*.tla"            \
+            \(                                                  \
+                   -not -name "Chameneos.tla"                   \
+              -and -not -name "ReachabilityTest.tla"            \
+              -and -not -name "MCReachabilityTest.tla"          \
+              -and -not -name "MCDistributedReplicatedLog.tla"  \
+              -and -not -name "SimKnuthYao.tla"                 \
+              -and -not -name "SpanTreeTest.tla"                \
+              -and -not -name "TransitiveClosure.tla"           \
+              -and -not -name "BufferedRandomAccessFile.tla"    \
+              -and -not -name "YoYoPruning.tla"                 \
+              -and -not -name "MCYoYoPruning.tla"               \
+              -and -not -name "Einstein.tla"                    \
+              -and -not -name "BPConProof.tla"                  \
+              -and -not -wholename "*/Composing/*"              \
+              -and -not -wholename "*/RealTime/*"               \
+              -and -not -wholename "*/LeastCircularSubstring/*" \
+              -and -not -wholename "*/diskpaxos/*"              \
+              -and -not -wholename "*/ewd998/*"                 \
+              -and -not -wholename "*/ewd840/*"                 \
+            \)                                                  \
+            -print0 | xargs -0 -n1 -r -t               \
+            time $DEPS_DIR/tlapm/bin/tlapm --cleanfp --stretch 5 -I $DEPS_DIR/community
       - name: Smoke-test manifest generation script
         run: |
           python $SCRIPT_DIR/generate_manifest.py \

specifications/CoffeeCan/manifest.json

@@ -15,7 +15,7 @@
       "models": [
         {
           "path": "specifications/CoffeeCan/CoffeeCan1000Beans.cfg",
-          "runtime": "00:00:15",
+          "runtime": "00:00:45",
           "mode": "exhaustive search",
           "result": "success",
           "distinctStates": 501500,
@@ -40,4 +40,4 @@
       ]
     }
   ]
-}
+}