build: the fourteen type rules the gate names are errors, so a regression fails CI instead of scrolling past

[FBumann]

Prompt: "Should we add some stricter rules and add more type annotations?"

Note

The following content was generated by AI.

[tool.pyrefly.errors] said those fourteen rules were "promoted to error, so a regression fails the gate instead of scrolling past", and that "all of these are already clean". Neither was true: in pyrefly 1.2.0 rule = true enables a rule at its default severity, so nine warnings scrolled past a green gate. The severity string is what promotes. The comment is now the behaviour.

The nine, all in src/math_spec:

rule	count	what it was
unnecessary-type-conversion	4	float() on a float in dimensions.py, three str() on a str in resolution.py
redundant-cast	3	lowering.py casting VariableDomain, VariableAbsence and SosType to the Literals the model already declares
untyped-import	2	import yaml, no stubs

Dropping the three casts leaves Literal and cast unused in lowering.py; both imports go. types-pyyaml joins [feature.test.dependencies] beside pyrefly — the checker's own hint, and it keeps untyped-import a gate rather than a rule with a standing exception.

Verified

pixi run ci exit 0: lint clean (12 jobs), 911 passed, mkdocs build --strict builds, 27 TeX documents compile. pyrefly check is 0 errors, 0 warnings — the "N warnings not shown" line is gone, which is the claim.

The guard here is the gate, not a test. No pytest case can reach a severity in pyproject.toml, so the evidence is the mutation, run on the committed tree and restored with git checkout --:

Mutation table

Mutation	pyrefly check
committed tree	exit 0 — 0 errors
config back to = true, code clean	exit 0 — 0 errors
float() regression reintroduced, new config	exit 1 — 1 error
the same regression, old = true config	exit 0 — 0 errors, 1 warning not shown
types-pyyaml removed	exit 1 — 2 errors
restored	exit 0 — 0 errors

Rows three and four are the pair the PR exists for: one regression, failing under the new spelling and passing under the old.

Not done, deliberately

No new annotations, and no second checker. The question that started this was prompted by basedpyright annotations in an editor — 28 errors and 471 warnings over the same 26 files pyrefly calls clean. They do not survive reading: 133 reportAny and 68 reportExplicitAny are pydantic mode='before' validators and the YAML door, where arbitrary input is the construct; 135 reportUnknown* are the pyparsing seam [tool.pyrefly] already documents and suppresses per line; 74 are reportImplicitStringConcatenation. Annotating those away means saying something less true than Any. Two of its rules might be worth having on their own merits — reportImplicitOverride and reportUnnecessaryIsInstance, both of which pyrefly has equivalents for — and that is a separate question about pyrefly's rule list, not an argument for running two checkers that disagree about whether src/ is clean.

untyped-import was kept rather than dropped. Adding a stub package to satisfy a rule is the larger change; the alternative was deleting the rule from the list with a reason. Kept because two import yaml lines are cheap to make answerable and the rule then guards the next untyped import.

[read-the-docs-community]

Documentation build overview

📚 math-spec | 🛠️ Build #34336469 | 📁 Comparing f38b891 against latest (18644cd)

  🔍 Preview build  

11 files changed · ± 10 modified · - 1 deleted

± Modified

• CHANGELOG/index.html
• reference/language/expressions/index.html
• reference/language/reading/index.html
• reference/math_spec/dimensions/index.html
• reference/math_spec/expression_parser/index.html
• reference/math_spec/lowering/index.html
• reference/math_spec/program/index.html
• reference/math_spec/resolution/index.html
• reference/math_spec/validation/index.html
• reference/math_spec/typesetting/walk/index.html

- Deleted

• reference/math_spec/where_parser/index.html