From b9903b05f7903510fcb266d27ca1a01829d64d9b Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 15 May 2024 15:07:41 +0200 Subject: [PATCH] feat: rewrite set_option style linter in lean Unlike the Python version, this script also supports set_option tactics and terms. --- Mathlib.lean | 1 + Mathlib/Tactic.lean | 1 + Mathlib/Tactic/Linter.lean | 2 +- Mathlib/Tactic/Linter/Style.lean | 69 ++++++++++++++++++++ scripts/lint-style.py | 18 ------ test/lint_style.lean | 108 +++++++++++++++++++++++++++++++ 6 files changed, 180 insertions(+), 19 deletions(-) create mode 100644 Mathlib/Tactic/Linter/Style.lean create mode 100644 test/lint_style.lean diff --git a/Mathlib.lean b/Mathlib.lean index 654d0d50d56d3c..032f89be4c4015 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3767,6 +3767,7 @@ import Mathlib.Tactic.Linarith.Verification import Mathlib.Tactic.LinearCombination import Mathlib.Tactic.Linter import Mathlib.Tactic.Linter.Lint +import Mathlib.Tactic.Linter.Style import Mathlib.Tactic.Measurability import Mathlib.Tactic.Measurability.Init import Mathlib.Tactic.MkIffOfInductiveProp diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean index 89ca2fd4e18d15..be9923bda32464 100644 --- a/Mathlib/Tactic.lean +++ b/Mathlib/Tactic.lean @@ -113,6 +113,7 @@ import Mathlib.Tactic.Linarith.Verification import Mathlib.Tactic.LinearCombination import Mathlib.Tactic.Linter import Mathlib.Tactic.Linter.Lint +import Mathlib.Tactic.Linter.Style import Mathlib.Tactic.Measurability import Mathlib.Tactic.Measurability.Init import Mathlib.Tactic.MkIffOfInductiveProp diff --git a/Mathlib/Tactic/Linter.lean b/Mathlib/Tactic/Linter.lean index fbc9af4ccf56f5..ca02fe094f3314 100644 --- a/Mathlib/Tactic/Linter.lean +++ b/Mathlib/Tactic/Linter.lean @@ -2,7 +2,7 @@ This is the `Linter`s file: it only imports files defining linters and is intended to be imported fairly early in `Mathlib`. -This file is ignored by `Shake`: +This file is ignored by `shake`: * it is in `ignoreAll`, meaning that all its imports are considered necessary; * it is in `ignoreImport`, meaning that where it is imported, it is considered necessary. -/ diff --git a/Mathlib/Tactic/Linter/Style.lean b/Mathlib/Tactic/Linter/Style.lean new file mode 100644 index 00000000000000..5aa61dec213f1d --- /dev/null +++ b/Mathlib/Tactic/Linter/Style.lean @@ -0,0 +1,69 @@ +/- +Copyright (c) 2024 Michael Rothgang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Rothgang +-/ + +import Lean.Elab.Command +import Lean.Linter.Util + +/-! +## Style linters + +This file contains (currently one, eventually more) linters about stylistic aspects: +these are only about coding style, but do not affect correctness nor global coherence of mathlib. +Historically, these were ported from the `lint-style.py` Python script. +-/ + +open Lean Elab Command + +namespace Mathlib.Linter.Style.SetOption + +/-- Whether a syntax element is a `set_option` call: +Return the name of the option being set, if any. -/ +def parse_set_option : Syntax → Option (Ident) + -- This handles all four possibilities of `_val`: a string, number, `true` and `false` + | `(command|set_option $name:ident $_val) => some name + | `(set_option $name:ident $_val in $_x) => some name + | `(tactic|set_option $name:ident $_val in $_x) => some name + | _ => none + +/-- Whether a given piece of syntax is a `set_option` command, tactic or term. -/ +def is_set_option : Syntax → Bool := + fun stx ↦ parse_set_option stx matches some _name + +/-- The `setOption` linter emits a warning on a `set_option` command, term or tactic +which sets a `pp`, `profiler` or `trace` option. -/ +register_option linter.setOption : Bool := { + defValue := true + descr := "enable the `setOption` linter" +} + +/-- Gets the value of the `linter.setOption` option. -/ +def getLinterHash (o : Options) : Bool := Linter.getLinterValue linter.setOption o + +/-- The `setOption` linter: this lints any `set_option` command, term or tactic +which sets a `pp`, `profiler` or `trace` option. + +**Why is this bad?** These options are good for debugging, but should not be +used in production code. +**How to fix this?** Remove these options: usually, they are not necessary for production code. +(Some tests will intentionally use one of these options; in this case, simply allow the linter.) +-/ +def setOptionLinter : Linter where run := withSetOptionIn fun stx => do + unless getLinterHash (← getOptions) do + return + if (← MonadState.get).messages.hasErrors then + return + match stx.findStack? (fun _ ↦ true) is_set_option with + | some ((head, _n)::_chain) => + if let some (name) := parse_set_option head then + -- Drop a leading backtick. + let name := (toString name).drop 1 + if name.startsWith "pp." || name.startsWith "profiler." || name.startsWith "trace." then + Linter.logLint linter.setOption head m!"Forbidden set_option `{name}`; please remove" + | _ => return + +initialize addLinter setOptionLinter + +end Mathlib.Linter.Style.SetOption diff --git a/scripts/lint-style.py b/scripts/lint-style.py index b7fe40603202f6..7c54bfaa83c5d3 100755 --- a/scripts/lint-style.py +++ b/scripts/lint-style.py @@ -40,7 +40,6 @@ ERR_COP = 0 # copyright header ERR_MOD = 2 # module docstring ERR_LIN = 3 # line length -ERR_OPT = 6 # set_option ERR_AUT = 7 # malformed authors list ERR_TAC = 9 # imported Mathlib.Tactic ERR_IBY = 11 # isolated by @@ -142,20 +141,6 @@ def annotate_strings(enumerate_lines): continue yield line_nr, line, *rem, False -def set_option_check(lines, path): - errors = [] - newlines = [] - for line_nr, line, in_comment, in_string in annotate_strings(annotate_comments(lines)): - if line.strip().startswith('set_option') and not in_comment and not in_string: - option_prefix = line.strip().split(' ', 2)[1].split('.', 1)[0] - # forbidden options: pp, profiler, trace - if option_prefix in {'pp', 'profiler', 'trace'}: - errors += [(ERR_OPT, line_nr, path)] - # skip adding this line to newlines so that we suggest removal - continue - newlines.append((line_nr, line)) - return errors, newlines - def line_endings_check(lines, path): errors = [] newlines = [] @@ -373,8 +358,6 @@ def format_errors(errors): output_message(path, line_nr, "ERR_MOD", "Module docstring missing, or too late") if errno == ERR_LIN: output_message(path, line_nr, "ERR_LIN", "Line has more than 100 characters") - if errno == ERR_OPT: - output_message(path, line_nr, "ERR_OPT", "Forbidden set_option command") if errno == ERR_AUT: output_message(path, line_nr, "ERR_AUT", "Authors line should look like: 'Authors: Jean Dupont, Иван Иванович Иванов'") if errno == ERR_TAC: @@ -410,7 +393,6 @@ def lint(path, fix=False): four_spaces_in_second_line, long_lines_check, isolated_by_dot_semicolon_check, - set_option_check, left_arrow_check, nonterminal_simp_check]: errs, newlines = error_check(newlines, path) diff --git a/test/lint_style.lean b/test/lint_style.lean new file mode 100644 index 00000000000000..e2371653e0074a --- /dev/null +++ b/test/lint_style.lean @@ -0,0 +1,108 @@ +import Mathlib.Tactic.Linter.Style +import Mathlib.Tactic.Common + +/-! Tests for all the style linters. -/ + +/-! Tests for the `setOption` linter -/ +section setOption + +-- The warning generated by `linter.setOption` is not suppressed by `#guard_msgs`, +-- because the linter is run on `#guard_msgs` itself. This is a known issue, see e.g. +-- https://leanprover.zulipchat.com/#narrow/stream/348111-batteries/topic/unreachableTactic.20linter.20not.20suppressed.20by.20.60.23guard_msgs.60 +-- We jump through an extra hoop here to silence the warning. + +-- All types of options are supported: boolean, numeric and string-valued. +-- On the top level, i.e. as commands. + +set_option linter.setOption false in +/-- +warning: Forbidden set_option `pp.all`; please remove +note: this linter can be disabled with `set_option linter.setOption false` +-/ +#guard_msgs in +set_option linter.setOption true in +set_option pp.all true + +set_option linter.setOption false in +/-- +warning: Forbidden set_option `pp.all`; please remove +note: this linter can be disabled with `set_option linter.setOption false` +-/ +#guard_msgs in +set_option linter.setOption true in +set_option pp.all false + +set_option linter.setOption false in +/-- +warning: Forbidden set_option `pp.raw.maxDepth`; please remove +note: this linter can be disabled with `set_option linter.setOption false` +-/ +#guard_msgs in +set_option linter.setOption true in +set_option pp.raw.maxDepth 32 + +set_option linter.setOption false in +/-- +warning: Forbidden set_option `trace.profiler.output`; please remove +note: this linter can be disabled with `set_option linter.setOption false` +-/ +#guard_msgs in +set_option linter.setOption true in +set_option trace.profiler.output "foo" + +-- The lint does not fire on arbitrary options. +set_option autoImplicit false + +-- We also cover set_option tactics. + +set_option linter.setOption false in +/-- +warning: Forbidden set_option `pp.all`; please remove +note: this linter can be disabled with `set_option linter.setOption false` +-/ +#guard_msgs in +set_option linter.setOption true in +lemma tactic : True := by + set_option pp.all true in + trivial + +set_option linter.setOption false in +/-- +warning: Forbidden set_option `pp.raw.maxDepth`; please remove +note: this linter can be disabled with `set_option linter.setOption false` +-/ +#guard_msgs in +set_option linter.setOption true in +lemma tactic2 : True := by + set_option pp.raw.maxDepth 32 in + trivial + +set_option linter.setOption false in +/-- +warning: Forbidden set_option `pp.all`; please remove +note: this linter can be disabled with `set_option linter.setOption false` +-/ +#guard_msgs in +set_option linter.setOption true in +lemma tactic3 : True := by + set_option pp.all false in + trivial + +set_option linter.setOption false in +/-- +warning: Forbidden set_option `trace.profiler.output`; please remove +note: this linter can be disabled with `set_option linter.setOption false` +-/ +#guard_msgs in +set_option linter.setOption true in +lemma tactic4 : True := by + set_option trace.profiler.output "foo" in + trivial + +-- This option is not affected, hence does not throw an error. +set_option autoImplicit true in +lemma foo' : True := trivial + +-- TODO: add terms for the term form + +end setOption