From f966474ac9dc4d5ff1f1cb1de556cf4767ec6288 Mon Sep 17 00:00:00 2001 From: damiano Date: Fri, 24 May 2024 03:47:06 +0000 Subject: [PATCH] feat: syntax linter for `#`-commands (#11019) A Lean-linter implementation of the `#`-command linter introduced in #10809. This linter produces a warning whenever a non-allowed `#`-command is used. The allowed commands are ```lean #align #align_import #noalign #adaptation_note ``` [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2311019.3A.20a.20syntax.20linter.20for.20.23-commands) Co-authored-by: Michael Rothgang --- Mathlib.lean | 1 + Mathlib/Tactic.lean | 1 + Mathlib/Tactic/Linter.lean | 1 + Mathlib/Tactic/Linter/HashCommandLinter.lean | 87 ++++++++++++++ test/HashCommandLinter.lean | 114 +++++++++++++++++++ 5 files changed, 204 insertions(+) create mode 100644 Mathlib/Tactic/Linter/HashCommandLinter.lean create mode 100644 test/HashCommandLinter.lean diff --git a/Mathlib.lean b/Mathlib.lean index bd206c0d44a3c..25e7ac4d631d4 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3773,6 +3773,7 @@ import Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithm import Mathlib.Tactic.Linarith.Verification import Mathlib.Tactic.LinearCombination import Mathlib.Tactic.Linter +import Mathlib.Tactic.Linter.HashCommandLinter import Mathlib.Tactic.Linter.Lint import Mathlib.Tactic.Measurability import Mathlib.Tactic.Measurability.Init diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean index 89ca2fd4e18d1..91fb8bd191a4b 100644 --- a/Mathlib/Tactic.lean +++ b/Mathlib/Tactic.lean @@ -112,6 +112,7 @@ import Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithm import Mathlib.Tactic.Linarith.Verification import Mathlib.Tactic.LinearCombination import Mathlib.Tactic.Linter +import Mathlib.Tactic.Linter.HashCommandLinter import Mathlib.Tactic.Linter.Lint import Mathlib.Tactic.Measurability import Mathlib.Tactic.Measurability.Init diff --git a/Mathlib/Tactic/Linter.lean b/Mathlib/Tactic/Linter.lean index fbc9af4ccf56f..25a25c423029f 100644 --- a/Mathlib/Tactic/Linter.lean +++ b/Mathlib/Tactic/Linter.lean @@ -7,4 +7,5 @@ This file is ignored by `Shake`: * it is in `ignoreImport`, meaning that where it is imported, it is considered necessary. -/ +import Mathlib.Tactic.Linter.HashCommandLinter import Mathlib.Tactic.Linter.Lint diff --git a/Mathlib/Tactic/Linter/HashCommandLinter.lean b/Mathlib/Tactic/Linter/HashCommandLinter.lean new file mode 100644 index 0000000000000..64ee30a0e6d9e --- /dev/null +++ b/Mathlib/Tactic/Linter/HashCommandLinter.lean @@ -0,0 +1,87 @@ +/- +Copyright (c) 2024 Damiano Testa. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Damiano Testa +-/ + +import Lean.Elab.Command +import Lean.Linter.Util +import Batteries.Lean.HashSet + +/-! +# `#`-command linter + +The `#`-command linter produces a warning when a command starting with `#` is used *and* +* either the command emits no message; +* or `warningAsError` is set to `true`. + +The rationale behind this is that `#`-commands are intended to be transient: +they provide useful information in development, but are not intended to be present in final code. +Most of them are noisy and get picked up anyway by CI, but even the quiet ones are not expected to +outlive their in-development status. +-/ + +namespace Mathlib.Linter + +/-- +The linter emits a warning on any command beginning with `#` that itself emits no message. +For example, `#guard true` and `#check_tactic True ~> True by skip` trigger a message. +There is a list of silent `#`-command that are allowed. +-/ +register_option linter.hashCommand : Bool := { + defValue := true + descr := "enable the `#`-command linter" +} + +namespace HashCommandLinter + +open Lean Elab + +/-- Gets the value of the `linter.hashCommand` option. -/ +def getLinterHash (o : Options) : Bool := Linter.getLinterValue linter.hashCommand o + +open Command in +/-- Exactly like `withSetOptionIn`, but recursively discards nested uses of `in`. +Intended to be used in the `hashCommand` linter, where we want to enter `set_option` `in` commands. +-/ +private partial def withSetOptionIn' (cmd : CommandElab) : CommandElab := fun stx => do + if stx.getKind == ``Lean.Parser.Command.in then + if stx[0].getKind == ``Lean.Parser.Command.set_option then + let opts ← Elab.elabSetOption stx[0][1] stx[0][3] + withScope (fun scope => { scope with opts }) do + withSetOptionIn' cmd stx[2] + else + withSetOptionIn' cmd stx[2] + else + cmd stx + +/-- `allowed_commands` is the `HashSet` of `#`-commands that are allowed in 'Mathlib'. -/ +private abbrev allowed_commands : HashSet String := + { "#align", "#align_import", "#noalign", "#adaptation_note" } + +/-- Checks that no command beginning with `#` is present in 'Mathlib', +except for the ones in `allowed_commands`. + +If `warningAsError` is `true`, then the linter logs an info (rather than a warning). +This means that CI will eventually fail on `#`-commands, but not stop it from continuing. + +However, in order to avoid local clutter, when `warningAsError` is `false`, the linter +logs a warning only for the `#`-commands that do not already emit a message. -/ +def hashCommandLinter : Linter where run := withSetOptionIn' fun stx => do + let mod := (← getMainModule).components + if getLinterHash (← getOptions) && + ((← get).messages.msgs.size == 0 || warningAsError.get (← getOptions)) && + -- we check that the module is either not in `test` or, is `test.HashCommandLinter` + (mod.getD 0 default != `test || (mod == [`test, `HashCommandLinter])) + then + if let some sa := stx.getHead? then + let a := sa.getAtomVal + if (a.get ⟨0⟩ == '#' && ! allowed_commands.contains a) then + let msg := m!"`#`-commands, such as '{a}', are not allowed in 'Mathlib'" + if warningAsError.get (← getOptions) then + logInfoAt sa (msg ++ " [linter.hashCommand]") + else Linter.logLint linter.hashCommand sa msg + +initialize addLinter hashCommandLinter + +end HashCommandLinter diff --git a/test/HashCommandLinter.lean b/test/HashCommandLinter.lean new file mode 100644 index 0000000000000..4a495a84f3ee4 --- /dev/null +++ b/test/HashCommandLinter.lean @@ -0,0 +1,114 @@ +import Lean.Elab.GuardMsgs +import Mathlib.Mathport.Rename +import Mathlib.Tactic.AdaptationNote +import Mathlib.Tactic.Linter.HashCommandLinter + +section ignored_commands +theorem fo₁ : True := .intro +-- `#align` is allowed by the linter +#align true fo₁ + +-- `#guard_msgs in` without a doc-string triggers the linter, but with the `doc-string does not +/-- +warning: `#`-commands, such as '#guard_msgs', are not allowed in 'Mathlib' +note: this linter can be disabled with `set_option linter.hashCommand false` +-/ +#guard_msgs in +#guard_msgs in +#adaptation_note /-- testing that the hashCommand linter ignores this. -/ + +/-- info: 0 -/ +#guard_msgs in +-- emits a message -- the linter allows it +#eval 0 + +/-- info: constructor PUnit.unit.{u} : PUnit -/ +#guard_msgs in +-- emits a message -- the linter allows it +#print PUnit.unit + +/-- info: 0 : Nat -/ +#guard_msgs in +-- emits a message -- the linter allows it +#check 0 + +/-- +info: +-/ +#guard_msgs in +-- emits an empty message -- the linter allows it +#eval show Lean.MetaM _ from do guard true + +-- not a `#`-command and not emitting a message: the linter allows it +run_cmd if false then Lean.logInfo "0" +end ignored_commands + +section linted_commands +/-- +warning: `#`-commands, such as '#guard', are not allowed in 'Mathlib' +note: this linter can be disabled with `set_option linter.hashCommand false` +-/ +#guard_msgs in +#guard true + +/-- +warning: `#`-commands, such as '#check_tactic', are not allowed in 'Mathlib' +note: this linter can be disabled with `set_option linter.hashCommand false` +-/ +#guard_msgs in +#check_tactic True ~> True by skip + +-- Testing that the linter enters `in` recursively. + +/-- +warning: `#`-commands, such as '#guard', are not allowed in 'Mathlib' +note: this linter can be disabled with `set_option linter.hashCommand false` +-/ +#guard_msgs in +variable (n : Nat) in +#guard true + +/-- +warning: `#`-commands, such as '#guard', are not allowed in 'Mathlib' +note: this linter can be disabled with `set_option linter.hashCommand false` +-/ +#guard_msgs in +open Nat in +variable (n : Nat) in +variable (n : Nat) in +#guard true + +/-- +warning: `#`-commands, such as '#guard', are not allowed in 'Mathlib' +note: this linter can be disabled with `set_option linter.hashCommand false` +-/ +#guard_msgs in +open Nat in +variable (n : Nat) in +#guard true + +-- a test for `withSetOptionIn'` +set_option linter.unusedVariables false in +example {n : Nat} : Nat := 0 + +section warningAsError + +-- if `warningAsError = true`, log an info (instead of a warning) on all `#`-commands, noisy or not +set_option warningAsError true +/-- +info: 0 +--- +info: `#`-commands, such as '#eval', are not allowed in 'Mathlib' [linter.hashCommand] +-/ +#guard_msgs in +#eval 0 + +/-- +info: `#`-commands, such as '#guard', are not allowed in 'Mathlib' [linter.hashCommand] +-/ +#guard_msgs in +#guard true + +end warningAsError + +end linted_commands