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 <[email protected]>

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

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

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

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

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