Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat: rewrite set_option style linter in lean #12928

Closed
wants to merge 7 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3816,6 +3816,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 @@ -115,6 +115,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_IBY = 11 # isolated by
Expand Down Expand Up @@ -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 = []
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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)
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
Loading