CI: filter on max proof time in manifests

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

Author: ahelwer

.github/scripts/generate_manifest.py

@@ -93,7 +93,7 @@ def generate_new_manifest(examples_root, spec_path, spec_name, parser, queries):
                     }
                     for cfg_path in sorted(get_cfg_files(examples_root, tla_path))
                 ]
-            } | ({'proof' : {'runtime': 'unknown'}} if 'proof' in module_features else {})
+            } | ({'proof' : {'maxRuntimeMinutes': 1}} if 'proof' in module_features else {})
             for tla_path, module_features in get_tla_file_features(examples_root, spec_path, parser, queries)
         ]
     }
@@ -133,7 +133,7 @@ def find_corresponding_model(old_model, new_module):
     return models[0] if any(models) else None
 
 def integrate_model_info(old_model, new_model):
-    fields = ['runtime', 'mode', 'result', 'distinctStates', 'totalStates', 'stateDepth']
+    fields = ['runtime', 'mode', 'result', 'distinctStates', 'totalStates', 'stateDepth', 'workers']
     for field in fields:
         if field in old_model:
             new_model[field] = old_model[field]

.github/workflows/CI.yml

@@ -38,6 +38,9 @@ jobs:
         with:
           distribution: adopt
           java-version: 17
+      - name: Install timeout command
+        if: matrix.os == 'macos-latest'
+        run: brew install coreutils
       - name: Download TLA⁺ dependencies (Windows)
         if: matrix.os == 'windows-latest'
         run: $SCRIPT_DIR/windows-setup.sh $SCRIPT_DIR $DEPS_DIR false
@@ -146,13 +149,12 @@ jobs:
             | map(select(has("proof")))
             # Failing on Linux
             | map(select(.path != "specifications/LoopInvariance/SumSequence.tla"))
-            # Take too long to check in the CI
-            | map(select(.path != "specifications/byzpaxos/BPConProof.tla"))
-            | map(select(.path != "specifications/tcp/tcp_proof.tla"))
-            | map(.path + "\u0000")
+            # Skip long-running proofs in CI
+            | map(select(.proof.maxRuntimeMinutes <= 5))
+            | map((.proof.maxRuntimeMinutes | tostring) + "\u0000" + .path + "\u0000")
             | join("")' \
-          | xargs --verbose --null --no-run-if-empty -I {TLA_FILE} \
-          time "$DEPS_DIR/tlapm/bin/tlapm" "{TLA_FILE}" -I "$DEPS_DIR/community" --stretch 5
+          | xargs --verbose --null --no-run-if-empty -n 2 \
+          sh -c 'time timeout --signal=KILL "${1}m" "$DEPS_DIR/tlapm/bin/tlapm" "$2" -I "$DEPS_DIR/community" --stretch 5' --
       - name: Smoke-test manifest generation script
         run: |
           python $SCRIPT_DIR/generate_manifest.py \

CONTRIBUTING.md

@@ -45,7 +45,7 @@ Steps:
    - Spec authors: a list of people who authored the spec
    - Spec tags:
      - `"beginner"` if your spec is appropriate for TLA⁺ newcomers
-   - Module proof runtime: if module contains formal proofs, record the approximate time necessary to check the proofs with TLAPM on an ordinary workstation; add `"proof" : { "runtime" : "HH:MM:SS" }` to the module fields at the same level as `models`
+   - Module proof runtime: if module contains formal proofs, record the estimated maximum time necessary to check the proofs with TLAPM on an underpowered workstation such as a CI runner machine; add `"proof" : { "maxRuntimeMinutes" : N }` to the module fields at the same level as `models`. If you have a relatively powerful machine this might up to twice the amount of time it takes locally. If your proof completes in only a couple seconds, put 1 for this value.
      - If less than one minute, proof will be checked in its entirety by the CI
    - Model runtime: approximate model runtime on an ordinary workstation, in `"HH:MM:SS"` format
      - If less than 30 seconds, will be run in its entirety by the CI; otherwise will only be smoke-tested for 5 seconds

manifest-schema.json

@@ -29,13 +29,10 @@
           },
           "proof": {
             "type": "object",
-            "required": ["runtime"],
+            "required": ["maxRuntimeMinutes"],
             "additionalProperties": false,
             "properties": {
-              "runtime": {
-                "type": "string",
-                "pattern": "^(([0-9][0-9]:[0-9][0-9]:[0-9][0-9])|unknown)$"
-              }
+              "maxRuntimeMinutes": {"type": "integer"}
             }
           },
           "models": {

specifications/Bakery-Boulangerie/manifest.json

@@ -13,7 +13,7 @@
       ],
       "models": [],
       "proof": {
-        "runtime": "00:00:20"
+        "maxRuntimeMinutes": 2
       }
     },
     {
@@ -23,7 +23,7 @@
       ],
       "models": [],
       "proof": {
-        "runtime": "00:00:30"
+        "maxRuntimeMinutes": 3
       }
     },
     {
@@ -54,4 +54,4 @@
       ]
     }
   ]
-}
+}

specifications/CigaretteSmokers/manifest.json

@@ -39,7 +39,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "unknown"
+        "maxRuntimeMinutes": 1
       }
     }
   ]

specifications/CoffeeCan/manifest.json

@@ -56,7 +56,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "unknown"
+        "maxRuntimeMinutes": 1
       }
     }
   ]

specifications/DieHard/manifest.json

@@ -36,6 +36,14 @@
         }
       ]
     },
+    {
+      "path": "specifications/DieHard/DieHard_proof.tla",
+      "features": [],
+      "models": [],
+      "proof": {
+        "maxRuntimeMinutes": 1
+      }
+    },
     {
       "path": "specifications/DieHard/DieHarder.tla",
       "features": [],
@@ -70,14 +78,6 @@
           "workers": 1
         }
       ]
-    },
-    {
-      "path": "specifications/DieHard/DieHard_proof.tla",
-      "features": [],
-      "models": [],
-      "proof": {
-        "runtime": "unknown"
-      }
     }
   ]
 }

specifications/Disruptor/manifest.json

@@ -19,11 +19,6 @@
         }
       ]
     },
-    {
-      "path": "specifications/Disruptor/APRingBuffer.tla",
-      "features": [],
-      "models": []
-    },
     {
       "path": "specifications/Disruptor/APDisruptor_SPMC.tla",
       "features": [],
@@ -36,6 +31,11 @@
         }
       ]
     },
+    {
+      "path": "specifications/Disruptor/APRingBuffer.tla",
+      "features": [],
+      "models": []
+    },
     {
       "path": "specifications/Disruptor/Disruptor_MPMC.tla",
       "features": [],

specifications/FiniteMonotonic/manifest.json

@@ -50,7 +50,7 @@
       "features": [],
       "models": [],
       "proof": {
-        "runtime": "00:00:01"
+        "maxRuntimeMinutes": 1
       }
     },
     {