Changed all scripts and CI to use split manifest

Signed-off-by: Andrew Helwer <[email protected]>

Author: ahelwer

.github/scripts/check_manifest_features.py

@@ -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')
@@ -235,18 +235,16 @@ def check_features(parser, queries, manifest, examples_root):
 
 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.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

@@ -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_markdown_table.py

@@ -4,7 +4,7 @@
 
 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

@@ -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/parse_modules.py

@@ -15,7 +15,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 .tla modules to skip parsing', required=False, default=[])
 parser.add_argument('--only', nargs='+', help='If provided, only parse models in this space-separated list', required=False, default=[])
 parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
@@ -28,8 +28,7 @@
 apalache_jar_path = normpath(join(args.apalache_path, 'lib', 'apalache.jar'))
 tlaps_modules = normpath(args.tlapm_lib_path)
 community_modules = normpath(args.community_modules_jar_path)
-manifest_path = normpath(args.manifest_path)
-examples_root = dirname(manifest_path)
+examples_root = args.examples_root
 skip_modules = args.skip
 only_modules = args.only
 enable_assertions = args.enable_assertions
@@ -64,12 +63,12 @@ def parse_module(path):
         logging.error(output)
         return False
 
-manifest = tla_utils.load_json(manifest_path)
+manifest = tla_utils.load_all_manifests(examples_root)
 
 # List of all modules to parse and whether they should use TLAPS imports
 modules = [
     tla_utils.from_cwd(examples_root, module['path'])
-    for spec in manifest['specifications']
+    for spec in manifest
     for module in spec['modules']
         if module['path'] not in skip_modules
         and (only_modules == [] or module['path'] in only_modules)

.github/scripts/smoke_test_large_models.py

@@ -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')
@@ -27,8 +27,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
@@ -80,11 +79,11 @@ def check_model(module, model):
 
 logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)
 
-manifest = tla_utils.load_json(manifest_path)
+manifest = tla_utils.load_all_manifests(examples_root)
 
 large_models = [
     (module, model)
-    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/translate_pluscal.py

@@ -13,7 +13,7 @@
 
 parser = ArgumentParser(description='Run PlusCal translation on all modules.')
 parser.add_argument('--tools_jar_path', help='Path to the tla2tools.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 .tla modules to skip converting', required=False, default=[])
 parser.add_argument('--only', nargs='+', help='If provided, only convert models in this space-separated list', required=False, default=[])
 parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
@@ -23,18 +23,17 @@
 logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)
 
 tools_path = normpath(args.tools_jar_path)
-manifest_path = normpath(args.manifest_path)
-examples_root = dirname(manifest_path)
+examples_root = args.examples_root
 skip_modules = args.skip
 only_modules = args.only
 enable_assertions = args.enable_assertions
 
-manifest = tla_utils.load_json(manifest_path)
+manifest = tla_utils.load_all_manifests(examples_root)
 
 # List of all modules to translate
 modules = [
     tla_utils.from_cwd(examples_root, module['path'])
-    for spec in manifest['specifications']
+    for spec in manifest
     for module in spec['modules']
         if 'pluscal' in module['features']
         and module['path'] not in skip_modules

.github/scripts/unicode_conversion.py

@@ -13,7 +13,7 @@
 
 parser = ArgumentParser(description='Converts all TLA+ modules from ASCII to Unicode or vice-versa.')
 parser.add_argument('--tlauc_path', help='Path to the TLAUC executable', 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('--to_ascii', help='Convert to ASCII instead of Unicode', action='store_true')
 parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip converting', required=False, default=[])
 parser.add_argument('--only', nargs='+', help='If provided, only convert models in this space-separated list', required=False, default=[])
@@ -24,17 +24,16 @@
 
 tlauc_path = normpath(args.tlauc_path)
 to_ascii = args.to_ascii
-manifest_path = normpath(args.manifest_path)
-examples_root = dirname(manifest_path)
+examples_root = args.examples_root
 skip_modules = args.skip
 only_modules = args.only
 
-manifest = tla_utils.load_json(manifest_path)
+manifest = tla_utils.load_all_manifests(examples_root)
 
 # List of all modules to convert
 modules = [
     tla_utils.from_cwd(examples_root, module['path'])
-    for spec in manifest['specifications']
+    for spec in manifest
     for module in spec['modules']
         if module['path'] not in skip_modules
         and (only_modules == [] or module['path'] in only_modules)

.github/scripts/unicode_number_set_shim.py

@@ -110,14 +110,13 @@ def write_module(examples_root, module_path, module_bytes):
 
 if __name__ == '__main__':
     parser = ArgumentParser(description='Adds ℕ/ℤ/ℝ Unicode number set shim definitions to modules as needed.')
-    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', required=False, default=[])
     parser.add_argument('--only', nargs='+', help='If provided, only modify models in this space-separated list', required=False, default=[])
     args = parser.parse_args()
 
-    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
 
@@ -127,7 +126,7 @@ def write_module(examples_root, module_path, module_bytes):
 
     modules = [
         module['path']
-        for spec in manifest['specifications']
+        for spec in manifest
         for module in spec['modules']
             if module['path'] not in skip_modules
             and (only_modules == [] or module['path'] in only_modules)