Manifest: remove community module usage details

.github/scripts/check_manifest_features.py

@@ -2,8 +2,8 @@
 This script performs whatever validations are possible on the metadata in
 the manifest.json files. Prominent checks include:
  * .tla files containing pluscal or proofs are marked as such
- * .tla files importing community modules have those modules listed
- * Human-written fields are not empty
+ * Model state counts are applicable to the model type
+ * Human-written fields such as authorship are not empty
 """
 
 from argparse import ArgumentParser
@@ -75,81 +75,6 @@ def get_module_features(examples_root, path, parser, queries):
     tree, _, _ = tla_utils.parse_module(examples_root, parser, path)
     return get_tree_features(tree, queries)
 
-# All the standard modules available when using TLC
-tlc_modules = {
-    'Bags',
-    'FiniteSets',
-    'Integers',
-    'Json',
-    'Naturals',
-    'Randomization',
-    'RealTime',
-    'Reals',
-    'Sequences',
-    'TLC',
-    'TLCExt',
-    'Toolbox',
-    'Apalache'
-}
-
-# All the standard modules available when using TLAPS
-tlaps_modules = {
-    'BagsTheorems',
-    'FiniteSetTheorems',
-    'FunctionForkTheorems',
-    'FunctionsFork',
-    'NaturalsInduction',
-    'SequencesExtForkTheorems',
-    'SequenceTheorems',
-    'TLAPS',
-    'WellFoundedInduction'
-}
-
-# Modules overloaded by TLAPS; some of these are ordinarily imported as
-# community modules.
-tlaps_module_overloads = {
-    'Bags',
-    'FiniteSets',
-    'Functions',
-    'RealTime',
-    'SequencesExt'
-}
-
-def get_community_imports(examples_root, tree, text, dir, has_proof, queries):
-    """
-    Gets all modules imported by a given .tla file that are not standard
-    modules or modules in the same file or directory. Community module
-    imports are what's left.
-    """
-    imports = set(
-        [
-            tla_utils.node_to_string(text, node)
-            for node in tla_utils.all_nodes_of(queries.imports.captures(tree.root_node))
-        ]
-    )
-    modules_in_file = set(
-        [
-            tla_utils.node_to_string(text, node)
-            for node in tla_utils.all_nodes_of(queries.module_names.captures(tree.root_node))
-        ]
-    )
-    imports = (
-        imports
-        - modules_in_file
-        - tlc_modules
-        - tlaps_modules
-        - get_module_names_in_dir(examples_root, dir)
-    )
-    return imports - tlaps_module_overloads if has_proof else imports
-
-def get_community_module_imports(examples_root, parser, path, queries):
-    """
-    Gets all community modules imported by the .tla file at the given path.
-    """
-    tree, text, _ = tla_utils.parse_module(examples_root, parser, path)
-    has_proof = 'proof' in get_tree_features(tree, queries)
-    return get_community_imports(examples_root, tree, text, dirname(path), has_proof, queries)
-
 def check_features(parser, queries, manifest, examples_root):
     """
     Validates every field of the manifest that can be validated.
@@ -177,14 +102,6 @@ def check_features(parser, queries, manifest, examples_root):
             if 'proof' in module_features and 'proof' not in module:
                 success = False
                 logging.error(f'Module {module["path"]} contains proof but no proof runtime details in manifest')
-            expected_imports = get_community_imports(examples_root, tree, text, dirname(module_path), 'proof' in module_features, queries)
-            actual_imports = set(module['communityDependencies'])
-            if expected_imports != actual_imports:
-                success = False
-                logging.error(
-                    f'Module {module["path"]} has incorrect community dependencies in manifest; '
-                    + f'expected {list(expected_imports)}, actual {list(actual_imports)}'
-                )
             for model in module['models']:
                 if tla_utils.has_state_count(model) and not tla_utils.is_state_count_valid(model):
                     success = False

.github/scripts/check_proofs.py

@@ -80,7 +80,7 @@
             logging.debug(output)
     except subprocess.TimeoutExpired as tlapm_result:
         # stdout is a string on Windows, byte array everywhere else
-        stdout = tlapm_result.stdout if type(tlapm_result.stdout) == str else tlapm_result.stdout.decode('utf-8')
+        stdout = '' if tlapm_result.stdout is None else tlapm_result.stdout if type(tlapm_result.stdout) == str else tlapm_result.stdout.decode('utf-8')
         args, timeout = tlapm_result.args
         logging.error(f'{module_path} hit hard timeout of {timeout} seconds')
         output = ' '.join(args) + '\n' + stdout

.github/scripts/generate_manifest.py

