Skip to content

Commit

Permalink
fix(scripts/yaml_check.py): more consistent error handling (#20614)
Browse files Browse the repository at this point in the history
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).
  • Loading branch information
bryangingechen committed Jan 9, 2025
1 parent 2154395 commit 921866e
Showing 1 changed file with 8 additions and 3 deletions.
11 changes: 8 additions & 3 deletions scripts/yaml_check.py
Original file line number Diff line number Diff line change
Expand Up @@ -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; "
Expand All @@ -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]] = []
Expand All @@ -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; "
Expand All @@ -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)
Expand All @@ -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))

0 comments on commit 921866e

Please sign in to comment.