Validate README.md markdown table in CI

.github/scripts/check_markdown_table.py

@@ -0,0 +1,201 @@
+"""
+Validates the spec table in README.md, ensuring it matches manifest.json.
+"""
+
+from argparse import ArgumentParser
+from dataclasses import dataclass
+from os.path import normpath
+from typing import Any, Set
+import tla_utils
+import mistletoe
+from mistletoe.block_token import Table
+
+@dataclass
+class TableRow:
+    name        : str
+    path        : str
+    authors     : Set[str]
+    beginner    : bool
+    proof       : bool
+    pcal        : bool
+    tlc         : bool
+    apalache    : bool
+    underlying  : Any
+
+columns = ['name', 'authors', 'beginner', 'proof', 'pcal', 'tlc', 'apalache']
+
+def get_column(row, index):
+    '''
+    Gets the cell of the given column in the given row.
+    '''
+    return row.children[columns.index(index)].children[0]
+
+def is_column_empty(row, index):
+    '''
+    Whether the given column cell is empty.
+    '''
+    return not any(row.children[columns.index(index)].children)
+
+def get_link_text(link):
+    '''
+    Gets the text in a markdown link.
+    '''
+    return link.children[0].content
+
+def from_markdown(record):
+    '''
+    Transforms a parsed markdown table row into a normalized form.
+    '''
+    return TableRow(
+        get_link_text(get_column(record, 'name')),
+        get_column(record, 'name').target,
+        set(name.strip() for name in get_column(record, 'authors').content.split(',')),
+        not is_column_empty(record, 'beginner'),
+        not is_column_empty(record, 'proof'),
+        not is_column_empty(record, 'pcal'),
+        not is_column_empty(record, 'tlc'),
+        not is_column_empty(record, 'apalache'),
+        record
+    )
+
+def from_json(spec):
+    '''
+    Transforms JSON from the manifest into a normalized form.
+    '''
+    return TableRow(
+        spec['title'],
+        spec['path'],
+        set(spec['authors']),
+        'beginner' in spec['tags'],
+        any([module for module in spec['modules'] if 'proof' in module['features']]),
+        any([module for module in spec['modules'] if 'pluscal' in module['features']]),
+        any([model for module in spec['modules'] for model in module['models'] if model['mode'] != 'symbolic']),
+        any([model for module in spec['modules'] for model in module['models'] if model['mode'] == 'symbolic']),
+        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))
+
+readme = None
+with open(normpath(args.readme_path), 'r', encoding='utf-8') as readme_file:
+    readme = mistletoe.Document(readme_file)
+
+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']]])
+
+# Checks that set of specs in manifest and table are equivalent
+success = True
+specs_not_in_table = manifest_specs.keys() - table_specs.keys()
+if any(specs_not_in_table):
+    success = False
+    print('ERROR: specs in manifest.json missing from README.md table:\n' + '\n'.join(specs_not_in_table))
+specs_not_in_manifest = table_specs.keys() - manifest_specs.keys()
+if any(specs_not_in_manifest):
+    success = False
+    print('ERROR: specs in README.md table missing from manifest.json:\n' + '\n'.join(specs_not_in_manifest))
+
+# Join the spec records together for comparison
+specs = [
+    (manifest_spec, table_specs[path])
+    for (path, manifest_spec) in manifest_specs.items()
+    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)
+    for (manifest_spec, table_spec) in specs
+    if manifest_spec.authors != table_spec.authors
+]
+if any(different_authors):
+    success = False
+    print('ERROR: spec author(s) in README.md table differ from manifest.json:')
+    for path, json, md in different_authors:
+        print(f'Spec {path} has author(s) {json} in manifest.json and {md} in README.md')
+
+# Ensure Beginner flag is correct
+different_beginner_flag = [
+    (manifest_spec.path, manifest_spec.beginner, table_spec.beginner)
+    for (manifest_spec, table_spec) in specs
+    if manifest_spec.beginner != table_spec.beginner
+]
+if any(different_beginner_flag):
+    success = False
+    print('ERROR: Beginner flags in README.md table differ from tags in manifest.json:')
+    for path, json, md in different_beginner_flag:
+        print(f'Spec {path} is missing a Beginner ' + ('tag in manifest.json' if md else 'flag in README.md'))
+
+# Ensure TLAPS proof flag is correct
+different_tlaps_flag = [
+    (manifest_spec.path, manifest_spec.proof, table_spec.proof)
+    for (manifest_spec, table_spec) in specs
+    if manifest_spec.proof != table_spec.proof
+]
+if any(different_tlaps_flag):
+    success = False
+    print('ERROR: Proof flags in README.md table differ from features in manifest.json:')
+    for path, json, md in different_tlaps_flag:
+        print(f'Spec {path} ' + ('incorrectly has' if md else 'is missing') + ' a proof flag in README.md table')
+
+# Ensure PlusCal flag is correct
+different_pcal_flag = [
+    (manifest_spec.path, manifest_spec.pcal, table_spec.pcal)
+    for (manifest_spec, table_spec) in specs
+    if manifest_spec.pcal != table_spec.pcal
+]
+if any(different_pcal_flag):
+    success = False
+    print('ERROR: PlusCal flags in README.md table differ from features in manifest.json:')
+    for path, json, md in different_pcal_flag:
+        print(f'Spec {path} ' + ('incorrectly has' if md else 'is missing') + ' a PlusCal flag in README.md table')
+
+# Ensure TLC flag is correct
+different_tlc_flag = [
+    (manifest_spec.path, manifest_spec.tlc, table_spec.tlc)
+    for (manifest_spec, table_spec) in specs
+    if manifest_spec.tlc != table_spec.tlc
+]
+if any(different_tlc_flag):
+    success = False
+    print('ERROR: TLC Model flags in README.md table differ from model records in manifest.json:')
+    for path, json, md in different_tlc_flag:
+        print(f'Spec {path} ' + ('incorrectly has' if md else 'is missing') + ' a TLC Model flag in README.md table')
+
+# Ensure Apalache flag is correct
+different_apalache_flag = [
+    (manifest_spec.path, manifest_spec.apalache, table_spec.apalache)
+    for (manifest_spec, table_spec) in specs
+    if manifest_spec.apalache != table_spec.apalache
+]
+if any(different_apalache_flag):
+    success = False
+    print('ERROR: Apalache Model flags in README.md table differ from model records in manifest.json:')
+    for path, json, md in different_tlc_flag:
+        print(f'Spec {path} ' + ('incorrectly has' if md else 'is missing') + ' an Apalache Model flag in README.md table')
+
+if success:
+    print('SUCCESS: manifest.json concords with README.md table')
+    exit(0)
+else:
+    print('ERROR: differences exist between manifest.json and README.md table; see above error messages')
+    exit(1)
+

