From 921866e6217e1eb22ae62d51daf4a7d8fd4b54fd Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Thu, 9 Jan 2025 19:05:33 +0000 Subject: [PATCH] fix(scripts/yaml_check.py): more consistent error handling (#20614) Invalid fields in the 100.yaml and 1000.yaml files are slipping through CI at the moment, see e.g. [this log](https://github.com/leanprover-community/mathlib4/actions/runs/12690334474/job/35370960547#step:19:8). After this commit, all errors detected by `yaml_check.py` print a message and increment the `errors` variable, only failing at the end of the script (so that all entries can get checked). --- scripts/yaml_check.py | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/scripts/yaml_check.py b/scripts/yaml_check.py index bf31ad0b0ecda..5cf9cb9e00a06 100644 --- a/scripts/yaml_check.py +++ b/scripts/yaml_check.py @@ -110,6 +110,7 @@ class ThousandPlusTheorem: _thm = HundredTheorem(index, **entry) except TypeError as e: print(f"error: entry for theorem {index} is invalid: {e}") + errors += 1 # Also verify that the |decl| and |decls| fields are not *both* provided. if _thm.decl and _thm.decls: print(f"warning: entry for theorem {index} has both a decl and a decls field; " @@ -121,7 +122,8 @@ class ThousandPlusTheorem: hundred_decls.append((f'{index} {title}', entry['decl'])) elif 'decls' in entry: if not isinstance(entry['decls'], list): - raise ValueError(f"For key {index} ({title}): did you mean `decl` instead of `decls`?") + print(f"For key {index} ({title}): did you mean `decl` instead of `decls`?") + errors += 1 hundred_decls = hundred_decls + [(f'{index} {title}', d) for d in entry['decls']] thousand_decls: List[Tuple[str, str]] = [] @@ -131,6 +133,7 @@ class ThousandPlusTheorem: _thm = ThousandPlusTheorem(index, **entry) except TypeError as e: print(f"error: entry for theorem {index} is invalid: {e}") + errors += 1 # Also verify that the |decl| and |decls| fields are not *both* provided. if _thm.decl and _thm.decls: print(f"warning: entry for theorem {index} has both a decl and a decls field; " @@ -142,7 +145,8 @@ class ThousandPlusTheorem: thousand_decls.append((f'{index} {title}', entry['decl'])) elif 'decls' in entry: if not isinstance(entry['decls'], list): - raise ValueError(f"For key {index} ({title}): did you mean `decl` instead of `decls`?") + print(f"For key {index} ({title}): did you mean `decl` instead of `decls`?") + errors += 1 thousand_decls = thousand_decls + [(f'{index} {title}', d) for d in entry['decls']] overview_decls = tiered_extract(overview) @@ -163,4 +167,5 @@ class ThousandPlusTheorem: json.dump(undergrad_decls, f) if errors: - sys.exit(errors) + # Return an error code of at most 125 so this return value can be used further in shell scripts. + sys.exit(min(errors, 125))