@@ -83,7 +83,6 @@ def generate_new_manifest(examples_root, spec_path, spec_name, parser, queries):
         'modules': [
             {
                 'path': tla_utils.to_posix(tla_path),
-                'communityDependencies': sorted(list(get_community_module_imports(examples_root, parser, tla_path, queries))),
                 'features': sorted(list(module_features - {'proof'})),
                 'models': [
                     {

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 the `communityDependencies` and `models`
+   - 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`
      - 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

@@ -19,14 +19,10 @@
       "type": "array",
       "items": {
         "type": "object",
-        "required": ["path", "communityDependencies", "features", "models"],
+        "required": ["path", "features", "models"],
         "additionalProperties": false,
         "properties": {
           "path": {"type": "string"},
-          "communityDependencies": {
-            "type": "array",
-            "items": {"type": "string"}
-          },
           "features": {
             "type": "array",
             "items": {"enum": ["pluscal", "action composition"]}

specifications/Bakery-Boulangerie/manifest.json

@@ -8,7 +8,6 @@
   "modules": [
     {
       "path": "specifications/Bakery-Boulangerie/Bakery.tla",
-      "communityDependencies": [],
       "features": [
         "pluscal"
       ],
@@ -19,7 +18,6 @@
     },
     {
       "path": "specifications/Bakery-Boulangerie/Boulanger.tla",
-      "communityDependencies": [],
       "features": [
         "pluscal"
       ],
@@ -30,7 +28,6 @@
     },
     {
       "path": "specifications/Bakery-Boulangerie/MCBakery.tla",
-      "communityDependencies": [],
       "features": [],
       "models": [
         {
@@ -46,7 +43,6 @@
     },
     {
       "path": "specifications/Bakery-Boulangerie/MCBoulanger.tla",
-      "communityDependencies": [],
       "features": [],
       "models": [
         {
@@ -58,4 +54,4 @@
       ]
     }
   ]
-}
+}

specifications/CarTalkPuzzle/manifest.json

@@ -9,19 +9,16 @@
   "modules": [
     {
       "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.tla",
-      "communityDependencies": [],
       "features": [],
       "models": []
     },
     {
       "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_1/CarTalkPuzzle.tla",
-      "communityDependencies": [],
       "features": [],
       "models": []
     },
     {
       "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_1/MC.tla",
-      "communityDependencies": [],
       "features": [],
       "models": [
         {
@@ -37,13 +34,11 @@
     },
     {
       "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_2/CarTalkPuzzle.tla",
-      "communityDependencies": [],
       "features": [],
       "models": []
     },
     {
       "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_2/MC.tla",
-      "communityDependencies": [],
       "features": [],
       "models": [
         {
@@ -59,13 +54,11 @@
     },
     {
       "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_3/CarTalkPuzzle.tla",
-      "communityDependencies": [],
       "features": [],
       "models": []
     },
     {
       "path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_3/MC.tla",
-      "communityDependencies": [],
       "features": [],
       "models": [
         {

specifications/Chameneos/manifest.json

@@ -9,7 +9,6 @@
   "modules": [
     {
       "path": "specifications/Chameneos/Chameneos.tla",
-      "communityDependencies": [],
       "features": [],
       "models": [
         {

specifications/CheckpointCoordination/manifest.json

@@ -10,13 +10,11 @@
   "modules": [
     {
       "path": "specifications/CheckpointCoordination/CheckpointCoordination.tla",
-      "communityDependencies": [],
       "features": [],
       "models": []
     },
     {
       "path": "specifications/CheckpointCoordination/MCCheckpointCoordination.tla",
-      "communityDependencies": [],
       "features": [],
       "models": [
         {

specifications/CigaretteSmokers/manifest.json

@@ -9,7 +9,6 @@
   "modules": [
     {
       "path": "specifications/CigaretteSmokers/CigaretteSmokers.tla",
-      "communityDependencies": [],
       "features": [],
       "models": [
         {

specifications/CoffeeCan/manifest.json

@@ -11,7 +11,6 @@
   "modules": [
     {
       "path": "specifications/CoffeeCan/CoffeeCan.tla",
-      "communityDependencies": [],
       "features": [],
       "models": [
         {

specifications/DieHard/manifest.json

@@ -9,7 +9,6 @@
   "modules": [
     {
       "path": "specifications/DieHard/DieHard.tla",
-      "communityDependencies": [],
       "features": [],
       "models": [
         {
@@ -22,13 +21,11 @@
     },
     {
       "path": "specifications/DieHard/DieHarder.tla",
-      "communityDependencies": [],
       "features": [],
       "models": []
     },
     {
       "path": "specifications/DieHard/MCDieHarder.tla",
-      "communityDependencies": [],
       "features": [],
       "models": [
         {

specifications/DiningPhilosophers/manifest.json

@@ -9,7 +9,6 @@
   "modules": [
     {
       "path": "specifications/DiningPhilosophers/DiningPhilosophers.tla",
-      "communityDependencies": [],
       "features": [
         "pluscal"
       ],

specifications/Disruptor/manifest.json

@@ -9,7 +9,6 @@
   "modules": [
     {
       "path": "specifications/Disruptor/Disruptor_MPMC.tla",
-      "communityDependencies": [],
       "features": [],
       "models": [
         {
@@ -34,7 +33,6 @@
     },
     {
       "path": "specifications/Disruptor/Disruptor_SPMC.tla",
-      "communityDependencies": [],
       "features": [],
       "models": [
         {
@@ -50,7 +48,6 @@
     },
     {
       "path": "specifications/Disruptor/RingBuffer.tla",
-      "communityDependencies": [],
       "features": [],
       "models": []
     }

specifications/EinsteinRiddle/manifest.json

@@ -8,7 +8,6 @@
   "modules": [
     {
       "path": "specifications/EinsteinRiddle/Einstein.tla",
-      "communityDependencies": [],
       "features": [],
       "models": [
         {