Documented scripts

Signed-off-by: Andrew Helwer <[email protected]>
tlaplus · Jan 17, 2024 · 083bf32 · 083bf32
1 parent 785f70f
commit 083bf32
Show file tree

Hide file tree

Showing 4 changed files with 44 additions and 16 deletions.
diff --git a/.github/scripts/check_markdown_table.py b/.github/scripts/check_markdown_table.py
@@ -1,5 +1,5 @@
 """
-Validates the spec table in README.md.
+Validates the spec table in README.md, ensuring it matches manifest.json.
 """
 
 from argparse import ArgumentParser
@@ -9,7 +9,6 @@
 import tla_utils
 import mistletoe
 from mistletoe.block_token import Table
-from mistletoe.markdown_renderer import MarkdownRenderer
 
 @dataclass
 class TableRow:
@@ -26,15 +25,27 @@ class TableRow:
 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,
@@ -48,6 +59,9 @@ def from_markdown(record):
     )
 
 def from_json(spec):
+    '''
+    Transforms JSON from the manifest into a normalized form.
+    '''
     return TableRow(
         spec['title'],
         spec['path'],
@@ -60,7 +74,7 @@ def from_json(spec):
         spec
     )
 
-parser = ArgumentParser(description='Formats or modifies the spec table in README.md.')
+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()

diff --git a/.github/scripts/format_markdown_table.py b/.github/scripts/format_markdown_table.py
@@ -1,10 +1,13 @@
 """
-Format or modify the spec table in README.md.
+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 re
 import mistletoe
 from mistletoe.block_token import Table
 from mistletoe.markdown_renderer import MarkdownRenderer
@@ -13,14 +16,16 @@
 parser.add_argument('--readme_path', help='Path to the tlaplus/examples README.md file', required=True)
 args = parser.parse_args()
 
-# Read & parse README.md file
 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):
@@ -53,11 +58,14 @@ def swap_columns(table, first_col_index, second_col_index):
         row.children[second], row.children[first] = row.children[first], row.children[second]
 
 
-def format_table(readme):
-    table = next((child for child in readme.children if isinstance(child, Table)))
-    swap_columns(table, 'pcal', 'tlc')
+def format_table(table):
+    '''
+    All table transformations should go here.
+    '''
+    return
 
-format_table(readme)
+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:

diff --git a/.github/workflows/CI.yml b/.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                       \

diff --git a/README.md b/README.md
@@ -9,14 +9,14 @@ It serves as:
 - a collection of case studies in the application of formal specification in TLA<sup>+</sup>
 
 All TLA<sup>+</sup> specs can be found in the [`specifications`](specifications) directory.
-A central manifest of specs with descriptions and accounts of their various models and features can be found in the [`manifest.json`](manifest.json) file.
-Beginner-friendly specs can be found by searching for the "beginner" tag in that file.
-Similarly, PlusCal specs can be found by searching for the "pluscal" feature, or "proof" for specs with proofs.
-These details & others are mirrored in the table below.
+The table below lists all specs and their features, such as whether they are suitable for beginners or use PlusCal.
+The [`manifest.json`](manifest.json) file is the source of truth for this table, and is a detailed human- & machine-readable description of the specs & their models.
+Its schema is [`manifest-schema.json`](manifest-schema.json).
+All specs in this repository are subject to CI validation to ensure quality.
 
 ## Examples Included Here
 Here is a list of specs included in this repository, with links to the relevant directory and flags for various features:
-| Name                                                                                                | Authors                                    | Beginner | TLAPS Proof | PlusCal | TLC Model | Apalache |
+| Name                                                                                                | Author(s)                                  | Beginner | TLAPS Proof | PlusCal | TLC Model | Apalache |
 | --------------------------------------------------------------------------------------------------- | ------------------------------------------ | :------: | :---------: | :-----: | :-------: | :------: |
 | [Learn TLA⁺ Proofs](specifications/LearnProofs)                                                     | Andrew Helwer                              |    ✔     |      ✔      |    ✔    |     ✔     |          |
 | [Teaching Concurrency](specifications/TeachingConcurrency)                                          | Leslie Lamport                             |    ✔     |      ✔      |    ✔    |           |          |
@@ -88,7 +88,7 @@ Here is a list of specs included in this repository, with links to the relevant
 Here is a list of specs stored in locations outside this repository, including submodules.
 They are not covered by CI testing so it is possible they contain errors, the reported details are incorrect, or they are no longer available.
 Ideally these will be moved into this repo over time.
-| Name                                                                                                                              | Description                                                                                                                               | Authors                                                                        | TLAPS Proof? | TLC Model? | PlusCal? | Apalache? |
+| Name                                                                                                                              | Description                                                                                                                               | Author(s)                                                                      | TLAPS Proof? | TLC Model? | PlusCal? | Apalache? |
 | --------------------------------------------------------------------------------------------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------ | :----------: | :--------: | :------: | :-------: |
 | [2PCwithBTM](specifications/2PCwithBTM)                                                                                           | A modified version of P2TCommit (Gray & Lamport, 2006)                                                                                    | Murat Demirbas                                                                 |              |     ✔      |    ✔     |           |
 | [802.16](specifications/802.16)                                                                                                   | IEEE 802.16 WiMAX Protocols                                                                                                               | Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, and Hai Zhou |              |     ✔      |          |           |
@@ -151,6 +151,7 @@ Follow these instructions:
 1. Ensure name of each `.cfg` file matches the `.tla` file it models, or has its name as a prefix; for example `SpecName.tla` can have the models `SpecName.cfg` and `SpecNameLiveness.cfg`, etc.
 1. Consider including a `README.md` in the spec directory explaining the significance of the spec with links to any relevant websites or publications, or integrate this info as comments in the spec itself
 1. Add an entry to the table of specs included in this repo, summarizing your spec and its attributes
+
 ## Adding Spec to Continuous Integration
 To combat bitrot, it is important to add your spec and model to the continuous integration system.
 To do this, you'll have to update the [`manifest.json`](manifest.json) file with machine-readable records of your spec files.