Skip to content

Commit 083bf32

Browse files
ahelwerahelwer
committed
Documented scripts
Signed-off-by: Andrew Helwer <[email protected]>
1 parent 785f70f commit 083bf32

File tree

4 files changed

+44
-16
lines changed

4 files changed

+44
-16
lines changed

‎.github/scripts/check_markdown_table.py

Lines changed: 17 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
"""
2-
Validates the spec table in README.md.
2+
Validates the spec table in README.md, ensuring it matches manifest.json.
33
"""
44

55
from argparse import ArgumentParser
@@ -9,7 +9,6 @@
99
import tla_utils
1010
import mistletoe
1111
from mistletoe.block_token import Table
12-
from mistletoe.markdown_renderer import MarkdownRenderer
1312

1413
@dataclass
1514
class TableRow:
@@ -26,15 +25,27 @@ class TableRow:
2625
columns = ['name', 'authors', 'beginner', 'proof', 'pcal', 'tlc', 'apalache']
2726

2827
def get_column(row, index):
28+
'''
29+
Gets the cell of the given column in the given row.
30+
'''
2931
return row.children[columns.index(index)].children[0]
3032

3133
def is_column_empty(row, index):
34+
'''
35+
Whether the given column cell is empty.
36+
'''
3237
return not any(row.children[columns.index(index)].children)
3338

3439
def get_link_text(link):
40+
'''
41+
Gets the text in a markdown link.
42+
'''
3543
return link.children[0].content
3644

3745
def from_markdown(record):
46+
'''
47+
Transforms a parsed markdown table row into a normalized form.
48+
'''
3849
return TableRow(
3950
get_link_text(get_column(record, 'name')),
4051
get_column(record, 'name').target,
@@ -48,6 +59,9 @@ def from_markdown(record):
4859
)
4960

5061
def from_json(spec):
62+
'''
63+
Transforms JSON from the manifest into a normalized form.
64+
'''
5165
return TableRow(
5266
spec['title'],
5367
spec['path'],
@@ -60,7 +74,7 @@ def from_json(spec):
6074
spec
6175
)
6276

63-
parser = ArgumentParser(description='Formats or modifies the spec table in README.md.')
77+
parser = ArgumentParser(description='Validates the spec table in README.md against the manifest.json.')
6478
parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True)
6579
parser.add_argument('--readme_path', help='Path to the tlaplus/examples README.md file', required=True)
6680
args = parser.parse_args()

‎.github/scripts/format_markdown_table.py

Lines changed: 15 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,13 @@
11
"""
2-
Format or modify the spec table in README.md.
2+
Format or modify the spec table in README.md. This is a utility script kept
3+
around for occasional modifications to the README.md table(s), such as
4+
swapping/deleting columns or transforming each row element. By doing a simple
5+
round-trip without any transformation the tables will also be formatted
6+
nicely.
37
"""
48

59
from argparse import ArgumentParser
610
from os.path import normpath
7-
import re
811
import mistletoe
912
from mistletoe.block_token import Table
1013
from mistletoe.markdown_renderer import MarkdownRenderer
@@ -13,14 +16,16 @@
1316
parser.add_argument('--readme_path', help='Path to the tlaplus/examples README.md file', required=True)
1417
args = parser.parse_args()
1518

16-
# Read & parse README.md file
1719
readme = None
1820
with open(normpath(args.readme_path), 'r', encoding='utf-8') as readme_file:
1921
readme = mistletoe.Document(readme_file)
2022

2123
columns = ['name', 'authors', 'beginner', 'proof', 'tlc', 'pcal', 'apalache']
2224

2325
def get_column(row, index):
26+
'''
27+
Gets the cell of the given column in the given row.
28+
'''
2429
return row.children[columns.index(index)].children[0]
2530

2631
def remove_column(table, col_index):
@@ -53,11 +58,14 @@ def swap_columns(table, first_col_index, second_col_index):
5358
row.children[second], row.children[first] = row.children[first], row.children[second]
5459

5560

56-
def format_table(readme):
57-
table = next((child for child in readme.children if isinstance(child, Table)))
58-
swap_columns(table, 'pcal', 'tlc')
61+
def format_table(table):
62+
'''
63+
All table transformations should go here.
64+
'''
65+
return
5966

60-
format_table(readme)
67+
table = next((child for child in readme.children if isinstance(child, Table)))
68+
format_table(table)
6169

6270
# Write formatted markdown to README.md
6371
with open(normpath(args.readme_path), 'w', encoding='utf-8') as readme_file:

‎.github/workflows/CI.yml

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -134,6 +134,11 @@ jobs:
134134
python $SCRIPT_DIR/check_manifest_features.py \
135135
--manifest_path manifest.json \
136136
--ts_path deps/tree-sitter-tlaplus
137+
- name: Check README spec table
138+
run: |
139+
python $SCRIPT_DIR/check_markdown_table.py \
140+
--manifest_path manifest.json \
141+
--readme_path README.md
137142
- name: Parse all modules
138143
run: |
139144
python $SCRIPT_DIR/parse_modules.py \

‎README.md

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -9,14 +9,14 @@ It serves as:
99
- a collection of case studies in the application of formal specification in TLA<sup>+</sup>
1010

1111
All TLA<sup>+</sup> specs can be found in the [`specifications`](specifications) directory.
12-
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.
13-
Beginner-friendly specs can be found by searching for the "beginner" tag in that file.
14-
Similarly, PlusCal specs can be found by searching for the "pluscal" feature, or "proof" for specs with proofs.
15-
These details & others are mirrored in the table below.
12+
The table below lists all specs and their features, such as whether they are suitable for beginners or use PlusCal.
13+
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.
14+
Its schema is [`manifest-schema.json`](manifest-schema.json).
15+
All specs in this repository are subject to CI validation to ensure quality.
1616

1717
## Examples Included Here
1818
Here is a list of specs included in this repository, with links to the relevant directory and flags for various features:
19-
| Name | Authors | Beginner | TLAPS Proof | PlusCal | TLC Model | Apalache |
19+
| Name | Author(s) | Beginner | TLAPS Proof | PlusCal | TLC Model | Apalache |
2020
| --------------------------------------------------------------------------------------------------- | ------------------------------------------ | :------: | :---------: | :-----: | :-------: | :------: |
2121
| [Learn TLA⁺ Proofs](specifications/LearnProofs) | Andrew Helwer | ✔ | ✔ | ✔ | ✔ | |
2222
| [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
8888
Here is a list of specs stored in locations outside this repository, including submodules.
8989
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.
9090
Ideally these will be moved into this repo over time.
91-
| Name | Description | Authors | TLAPS Proof? | TLC Model? | PlusCal? | Apalache? |
91+
| Name | Description | Author(s) | TLAPS Proof? | TLC Model? | PlusCal? | Apalache? |
9292
| --------------------------------------------------------------------------------------------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------ | :----------: | :--------: | :------: | :-------: |
9393
| [2PCwithBTM](specifications/2PCwithBTM) | A modified version of P2TCommit (Gray & Lamport, 2006) | Murat Demirbas | | ✔ | ✔ | |
9494
| [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:
151151
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.
152152
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
153153
1. Add an entry to the table of specs included in this repo, summarizing your spec and its attributes
154+
154155
## Adding Spec to Continuous Integration
155156
To combat bitrot, it is important to add your spec and model to the continuous integration system.
156157
To do this, you'll have to update the [`manifest.json`](manifest.json) file with machine-readable records of your spec files.

0 commit comments

Comments
 (0)