|
| 1 | +""" |
| 2 | +Validates the spec table in README.md, ensuring it matches manifest.json. |
| 3 | +""" |
| 4 | + |
| 5 | +from argparse import ArgumentParser |
| 6 | +from dataclasses import dataclass |
| 7 | +from os.path import normpath |
| 8 | +from typing import Any, Set |
| 9 | +import tla_utils |
| 10 | +import mistletoe |
| 11 | +from mistletoe.block_token import Table |
| 12 | + |
| 13 | +@dataclass |
| 14 | +class TableRow: |
| 15 | + name : str |
| 16 | + path : str |
| 17 | + authors : Set[str] |
| 18 | + beginner : bool |
| 19 | + proof : bool |
| 20 | + pcal : bool |
| 21 | + tlc : bool |
| 22 | + apalache : bool |
| 23 | + underlying : Any |
| 24 | + |
| 25 | +columns = ['name', 'authors', 'beginner', 'proof', 'pcal', 'tlc', 'apalache'] |
| 26 | + |
| 27 | +def get_column(row, index): |
| 28 | + ''' |
| 29 | + Gets the cell of the given column in the given row. |
| 30 | + ''' |
| 31 | + return row.children[columns.index(index)].children[0] |
| 32 | + |
| 33 | +def is_column_empty(row, index): |
| 34 | + ''' |
| 35 | + Whether the given column cell is empty. |
| 36 | + ''' |
| 37 | + return not any(row.children[columns.index(index)].children) |
| 38 | + |
| 39 | +def get_link_text(link): |
| 40 | + ''' |
| 41 | + Gets the text in a markdown link. |
| 42 | + ''' |
| 43 | + return link.children[0].content |
| 44 | + |
| 45 | +def from_markdown(record): |
| 46 | + ''' |
| 47 | + Transforms a parsed markdown table row into a normalized form. |
| 48 | + ''' |
| 49 | + return TableRow( |
| 50 | + get_link_text(get_column(record, 'name')), |
| 51 | + get_column(record, 'name').target, |
| 52 | + set(name.strip() for name in get_column(record, 'authors').content.split(',')), |
| 53 | + not is_column_empty(record, 'beginner'), |
| 54 | + not is_column_empty(record, 'proof'), |
| 55 | + not is_column_empty(record, 'pcal'), |
| 56 | + not is_column_empty(record, 'tlc'), |
| 57 | + not is_column_empty(record, 'apalache'), |
| 58 | + record |
| 59 | + ) |
| 60 | + |
| 61 | +def from_json(spec): |
| 62 | + ''' |
| 63 | + Transforms JSON from the manifest into a normalized form. |
| 64 | + ''' |
| 65 | + return TableRow( |
| 66 | + spec['title'], |
| 67 | + spec['path'], |
| 68 | + set(spec['authors']), |
| 69 | + 'beginner' in spec['tags'], |
| 70 | + any([module for module in spec['modules'] if 'proof' in module['features']]), |
| 71 | + any([module for module in spec['modules'] if 'pluscal' in module['features']]), |
| 72 | + any([model for module in spec['modules'] for model in module['models'] if model['mode'] != 'symbolic']), |
| 73 | + any([model for module in spec['modules'] for model in module['models'] if model['mode'] == 'symbolic']), |
| 74 | + spec |
| 75 | + ) |
| 76 | + |
| 77 | +parser = ArgumentParser(description='Validates the spec table in README.md against the manifest.json.') |
| 78 | +parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True) |
| 79 | +parser.add_argument('--readme_path', help='Path to the tlaplus/examples README.md file', required=True) |
| 80 | +args = parser.parse_args() |
| 81 | + |
| 82 | +manifest = tla_utils.load_json(normpath(args.manifest_path)) |
| 83 | + |
| 84 | +readme = None |
| 85 | +with open(normpath(args.readme_path), 'r', encoding='utf-8') as readme_file: |
| 86 | + readme = mistletoe.Document(readme_file) |
| 87 | + |
| 88 | +spec_table = next((child for child in readme.children if isinstance(child, Table))) |
| 89 | + |
| 90 | +table_specs = dict([(record.path, record) for record in [from_markdown(node) for node in spec_table.children]]) |
| 91 | +manifest_specs = dict([(record.path, record) for record in [from_json(spec) for spec in manifest['specifications']]]) |
| 92 | + |
| 93 | +# Checks that set of specs in manifest and table are equivalent |
| 94 | +success = True |
| 95 | +specs_not_in_table = manifest_specs.keys() - table_specs.keys() |
| 96 | +if any(specs_not_in_table): |
| 97 | + success = False |
| 98 | + print('ERROR: specs in manifest.json missing from README.md table:\n' + '\n'.join(specs_not_in_table)) |
| 99 | +specs_not_in_manifest = table_specs.keys() - manifest_specs.keys() |
| 100 | +if any(specs_not_in_manifest): |
| 101 | + success = False |
| 102 | + print('ERROR: specs in README.md table missing from manifest.json:\n' + '\n'.join(specs_not_in_manifest)) |
| 103 | + |
| 104 | +# Join the spec records together for comparison |
| 105 | +specs = [ |
| 106 | + (manifest_spec, table_specs[path]) |
| 107 | + for (path, manifest_spec) in manifest_specs.items() |
| 108 | + if path in table_specs |
| 109 | +] |
| 110 | + |
| 111 | +# Ensure spec names are identical |
| 112 | +different_names = [ |
| 113 | + (manifest_spec.path, manifest_spec.name, table_spec.name) |
| 114 | + for (manifest_spec, table_spec) in specs |
| 115 | + if manifest_spec.name != table_spec.name |
| 116 | +] |
| 117 | +if any(different_names): |
| 118 | + success = False |
| 119 | + print('ERROR: spec names in README.md table differ from manifest.json:') |
| 120 | + for path, json, md in different_names: |
| 121 | + print(f'Spec {path} has name {json} in manifest and {md} in README') |
| 122 | + |
| 123 | +# Ensure spec authors are identical |
| 124 | +different_authors = [ |
| 125 | + (manifest_spec.path, manifest_spec.authors, table_spec.authors) |
| 126 | + for (manifest_spec, table_spec) in specs |
| 127 | + if manifest_spec.authors != table_spec.authors |
| 128 | +] |
| 129 | +if any(different_authors): |
| 130 | + success = False |
| 131 | + print('ERROR: spec author(s) in README.md table differ from manifest.json:') |
| 132 | + for path, json, md in different_authors: |
| 133 | + print(f'Spec {path} has author(s) {json} in manifest.json and {md} in README.md') |
| 134 | + |
| 135 | +# Ensure Beginner flag is correct |
| 136 | +different_beginner_flag = [ |
| 137 | + (manifest_spec.path, manifest_spec.beginner, table_spec.beginner) |
| 138 | + for (manifest_spec, table_spec) in specs |
| 139 | + if manifest_spec.beginner != table_spec.beginner |
| 140 | +] |
| 141 | +if any(different_beginner_flag): |
| 142 | + success = False |
| 143 | + print('ERROR: Beginner flags in README.md table differ from tags in manifest.json:') |
| 144 | + for path, json, md in different_beginner_flag: |
| 145 | + print(f'Spec {path} is missing a Beginner ' + ('tag in manifest.json' if md else 'flag in README.md')) |
| 146 | + |
| 147 | +# Ensure TLAPS proof flag is correct |
| 148 | +different_tlaps_flag = [ |
| 149 | + (manifest_spec.path, manifest_spec.proof, table_spec.proof) |
| 150 | + for (manifest_spec, table_spec) in specs |
| 151 | + if manifest_spec.proof != table_spec.proof |
| 152 | +] |
| 153 | +if any(different_tlaps_flag): |
| 154 | + success = False |
| 155 | + print('ERROR: Proof flags in README.md table differ from features in manifest.json:') |
| 156 | + for path, json, md in different_tlaps_flag: |
| 157 | + print(f'Spec {path} ' + ('incorrectly has' if md else 'is missing') + ' a proof flag in README.md table') |
| 158 | + |
| 159 | +# Ensure PlusCal flag is correct |
| 160 | +different_pcal_flag = [ |
| 161 | + (manifest_spec.path, manifest_spec.pcal, table_spec.pcal) |
| 162 | + for (manifest_spec, table_spec) in specs |
| 163 | + if manifest_spec.pcal != table_spec.pcal |
| 164 | +] |
| 165 | +if any(different_pcal_flag): |
| 166 | + success = False |
| 167 | + print('ERROR: PlusCal flags in README.md table differ from features in manifest.json:') |
| 168 | + for path, json, md in different_pcal_flag: |
| 169 | + print(f'Spec {path} ' + ('incorrectly has' if md else 'is missing') + ' a PlusCal flag in README.md table') |
| 170 | + |
| 171 | +# Ensure TLC flag is correct |
| 172 | +different_tlc_flag = [ |
| 173 | + (manifest_spec.path, manifest_spec.tlc, table_spec.tlc) |
| 174 | + for (manifest_spec, table_spec) in specs |
| 175 | + if manifest_spec.tlc != table_spec.tlc |
| 176 | +] |
| 177 | +if any(different_tlc_flag): |
| 178 | + success = False |
| 179 | + print('ERROR: TLC Model flags in README.md table differ from model records in manifest.json:') |
| 180 | + for path, json, md in different_tlc_flag: |
| 181 | + print(f'Spec {path} ' + ('incorrectly has' if md else 'is missing') + ' a TLC Model flag in README.md table') |
| 182 | + |
| 183 | +# Ensure Apalache flag is correct |
| 184 | +different_apalache_flag = [ |
| 185 | + (manifest_spec.path, manifest_spec.apalache, table_spec.apalache) |
| 186 | + for (manifest_spec, table_spec) in specs |
| 187 | + if manifest_spec.apalache != table_spec.apalache |
| 188 | +] |
| 189 | +if any(different_apalache_flag): |
| 190 | + success = False |
| 191 | + print('ERROR: Apalache Model flags in README.md table differ from model records in manifest.json:') |
| 192 | + for path, json, md in different_tlc_flag: |
| 193 | + print(f'Spec {path} ' + ('incorrectly has' if md else 'is missing') + ' an Apalache Model flag in README.md table') |
| 194 | + |
| 195 | +if success: |
| 196 | + print('SUCCESS: manifest.json concords with README.md table') |
| 197 | + exit(0) |
| 198 | +else: |
| 199 | + print('ERROR: differences exist between manifest.json and README.md table; see above error messages') |
| 200 | + exit(1) |
| 201 | + |
0 commit comments