Skip to content

Commit 0e018bc

Browse files
ahelwerahelwer
committed
CI: remove community modules details from manifest
Signed-off-by: Andrew Helwer <[email protected]>
1 parent 9ece37b commit 0e018bc

File tree

83 files changed

+14
-481
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

83 files changed

+14
-481
lines changed

‎.github/scripts/check_manifest_features.py‎

Lines changed: 2 additions & 85 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@
22
This script performs whatever validations are possible on the metadata in
33
the manifest.json files. Prominent checks include:
44
* .tla files containing pluscal or proofs are marked as such
5-
* .tla files importing community modules have those modules listed
6-
* Human-written fields are not empty
5+
* Model state counts are applicable to the model type
6+
* Human-written fields such as authorship are not empty
77
"""
88

99
from argparse import ArgumentParser
@@ -75,81 +75,6 @@ def get_module_features(examples_root, path, parser, queries):
7575
tree, _, _ = tla_utils.parse_module(examples_root, parser, path)
7676
return get_tree_features(tree, queries)
7777

78-
# All the standard modules available when using TLC
79-
tlc_modules = {
80-
'Bags',
81-
'FiniteSets',
82-
'Integers',
83-
'Json',
84-
'Naturals',
85-
'Randomization',
86-
'RealTime',
87-
'Reals',
88-
'Sequences',
89-
'TLC',
90-
'TLCExt',
91-
'Toolbox',
92-
'Apalache'
93-
}
94-
95-
# All the standard modules available when using TLAPS
96-
tlaps_modules = {
97-
'BagsTheorems',
98-
'FiniteSetTheorems',
99-
'FunctionForkTheorems',
100-
'FunctionsFork',
101-
'NaturalsInduction',
102-
'SequencesExtForkTheorems',
103-
'SequenceTheorems',
104-
'TLAPS',
105-
'WellFoundedInduction'
106-
}
107-
108-
# Modules overloaded by TLAPS; some of these are ordinarily imported as
109-
# community modules.
110-
tlaps_module_overloads = {
111-
'Bags',
112-
'FiniteSets',
113-
'Functions',
114-
'RealTime',
115-
'SequencesExt'
116-
}
117-
118-
def get_community_imports(examples_root, tree, text, dir, has_proof, queries):
119-
"""
120-
Gets all modules imported by a given .tla file that are not standard
121-
modules or modules in the same file or directory. Community module
122-
imports are what's left.
123-
"""
124-
imports = set(
125-
[
126-
tla_utils.node_to_string(text, node)
127-
for node in tla_utils.all_nodes_of(queries.imports.captures(tree.root_node))
128-
]
129-
)
130-
modules_in_file = set(
131-
[
132-
tla_utils.node_to_string(text, node)
133-
for node in tla_utils.all_nodes_of(queries.module_names.captures(tree.root_node))
134-
]
135-
)
136-
imports = (
137-
imports
138-
- modules_in_file
139-
- tlc_modules
140-
- tlaps_modules
141-
- get_module_names_in_dir(examples_root, dir)
142-
)
143-
return imports - tlaps_module_overloads if has_proof else imports
144-
145-
def get_community_module_imports(examples_root, parser, path, queries):
146-
"""
147-
Gets all community modules imported by the .tla file at the given path.
148-
"""
149-
tree, text, _ = tla_utils.parse_module(examples_root, parser, path)
150-
has_proof = 'proof' in get_tree_features(tree, queries)
151-
return get_community_imports(examples_root, tree, text, dirname(path), has_proof, queries)
152-
15378
def check_features(parser, queries, manifest, examples_root):
15479
"""
15580
Validates every field of the manifest that can be validated.
@@ -177,14 +102,6 @@ def check_features(parser, queries, manifest, examples_root):
177102
if 'proof' in module_features and 'proof' not in module:
178103
success = False
179104
logging.error(f'Module {module["path"]} contains proof but no proof runtime details in manifest')
180-
expected_imports = get_community_imports(examples_root, tree, text, dirname(module_path), 'proof' in module_features, queries)
181-
actual_imports = set(module['communityDependencies'])
182-
if expected_imports != actual_imports:
183-
success = False
184-
logging.error(
185-
f'Module {module["path"]} has incorrect community dependencies in manifest; '
186-
+ f'expected {list(expected_imports)}, actual {list(actual_imports)}'
187-
)
188105
for model in module['models']:
189106
if tla_utils.has_state_count(model) and not tla_utils.is_state_count_valid(model):
190107
success = False

‎.github/scripts/check_proofs.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,7 @@
8080
logging.debug(output)
8181
except subprocess.TimeoutExpired as tlapm_result:
8282
# stdout is a string on Windows, byte array everywhere else
83-
stdout = tlapm_result.stdout if type(tlapm_result.stdout) == str else tlapm_result.stdout.decode('utf-8')
83+
stdout = '' if tlapm_result.stdout is None else tlapm_result.stdout if type(tlapm_result.stdout) == str else tlapm_result.stdout.decode('utf-8')
8484
args, timeout = tlapm_result.args
8585
logging.error(f'{module_path} hit hard timeout of {timeout} seconds')
8686
output = ' '.join(args) + '\n' + stdout

