@@ -69,50 +69,45 @@ def get_cfg_files(examples_root, tla_path):
6969 ])
7070 ]
7171
72- def generate_new_manifest (examples_root , ignored_dirs , parser , queries ):
72+ def generate_new_manifest (examples_root , spec_path , spec_name , parser , queries ):
7373 """
74- Generate new base manifest.json from files in specifications dir .
74+ Generate new manifest.json file for a given specification directory .
7575 """
7676 return {
77- 'specifications' : [
77+ 'path' : to_posix (spec_path ),
78+ 'title' : spec_name ,
79+ 'description' : '' ,
80+ 'sources' : [],
81+ 'authors' : [],
82+ 'tags' : [],
83+ 'modules' : [
7884 {
79- 'path' : to_posix (spec_path ),
80- 'title' : spec_name ,
81- 'description' : '' ,
82- 'sources' : [],
83- 'authors' : [],
84- 'tags' : [],
85- 'modules' : [
85+ 'path' : to_posix (tla_path ),
86+ 'communityDependencies' : sorted (list (get_community_module_imports (examples_root , parser , tla_path , queries ))),
87+ 'tlaLanguageVersion' : 2 ,
88+ 'features' : sorted (list (get_module_features (examples_root , tla_path , parser , queries ))),
89+ 'models' : [
8690 {
87- 'path' : to_posix (tla_path ),
88- 'communityDependencies' : sorted (list (get_community_module_imports (examples_root , parser , tla_path , queries ))),
89- 'tlaLanguageVersion' : 2 ,
90- 'features' : sorted (list (get_module_features (examples_root , tla_path , parser , queries ))),
91- 'models' : [
92- {
93- 'path' : to_posix (cfg_path ),
94- 'runtime' : 'unknown' ,
95- 'size' : 'unknown' ,
96- 'mode' : 'exhaustive search' ,
97- 'features' : sorted (list (get_model_features (examples_root , cfg_path ))),
98- 'result' : 'unknown'
99- }
100- for cfg_path in sorted (get_cfg_files (examples_root , tla_path ))
101- ]
91+ 'path' : to_posix (cfg_path ),
92+ 'runtime' : 'unknown' ,
93+ 'size' : 'unknown' ,
94+ 'mode' : 'exhaustive search' ,
95+ 'features' : sorted (list (get_model_features (examples_root , cfg_path ))),
96+ 'result' : 'unknown'
10297 }
103- for tla_path in sorted (get_tla_files (examples_root , spec_path ))
98+ for cfg_path in sorted (get_cfg_files (examples_root , tla_path ))
10499 ]
105100 }
106- for ( spec_path , spec_name ) in get_spec_dirs ( examples_root , ignored_dirs )
101+ for tla_path in sorted ( get_tla_files ( examples_root , spec_path ) )
107102 ]
108103 }
109104
110105# Integrate human-written info from existing manifest.json
111106
112- def find_corresponding_spec (old_spec , new_manifest ):
107+ def find_corresponding_spec (old_manifest , new_spec ):
113108 specs = [
114- spec for spec in new_manifest ['specifications' ]
115- if to_posix ( spec ['path' ]) == old_spec ['path' ]
109+ spec for spec in old_manifest ['specifications' ]
110+ if spec ['path' ] == new_spec ['path' ]
116111 ]
117112 return specs [0 ] if any (specs ) else None
118113
@@ -146,22 +141,19 @@ def integrate_model_info(old_model, new_model):
146141 if field in old_model :
147142 new_model [field ] = old_model [field ]
148143
149- def integrate_old_manifest_into_new (old_manifest , new_manifest ):
150- for old_spec in old_manifest ['specifications' ]:
151- new_spec = find_corresponding_spec (old_spec , new_manifest )
152- if new_spec is None :
144+ def integrate_old_manifest_into_new (old_manifest , new_spec ):
145+ old_spec = find_corresponding_spec (old_manifest , new_spec )
146+ integrate_spec_info (old_spec , new_spec )
147+ for old_module in old_spec ['modules' ]:
148+ new_module = find_corresponding_module (old_module , new_spec )
149+ if new_module is None :
153150 continue
154- integrate_spec_info ( old_spec , new_spec )
155- for old_module in old_spec [ 'modules ' ]:
156- new_module = find_corresponding_module ( old_module , new_spec )
157- if new_module is None :
151+ integrate_module_info ( old_module , new_module )
152+ for old_model in old_module [ 'models ' ]:
153+ new_model = find_corresponding_model ( old_model , new_module )
154+ if new_model is None :
158155 continue
159- integrate_module_info (old_module , new_module )
160- for old_model in old_module ['models' ]:
161- new_model = find_corresponding_model (old_model , new_module )
162- if new_model is None :
163- continue
164- integrate_model_info (old_model , new_model )
156+ integrate_model_info (old_model , new_model )
165157
166158if __name__ == '__main__' :
167159 parser = ArgumentParser (description = 'Generates a new manifest.json derived from files in the repo.' )
@@ -179,8 +171,8 @@ def integrate_old_manifest_into_new(old_manifest, new_manifest):
179171 queries = build_queries (TLAPLUS_LANGUAGE )
180172
181173 old_manifest = tla_utils .load_json (manifest_path )
182- new_manifest = generate_new_manifest ( examples_root , ignored_dirs , parser , queries )
183- integrate_old_manifest_into_new ( old_manifest , new_manifest )
184-
185- tla_utils .write_json (new_manifest , manifest_path )
174+ for ( spec_path , spec_name ) in get_spec_dirs ( examples_root , ignored_dirs ):
175+ new_manifest = generate_new_manifest ( examples_root , spec_path , spec_name , parser , queries )
176+ integrate_old_manifest_into_new ( old_manifest , new_manifest )
177+ tla_utils .write_json (new_manifest , join ( spec_path , 'manifest.json' ) )
186178
0 commit comments