Manifest: remove path, title, and description fields

In furtherance of tlaplus#171

The path property is now inherent in the location of the manifest.json
file, the README.md table can be the source of truth for the spec title,
and the spec description can live in the directory-specific README.md
file.

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

Author: ahelwer

.github/scripts/check_manifest_features.py

@@ -154,16 +154,10 @@ def check_features(parser, queries, manifest, examples_root):
     Validates every field of the manifest that can be validated.
     """
     success = True
-    for spec in manifest:
-        if spec['title'] == '':
-            success = False
-            logging.error(f'Spec {spec["path"]} does not have a title')
-        if spec['description'] == '':
-            success = False
-            logging.error(f'Spec {spec["path"]} does not have a description')
+    for path, spec in manifest:
         if not any(spec['authors']):
             success = False
-            logging.error(f'Spec {spec["path"]} does not have any listed authors')
+            logging.error(f'Spec {path} does not have any listed authors')
         for module in spec['modules']:
             module_path = module['path']
             tree, text, parse_err = tla_utils.parse_module(examples_root, parser, module_path)

.github/scripts/check_manifest_files.py

@@ -19,7 +19,7 @@
 examples_root = dirname(ci_ignore_path)
 manifest = tla_utils.load_all_manifests(examples_root)
 
-module_lists = [spec["modules"] for spec in manifest]
+module_lists = [spec["modules"] for path, 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

@@ -21,8 +21,8 @@
 examples_root = dirname(args.schema_path)
 schema = tla_utils.load_json(normpath(args.schema_path))
 failures = []
-for manifest in tla_utils.load_all_manifests(examples_root):
-    manifest_path = join(manifest['path'], "manifest.json")
+for path, manifest in tla_utils.load_all_manifests(examples_root):
+    manifest_path = join(path, 'manifest.json')
     try:
         validate(instance=manifest, schema=schema)
     except ValidationError as error:

.github/scripts/check_markdown_table.py

@@ -58,13 +58,13 @@ def from_markdown(record):
         record
     )
 
-def from_json(spec):
+def from_json(path, spec):
     '''
     Transforms JSON from the manifest into a normalized form.
     '''
     return TableRow(
-        spec['title'],
-        spec['path'],
+        '',
+        path,
         set(spec['authors']),
         'beginner' in spec['tags'],
         any([module for module in spec['modules'] if 'proof' in module['features']]),
@@ -87,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]])
+manifest_specs = dict([(record.path, record) for record in [from_json(path, spec) for path, spec in manifest]])
 
 # Checks that set of specs in manifest and table are equivalent
 success = True
@@ -107,18 +107,6 @@ def from_json(spec):
     if path in table_specs
 ]
 
-# Ensure spec names are identical
-different_names = [
-    (manifest_spec.path, manifest_spec.name, table_spec.name)
-    for (manifest_spec, table_spec) in specs
-    if manifest_spec.name != table_spec.name
-]
-if any(different_names):
-    success = False
-    print('ERROR: spec names in README.md table differ from manifest.json:')
-    for path, json, md in different_names:
-        print(f'Spec {path} has name {json} in manifest and {md} in README')
-
 # Ensure spec authors are identical
 different_authors = [
     (manifest_spec.path, manifest_spec.authors, table_spec.authors)

.github/scripts/check_proofs.py

@@ -27,7 +27,7 @@
 
 proof_module_paths = [
     module['path']
-    for spec in manifest
+    for path, 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

@@ -89,7 +89,7 @@ def check_model(module, model, expected_runtime):
 small_models = sorted(
     [
         (module, model, tla_utils.parse_timespan(model['runtime']))
-        for spec in manifest
+        for path, spec in manifest
         for module in spec['modules']
         for model in module['models']
             if model['size'] == 'small'

.github/scripts/generate_manifest.py

@@ -10,19 +10,11 @@
 from check_manifest_features import *
 import os
 from os.path import basename, dirname, join, normpath, relpath, splitext, isfile
-from pathlib import PureWindowsPath
 import glob
 import tla_utils
 import tree_sitter_tlaplus
 from tree_sitter import Language, Parser
 
-def to_posix(path):
-    """
-    Converts paths to normalized Posix format.
-    https://stackoverflow.com/q/75291812/2852699
-    """
-    return PureWindowsPath(normpath(path)).as_posix()
-
 def get_spec_dirs(examples_root, ignored_dirs):
     """
     Get all directories under the specifications dir, sorted alphabetically.
@@ -74,21 +66,18 @@ def generate_new_manifest(examples_root, spec_path, spec_name, parser, queries):
     Generate new manifest.json file for a given specification directory.
     """
     return {
-        'path': to_posix(spec_path),
-        'title': spec_name,
-        'description': '',
         'sources': [],
         'authors': [],
         'tags': [],
         'modules': [
             {
-                'path': to_posix(tla_path),
+                'path': tla_utils.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),
+                        'path': tla_utils.to_posix(cfg_path),
                         'runtime': 'unknown',
                         'size': 'unknown',
                         'mode': 'exhaustive search',
@@ -108,14 +97,14 @@ def get_old_manifest(spec_path):
     return tla_utils.load_json(old_manifest_path) if isfile(old_manifest_path) else None
 
 def integrate_spec_info(old_manifest, new_spec):
-    fields = ['title', 'description', 'authors', 'sources', 'tags']
+    fields = ['authors', 'sources', 'tags']
     for field in fields:
         new_spec[field] = old_manifest[field]
 
 def find_corresponding_module(old_module, new_spec):
     modules = [
         module for module in new_spec['modules']
-        if to_posix(module['path']) == to_posix(old_module['path'])
+        if tla_utils.to_posix(module['path']) == tla_utils.to_posix(old_module['path'])
     ]
     return modules[0] if any(modules) else None
 
@@ -127,7 +116,7 @@ def integrate_module_info(old_module, new_module):
 def find_corresponding_model(old_model, new_module):
     models = [
         model for model in new_module['models']
-        if to_posix(model['path']) == to_posix(old_model['path'])
+        if tla_utils.to_posix(model['path']) == tla_utils.to_posix(old_model['path'])
     ]
     return models[0] if any(models) else None
 

.github/scripts/parse_modules.py

@@ -68,7 +68,7 @@ def parse_module(path):
 # 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
+    for path, 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/record_model_state_space.py

@@ -79,7 +79,7 @@ def check_model(module, model):
 small_models = sorted(
     [
         (spec, module, model, tla_utils.parse_timespan(model['runtime']))
-        for spec in manifest
+        for path, spec in manifest
         for module in spec['modules']
         for model in module['models']
             if model['size'] == 'small'

.github/scripts/smoke_test_large_models.py

@@ -82,7 +82,7 @@ def check_model(module, model):
 
 large_models = [
     (module, model)
-    for spec in manifest
+    for path, spec in manifest
     for module in spec['modules']
     for model in module['models']
         if model['size'] != 'small'