Split centralized manifest.json into per-spec manifest.json files

.github/scripts/check_manifest_features.py

@@ -1,6 +1,6 @@
 """
 This script performs whatever validations are possible on the metadata in
-the manifest.json file. Prominent checks include:
+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
  * .cfg files with certain features are marked as such
@@ -183,7 +183,7 @@ def check_features(parser, queries, manifest, examples_root):
     Validates every field of the manifest that can be validated.
     """
     success = True
-    for spec in manifest['specifications']:
+    for spec in manifest:
         if spec['title'] == '':
             success = False
             logging.error(f'Spec {spec["path"]} does not have a title')
@@ -234,19 +234,17 @@ def check_features(parser, queries, manifest, examples_root):
     return success
 
 if __name__ == '__main__':
-    parser = ArgumentParser(description='Checks metadata in tlaplus/examples manifest.json against module and model files in repository.')
-    parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True)
+    parser = ArgumentParser(description='Checks metadata in manifest.json files against module and model files in repository.')
+    parser.add_argument('--examples_root', help='Root directory of the tlaplus/examples repository', required=True)
     args = parser.parse_args()
 
-    manifest_path = normpath(args.manifest_path)
-    manifest = tla_utils.load_json(manifest_path)
-    examples_root = dirname(manifest_path)
+    manifest = tla_utils.load_all_manifests(args.examples_root)
 
     TLAPLUS_LANGUAGE = Language(tree_sitter_tlaplus.language())
     parser = Parser(TLAPLUS_LANGUAGE)
     queries = build_queries(TLAPLUS_LANGUAGE)
 
-    if check_features(parser, queries, manifest, examples_root):
+    if check_features(parser, queries, manifest, args.examples_root):
         logging.info('SUCCESS: metadata in manifest is correct')
         exit(0)
     else:

.github/scripts/check_manifest_files.py

@@ -1,8 +1,8 @@
 """
 Checks to ensure all files in manifest.json exist, that all .tla and .cfg
 files in repo are recorded in manifest.json (except for those in .ciignore),
-and that no files are present twice in the manifest. Also checks to ensure
-no files in .ciignore are in the manifest.json.
+and that no files are present twice in the manifests. Also checks to ensure
+no files in .ciignore are in the manifest.json files.
 """
 
 from argparse import ArgumentParser
@@ -11,17 +11,15 @@
 import glob
 import tla_utils
 
-parser = ArgumentParser(description='Checks tlaplus/examples manifest.json against module and model files in repository.')
-parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True)
+parser = ArgumentParser(description='Checks manifests against module and model files in repository.')
 parser.add_argument('--ci_ignore_path', help='Path to the .ciignore file', required=True)
 args = parser.parse_args()
 
-manifest_path = normpath(args.manifest_path)
 ci_ignore_path = normpath(args.ci_ignore_path)
-examples_root = dirname(manifest_path)
-manifest = tla_utils.load_json(manifest_path)
+examples_root = dirname(ci_ignore_path)
+manifest = tla_utils.load_all_manifests(examples_root)
 
-module_lists = [spec["modules"] for spec in manifest["specifications"]]
+module_lists = [spec["modules"] for spec in manifest]
 modules = [module for module_list in module_lists for module in module_list]
 model_lists = [module["models"] for module in modules]
 

.github/scripts/check_manifest_schema.py

@@ -1,29 +1,38 @@
 """
-Checks to ensure manifest.json is valid according to schema; this can also
-be done manually at https://www.jsonschemavalidator.net/
+Checks to ensure manifest.json in each specifications/ subdirectory is valid
+according to schema; this can also be done manually at
+https://www.jsonschemavalidator.net/
+
 Learn about the JSON schema format at
 https://json-schema.org/understanding-json-schema/
 """
 
 from argparse import ArgumentParser
 from jsonschema import validate
-from os.path import normpath
+from jsonschema.exceptions import ValidationError
+from os.path import normpath, dirname, join
+from sys import stderr
 import tla_utils
 
-parser = ArgumentParser(description='Checks tlaplus/examples manifest.json against JSON schema file.')
-parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True)
+parser = ArgumentParser(description='Checks tlaplus/examples manifest.json files against JSON schema file.')
 parser.add_argument('--schema_path', help='Path to the tlaplus/examples manifest-schema.json file', required=True)
 args = parser.parse_args()
 
+examples_root = dirname(args.schema_path)
 schema = tla_utils.load_json(normpath(args.schema_path))
