Skip to content

Commit

Permalink
feat: rewrite set_option style linter in lean (#12928)
Browse files Browse the repository at this point in the history
Unlike the Python version, this script also supports set_option tactics and terms, and we add a couple of tests.
  • Loading branch information
grunweg authored and AntoineChambert-Loir committed Jun 20, 2024
1 parent b689e61 commit 648a142
Show file tree
Hide file tree
Showing 12 changed files with 189 additions and 21 deletions.
1 change: 1 addition & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3888,6 +3888,7 @@ import Mathlib.Tactic.Linter
import Mathlib.Tactic.Linter.GlobalAttributeIn
import Mathlib.Tactic.Linter.HashCommandLinter
import Mathlib.Tactic.Linter.Lint
import Mathlib.Tactic.Linter.Style
import Mathlib.Tactic.Measurability
import Mathlib.Tactic.Measurability.Init
import Mathlib.Tactic.MkIffOfInductiveProp
Expand Down
1 change: 1 addition & 0 deletions Mathlib/Tactic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -117,6 +117,7 @@ import Mathlib.Tactic.Linter
import Mathlib.Tactic.Linter.GlobalAttributeIn
import Mathlib.Tactic.Linter.HashCommandLinter
import Mathlib.Tactic.Linter.Lint
import Mathlib.Tactic.Linter.Style
import Mathlib.Tactic.Measurability
import Mathlib.Tactic.Measurability.Init
import Mathlib.Tactic.MkIffOfInductiveProp
Expand Down
3 changes: 2 additions & 1 deletion Mathlib/Tactic/Linter.lean
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,12 @@
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.
-/

import Mathlib.Tactic.Linter.GlobalAttributeIn
import Mathlib.Tactic.Linter.HashCommandLinter
import Mathlib.Tactic.Linter.Lint
import Mathlib.Tactic.Linter.Style
72 changes: 72 additions & 0 deletions Mathlib/Tactic/Linter/Style.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,72 @@
/-
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

/-- 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"
}

namespace Style.SetOption

/-- Whether a syntax element is a `set_option` command, tactic or term:
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

/-- 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
if let some (head) := stx.find? is_set_option then
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"

initialize addLinter setOptionLinter

end Style.SetOption

end Mathlib.Linter
18 changes: 0 additions & 18 deletions scripts/lint-style.py
Original file line number Diff line number Diff line change
Expand Up @@ -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_TAC2 = 10 # imported Lake in Mathlib
Expand Down Expand Up @@ -148,20 +147,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 = []
Expand Down Expand Up @@ -392,8 +377,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:
Expand Down Expand Up @@ -433,7 +416,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,
adaptation_note_check,
nonterminal_simp_check]:
Expand Down
1 change: 1 addition & 0 deletions test/Explode.lean
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ info: true_iff : ∀ (p : Prop), (True ↔ p) = p
-/
#guard_msgs in #explode true_iff

set_option linter.setOption false
-- On command line, tests format functions with => rather than ↦ without this.
set_option pp.unicode.fun true

Expand Down
2 changes: 0 additions & 2 deletions test/LibrarySearch/IsCompact.lean
Original file line number Diff line number Diff line change
@@ -1,8 +1,6 @@
import Mathlib.Topology.Instances.Real
import Mathlib.Topology.Algebra.Order.Compact

set_option pp.unicode.fun true

-- TODO: uses sorry, but is hidden behind the `apply?`
/-- warning: declaration uses 'sorry' -/
#guard_msgs(warning, drop info) in
Expand Down
1 change: 1 addition & 0 deletions test/LibrarySearch/basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ import Mathlib.Data.Real.Basic

set_option autoImplicit true

set_option linter.setOption false
-- Enable this option for tracing:
-- set_option trace.Tactic.librarySearch true
-- And this option to trace all candidate lemmas before application.
Expand Down
1 change: 1 addition & 0 deletions test/Recall.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ import Mathlib.Analysis.Calculus.Deriv.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import Mathlib.Data.Complex.Exponential

set_option linter.setOption false
-- Remark: When the test is run by make/CI, this option is not set, so we set it here.
set_option pp.unicode.fun true
set_option autoImplicit true
Expand Down
1 change: 1 addition & 0 deletions test/delabLinearIndependent.lean
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
import Mathlib.LinearAlgebra.LinearIndependent

set_option linter.setOption false
set_option pp.unicode.fun true

variable {K V : Type*} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} {x : V}
Expand Down
108 changes: 108 additions & 0 deletions test/lint_style.lean
Original file line number Diff line number Diff line change
@@ -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
1 change: 1 addition & 0 deletions test/vec_notation.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ open Lean
open Lean.Meta
open Qq

set_option linter.setOption false in
set_option pp.unicode.fun false

/-! These tests are testing `PiFin.toExpr` and fail with
Expand Down

0 comments on commit 648a142

Please sign in to comment.