‎.github/scripts/generate_manifest.py‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,6 @@ def generate_new_manifest(examples_root, spec_path, spec_name, parser, queries):
8383
'modules': [
8484
{
8585
'path': tla_utils.to_posix(tla_path),
86-
'communityDependencies': sorted(list(get_community_module_imports(examples_root, parser, tla_path, queries))),
8786
'features': sorted(list(module_features - {'proof'})),
8887
'models': [
8988
{

‎CONTRIBUTING.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ Steps:
4545
- Spec authors: a list of people who authored the spec
4646
- Spec tags:
4747
- `"beginner"` if your spec is appropriate for TLA⁺ newcomers
48-
- Module proof runtime: if module contains formal proofs, record the approximate time necessary to check the proofs with TLAPM on an ordinary workstation; add `"proof" : { "runtime" : "HH:MM:SS" }` to the module fields at the same level as the `communityDependencies` and `models`
48+
- Module proof runtime: if module contains formal proofs, record the approximate time necessary to check the proofs with TLAPM on an ordinary workstation; add `"proof" : { "runtime" : "HH:MM:SS" }` to the module fields at the same level as `models`
4949
- If less than one minute, proof will be checked in its entirety by the CI
5050
- Model runtime: approximate model runtime on an ordinary workstation, in `"HH:MM:SS"` format
5151
- If less than 30 seconds, will be run in its entirety by the CI; otherwise will only be smoke-tested for 5 seconds

‎manifest-schema.json‎

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -19,14 +19,10 @@
1919
"type": "array",
2020
"items": {
2121
"type": "object",
22-
"required": ["path", "communityDependencies", "features", "models"],
22+
"required": ["path", "features", "models"],
2323
"additionalProperties": false,
2424
"properties": {
2525
"path": {"type": "string"},
26-
"communityDependencies": {
27-
"type": "array",
28-
"items": {"type": "string"}
29-
},
3026
"features": {
3127
"type": "array",
3228
"items": {"enum": ["pluscal", "action composition"]}

‎specifications/Bakery-Boulangerie/manifest.json‎

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@
88
"modules": [
99
{
1010
"path": "specifications/Bakery-Boulangerie/Bakery.tla",
11-
"communityDependencies": [],
1211
"features": [
1312
"pluscal"
1413
],
@@ -19,7 +18,6 @@
1918
},
2019
{
2120
"path": "specifications/Bakery-Boulangerie/Boulanger.tla",
22-
"communityDependencies": [],
2321
"features": [
2422
"pluscal"
2523
],
@@ -30,7 +28,6 @@
3028
},
3129
{
3230
"path": "specifications/Bakery-Boulangerie/MCBakery.tla",
33-
"communityDependencies": [],
3431
"features": [],
3532
"models": [
3633
{
@@ -46,7 +43,6 @@
4643
},
4744
{
4845
"path": "specifications/Bakery-Boulangerie/MCBoulanger.tla",
49-
"communityDependencies": [],
5046
"features": [],
5147
"models": [
5248
{
@@ -58,4 +54,4 @@
5854
]
5955
}
6056
]
61-
}
57+
}

‎specifications/CarTalkPuzzle/manifest.json‎

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -9,19 +9,16 @@
99
"modules": [
1010
{
1111
"path": "specifications/CarTalkPuzzle/CarTalkPuzzle.tla",
12-
"communityDependencies": [],
1312
"features": [],
1413
"models": []
1514
},
1615
{
1716
"path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_1/CarTalkPuzzle.tla",
18-
"communityDependencies": [],
1917
"features": [],
2018
"models": []
2119
},
2220
{
2321
"path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_1/MC.tla",
24-
"communityDependencies": [],
2522
"features": [],
2623
"models": [
2724
{
@@ -37,13 +34,11 @@
3734
},
3835
{
3936
"path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_2/CarTalkPuzzle.tla",
40-
"communityDependencies": [],
4137
"features": [],
4238
"models": []
4339
},
4440
{
4541
"path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_2/MC.tla",
46-
"communityDependencies": [],
4742
"features": [],
4843
"models": [
4944
{
@@ -59,13 +54,11 @@
5954
},
6055
{
6156
"path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_3/CarTalkPuzzle.tla",
62-
"communityDependencies": [],
6357
"features": [],
6458
"models": []
6559
},
6660
{
6761
"path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_3/MC.tla",
68-
"communityDependencies": [],
6962
"features": [],
7063
"models": [
7164
{

‎specifications/Chameneos/manifest.json‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@
99
"modules": [
1010
{
1111
"path": "specifications/Chameneos/Chameneos.tla",
12-
"communityDependencies": [],
1312
"features": [],
1413
"models": [
1514
{

‎specifications/CheckpointCoordination/manifest.json‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,13 +10,11 @@
1010
"modules": [
1111
{
1212
"path": "specifications/CheckpointCoordination/CheckpointCoordination.tla",
13-
"communityDependencies": [],
1413
"features": [],
1514
"models": []
1615
},
1716
{
1817
"path": "specifications/CheckpointCoordination/MCCheckpointCoordination.tla",
19-
"communityDependencies": [],
2018
"features": [],
2119
"models": [
2220
{

‎specifications/CigaretteSmokers/manifest.json‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@
99
"modules": [
1010
{
1111
"path": "specifications/CigaretteSmokers/CigaretteSmokers.tla",
12-
"communityDependencies": [],
1312
"features": [],
1413
"models": [
1514
{

0 commit comments

Comments
 (0)