-manifest = tla_utils.load_json(normpath(args.manifest_path))
+failures = []
+for manifest in tla_utils.load_all_manifests(examples_root):
+    manifest_path = join(manifest['path'], "manifest.json")
+    try:
+        validate(instance=manifest, schema=schema)
+    except ValidationError as error:
+        print(f'FAILURE: schema NOT matched by {manifest_path}', file=stderr)
+        failures.append((manifest_path, error))
+    else:
+        print(f'SUCCESS: schema matched by {manifest_path}')
+
+for (manifest_path, manifest_error) in failures:
+    print(f'\nSchema failure in {manifest_path}:\n{manifest_error}\n', file=stderr)
 
-result = validate(instance=manifest, schema=schema)
-if None == result:
-    print('SUCCESS: Manifest correctly follows schema')
-    exit(0)
-else:
-    print('ERROR: Manifest does not follow schema')
-    print(result)
-    exit(1)
+exit(1 if any(failures) else 0)
 

.github/scripts/check_markdown_table.py

@@ -1,10 +1,10 @@
 """
-Validates the spec table in README.md, ensuring it matches manifest.json.
+Validates the spec table in README.md, ensuring it matches manifest.json files.
 """
 
 from argparse import ArgumentParser
 from dataclasses import dataclass
-from os.path import normpath
+from os.path import normpath, dirname
 from typing import Any, Set
 import tla_utils
 import mistletoe
@@ -75,11 +75,10 @@ def from_json(spec):
     )
 
 parser = ArgumentParser(description='Validates the spec table in README.md against the manifest.json.')
-parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True)
 parser.add_argument('--readme_path', help='Path to the tlaplus/examples README.md file', required=True)
 args = parser.parse_args()
 
-manifest = tla_utils.load_json(normpath(args.manifest_path))
+manifest = tla_utils.load_all_manifests(dirname(args.readme_path))
 
 readme = None
 with open(normpath(args.readme_path), 'r', encoding='utf-8') as readme_file:
@@ -88,7 +87,7 @@ def from_json(spec):
 spec_table = next((child for child in readme.children if isinstance(child, Table)))
 
 table_specs = dict([(record.path, record) for record in [from_markdown(node) for node in spec_table.children]])
-manifest_specs = dict([(record.path, record) for record in [from_json(spec) for spec in manifest['specifications']]])
+manifest_specs = dict([(record.path, record) for record in [from_json(spec) for spec in manifest]])
 
 # Checks that set of specs in manifest and table are equivalent
 success = True

.github/scripts/check_proofs.py

