Manifest generation and state space recording scripts now use split manifests

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

Author: ahelwer

.github/scripts/generate_manifest.py

@@ -9,7 +9,7 @@
 
 from check_manifest_features import *
 import os
-from os.path import basename, dirname, join, normpath, relpath, splitext
+from os.path import basename, dirname, join, normpath, relpath, splitext, isfile
 from pathlib import PureWindowsPath
 import glob
 import tla_utils
@@ -104,17 +104,14 @@ def generate_new_manifest(examples_root, spec_path, spec_name, parser, queries):
 
 # Integrate human-written info from existing manifest.json
 
-def find_corresponding_spec(old_manifest, new_spec):
-    specs = [
-        spec for spec in old_manifest['specifications']
-        if spec['path'] == new_spec['path']
-    ]
-    return specs[0] if any(specs) else None
+def get_old_manifest(spec_path):
+    old_manifest_path = join(spec_path, 'manifest.json')
+    return tla_utils.load_json(old_manifest_path) if isfile(old_manifest_path) else None
 
-def integrate_spec_info(old_spec, new_spec):
+def integrate_spec_info(old_manifest, new_spec):
     fields = ['title', 'description', 'authors', 'sources', 'tags']
     for field in fields:
-        new_spec[field] = old_spec[field]
+        new_spec[field] = old_manifest[field]
 
 def find_corresponding_module(old_module, new_spec):
     modules = [
@@ -142,9 +139,10 @@ def integrate_model_info(old_model, new_model):
             new_model[field] = old_model[field]
 
 def integrate_old_manifest_into_new(old_manifest, new_spec):
-    old_spec = find_corresponding_spec(old_manifest, new_spec)
-    integrate_spec_info(old_spec, new_spec)
-    for old_module in old_spec['modules']:
+    if old_manifest is None:
+        return
+    integrate_spec_info(old_manifest, new_spec)
+    for old_module in old_manifest['modules']:
         new_module = find_corresponding_module(old_module, new_spec)
         if new_module is None:
             continue
@@ -156,22 +154,20 @@ def integrate_old_manifest_into_new(old_manifest, new_spec):
             integrate_model_info(old_model, new_model)
 
 if __name__ == '__main__':
-    parser = ArgumentParser(description='Generates a new manifest.json derived from files in the repo.')
-    parser.add_argument('--manifest_path', help='Path to the current tlaplus/examples manifest.json file', default='manifest.json')
+    parser = ArgumentParser(description='Generates new manifest.json files derived from files in the repo.')
     parser.add_argument('--ci_ignore_path', help='Path to the CI ignore file', default='.ciignore')
     args = parser.parse_args()
 
-    manifest_path = normpath(args.manifest_path)
-    examples_root = dirname(manifest_path)
     ci_ignore_path = normpath(args.ci_ignore_path)
+    examples_root = dirname(ci_ignore_path)
     ignored_dirs = tla_utils.get_ignored_dirs(ci_ignore_path)
 
     TLAPLUS_LANGUAGE = Language(tree_sitter_tlaplus.language())
     parser = Parser(TLAPLUS_LANGUAGE)
     queries = build_queries(TLAPLUS_LANGUAGE)
 
-    old_manifest = tla_utils.load_json(manifest_path)
     for (spec_path, spec_name) in get_spec_dirs(examples_root, ignored_dirs):
+        old_manifest = get_old_manifest(spec_path)
         new_manifest = generate_new_manifest(examples_root, spec_path, spec_name, parser, queries)
         integrate_old_manifest_into_new(old_manifest, new_manifest)
         tla_utils.write_json(new_manifest, join(spec_path, 'manifest.json'))

.github/scripts/record_model_state_space.py

@@ -13,7 +13,7 @@
 parser.add_argument('--tools_jar_path', help='Path to the tla2tools.jar file', required=True)
 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('--examples_root', help='Root directory of the tlaplus/examples repository', required=True)
 parser.add_argument('--skip', nargs='+', help='Space-separated list of models to skip checking', required=False, default=[])
 parser.add_argument('--only', nargs='+', help='If provided, only check models in this space-separated list', required=False, default=[])
 parser.add_argument('--enable_assertions', help='Enable Java assertions (pass -enableassertions to JVM)', action='store_true')
@@ -25,8 +25,7 @@
 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)
+examples_root = args.examples_root
 skip_models = args.skip
 only_models = args.only
 run_all = args.all
@@ -77,11 +76,11 @@ def check_model(module, model):
             return False
 
 # Ensure longest-running modules go first
-manifest = tla_utils.load_json(manifest_path)
+manifest = tla_utils.load_all_manifests(examples_root)
 small_models = sorted(
     [
-        (module, model, tla_utils.parse_timespan(model['runtime']))
-        for spec in manifest['specifications']
+        (spec, module, model, tla_utils.parse_timespan(model['runtime']))
+        for spec in manifest
         for module in spec['modules']
         for model in module['models']
             if model['size'] == 'small'
@@ -105,7 +104,8 @@ def check_model(module, model):
 for path in skip_models:
     logging.info(f'Skipping {path}')
 
-for module, model, _ in small_models:
+for spec, module, model, _ in small_models:
+    manifest_path = join(spec['path'], 'manifest.json')
     success = check_model(module, model)
     if not success:
         exit(1)

.github/workflows/CI.yml

@@ -161,7 +161,6 @@ jobs:
       - name: Smoke-test manifest generation script
         run: |
           python $SCRIPT_DIR/generate_manifest.py \
-            --examples_root .                     \
             --ci_ignore_path .ciignore
           git diff -a
       - name: Smoke-test state space script