While working on USubst for Programs & Formulas and updating Lean to v4.30.0-rc2, I encountered the following new warnings:
linter.flexible
'' is a flexible tactic modifying '⊢'.
Lean now distinguishes between rigid tactics, whose effect is explicit and predictable, and flexible tactics, whose behavior depends on the current proof state and may implicitly transform the goal. A new linter warns about such flexible tactics to encourage more stable proofs.
For now, we simply disable that linter by setting linter.flexible = false.
See also: https://github.com/leanprover-community/mathlib4/blob/8d6de37e7bbc54ff0e990ef68f520d847048452d/Mathlib/Tactic/Linter/FlexibleLinter.lean#L104-L108
linter.style.emptyLine
Warns on empty lines that don't have a comment. We disable this one too for now.
While working on USubst for Programs & Formulas and updating Lean to v4.30.0-rc2, I encountered the following new warnings:
linter.flexible'' is a flexible tactic modifying '⊢'.
Lean now distinguishes between rigid tactics, whose effect is explicit and predictable, and flexible tactics, whose behavior depends on the current proof state and may implicitly transform the goal. A new linter warns about such flexible tactics to encourage more stable proofs.
For now, we simply disable that linter by setting
linter.flexible = false.See also: https://github.com/leanprover-community/mathlib4/blob/8d6de37e7bbc54ff0e990ef68f520d847048452d/Mathlib/Tactic/Linter/FlexibleLinter.lean#L104-L108
linter.style.emptyLineWarns on empty lines that don't have a comment. We disable this one too for now.