@@ -11,24 +11,23 @@
 
 parser = ArgumentParser(description='Validate all proofs in all modules with TLAPM.')
 parser.add_argument('--tlapm_path', help='Path to TLAPM install dir; should have bin and lib subdirs', 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 .tla modules to skip checking', required=False, default=[])
 parser.add_argument('--only', nargs='+', help='If provided, only check proofs in this space-separated list', required=False, default=[])
 parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
 args = parser.parse_args()
 
 tlapm_path = normpath(args.tlapm_path)
-manifest_path = normpath(args.manifest_path)
-manifest = tla_utils.load_json(manifest_path)
-examples_root = dirname(manifest_path)
+examples_root = args.examples_root
+manifest = tla_utils.load_all_manifests(examples_root)
 skip_modules = args.skip
 only_modules = args.only
 
 logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)
 
 proof_module_paths = [
     module['path']
-    for spec in manifest['specifications']
+    for spec in manifest
     for module in spec['modules']
         if 'proof' in module['features']
         and module['path'] not in skip_modules

.github/scripts/check_small_models.py

@@ -1,5 +1,5 @@
 """
-Check all models marked as size "small" in the manifest with TLC. Small
+Check all models marked as size "small" in each manifest with TLC. Small
 models should finish executing in less than ten seconds on the GitHub CI
 machines.
 """
@@ -16,7 +16,7 @@
 parser.add_argument('--apalache_path', help='Path to the Apalache directory', 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('--verbose', help='Set logging output level to debug', action='store_true')
@@ -29,8 +29,7 @@
 apalache_path = normpath(args.apalache_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
 enable_assertions = args.enable_assertions
@@ -87,11 +86,11 @@ def check_model(module, model, expected_runtime):
             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']
+        for spec in manifest
         for module in spec['modules']
         for model in module['models']
             if model['size'] == 'small'

.github/scripts/generate_manifest.py

@@ -1,5 +1,5 @@
 """
-Generates a best-effort manifest.json file. This is done by scanning all
+Generates best-effort manifest.json files. This is done by scanning all
 .tla and .cfg files in the specifications dir then attempting to sort them
 into a spec/module/model hierarchy. Files are parsed to check for features
 and imports. Human-written fields (title/description/source/authors for
@@ -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
@@ -69,57 +69,49 @@ def get_cfg_files(examples_root, tla_path):
         ])
     ]
 
-def generate_new_manifest(examples_root, ignored_dirs, parser, queries):
+def generate_new_manifest(examples_root, spec_path, spec_name, parser, queries):
     """
-    Generate new base manifest.json from files in specifications dir.
+    Generate new manifest.json file for a given specification directory.
     """
     return {
-        'specifications': [
+        'path': to_posix(spec_path),
+        'title': spec_name,
+        'description': '',
+        'sources': [],
+        'authors': [],
+        'tags': [],
+        'modules': [
             {
-                'path': to_posix(spec_path),
-                'title': spec_name,
-                'description': '',
-                'sources': [],
-                'authors': [],
-                'tags': [],
-                'modules': [
+                'path': to_posix(tla_path),
+                'communityDependencies': sorted(list(get_community_module_imports(examples_root, parser, tla_path, queries))),
+                'tlaLanguageVersion': 2,
+                'features': sorted(list(get_module_features(examples_root, tla_path, parser, queries))),
+                'models': [
                     {
-                        'path': to_posix(tla_path),
-                        'communityDependencies': sorted(list(get_community_module_imports(examples_root, parser, tla_path, queries))),
-                        'tlaLanguageVersion': 2,
-                        'features': sorted(list(get_module_features(examples_root, tla_path, parser, queries))),
-                        'models': [
-                            {
-                                'path': to_posix(cfg_path),
-                                'runtime': 'unknown',
-                                'size': 'unknown',
-                                'mode': 'exhaustive search',
-                                'features': sorted(list(get_model_features(examples_root, cfg_path))),
-                                'result': 'unknown'
-                            }
-                            for cfg_path in sorted(get_cfg_files(examples_root, tla_path))
-                        ]
+                        'path': to_posix(cfg_path),
+                        'runtime': 'unknown',
+                        'size': 'unknown',
+                        'mode': 'exhaustive search',
+                        'features': sorted(list(get_model_features(examples_root, cfg_path))),
+                        'result': 'unknown'
                     }
-                    for tla_path in sorted(get_tla_files(examples_root, spec_path))
+                    for cfg_path in sorted(get_cfg_files(examples_root, tla_path))
                 ]
             }
-            for (spec_path, spec_name) in get_spec_dirs(examples_root, ignored_dirs)
+            for tla_path in sorted(get_tla_files(examples_root, spec_path))
         ]
     }
 
 # Integrate human-written info from existing manifest.json
 
-def find_corresponding_spec(old_spec, new_manifest):
-    specs = [
-        spec for spec in new_manifest['specifications']
-        if to_posix(spec['path']) == old_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 = [
@@ -146,41 +138,37 @@ def integrate_model_info(old_model, new_model):
         if field in old_model:
             new_model[field] = old_model[field]
 
-def integrate_old_manifest_into_new(old_manifest, new_manifest):
-    for old_spec in old_manifest['specifications']:
-        new_spec = find_corresponding_spec(old_spec, new_manifest)
-        if new_spec is None:
+def integrate_old_manifest_into_new(old_manifest, new_spec):
+    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
-        integrate_spec_info(old_spec, new_spec)
-        for old_module in old_spec['modules']:
-            new_module = find_corresponding_module(old_module, new_spec)
-            if new_module is None:
+        integrate_module_info(old_module, new_module)
+        for old_model in old_module['models']:
+            new_model = find_corresponding_model(old_model, new_module)
+            if new_model is None:
                 continue
-            integrate_module_info(old_module, new_module)
-            for old_model in old_module['models']:
-                new_model = find_corresponding_model(old_model, new_module)
-                if new_model is None:
-                    continue
-                integrate_model_info(old_model, new_model)
+            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)
-    new_manifest = generate_new_manifest(examples_root, ignored_dirs, parser, queries)
-    integrate_old_manifest_into_new(old_manifest, new_manifest)
-
-    tla_utils.write_json(new_manifest, 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'))