.github/scripts/format_markdown_table.py

@@ -0,0 +1,74 @@
+"""
+Format or modify the spec table in README.md. This is a utility script kept
+around for occasional modifications to the README.md table(s), such as
+swapping/deleting columns or transforming each row element. By doing a simple
+round-trip without any transformation the tables will also be formatted
+nicely.
+"""
+
+from argparse import ArgumentParser
+from os.path import normpath
+import mistletoe
+from mistletoe.block_token import Table
+from mistletoe.markdown_renderer import MarkdownRenderer
+
+parser = ArgumentParser(description='Formats or modifies the spec table in README.md.')
+parser.add_argument('--readme_path', help='Path to the tlaplus/examples README.md file', required=True)
+args = parser.parse_args()
+
+readme = None
+with open(normpath(args.readme_path), 'r', encoding='utf-8') as readme_file:
+    readme = mistletoe.Document(readme_file)
+
+columns = ['name', 'authors', 'beginner', 'proof', 'tlc', 'pcal', 'apalache']
+
+def get_column(row, index):
+    '''
+    Gets the cell of the given column in the given row.
+    '''
+    return row.children[columns.index(index)].children[0]
+
+def remove_column(table, col_index):
+    '''
+    Removes the column of the given index from the table.
+    '''
+    index = columns.index(col_index)
+    table.header.children.pop(index)
+    table.column_align.pop(index)
+    for row in table.children:
+        row.children.pop(index)
+
+def blank_column(table, col_index):
+    '''
+    Removes all data in the given column.
+    '''
+    index = columns.index(col_index)
+    for row in table.children:
+        row.children[index].children = []
+
+def swap_columns(table, first_col_index, second_col_index):
+    '''
+    Swaps two columns in a table.
+    '''
+    first = columns.index(first_col_index)
+    second = columns.index(second_col_index)
+    table.header.children[second], table.header.children[first] = table.header.children[first], table.header.children[second]
+    table.column_align[second], table.column_align[first] = table.column_align[first], table.column_align[second]
+    for row in table.children:
+        row.children[second], row.children[first] = row.children[first], row.children[second]
+
+
+def format_table(table):
+    '''
+    All table transformations should go here.
+    '''
+    return
+
+table = next((child for child in readme.children if isinstance(child, Table)))
+format_table(table)
+
+# Write formatted markdown to README.md
+with open(normpath(args.readme_path), 'w', encoding='utf-8') as readme_file:
+    with MarkdownRenderer() as renderer:
+        readme_file.write(renderer.render(readme))
+

.github/scripts/requirements.txt

@@ -1,3 +1,4 @@
-jsonschema == 4.17.3
-tree-sitter==0.20.1
+jsonschema == 4.20.0
+tree-sitter==0.20.4
+mistletoe==1.2.1
 

.github/workflows/CI.yml

@@ -134,6 +134,11 @@ jobs:
           python $SCRIPT_DIR/check_manifest_features.py \
             --manifest_path manifest.json               \
             --ts_path deps/tree-sitter-tlaplus
+      - name: Check README spec table
+        run: |
+          python $SCRIPT_DIR/check_markdown_table.py  \
+            --manifest_path manifest.json             \
+            --readme_path README.md
       - name: Parse all modules
         run: |
           python $SCRIPT_DIR/parse_modules.py                       \