Rewriting lint-style.py in Lean

Stream: mathlib4

[Michael Rothgang]

I have "just" rewritten most of lint-style.py in Lean: more specifically:

• #12928 rewrites the set_option linter in syntax, as an honest syntax linter
  (This also means better coverage.)

• #13199 rewrites most remaining linters as text-based Lean linters. For simplicity, that PR depends on this one - but feel free to review it already. (The file Tactic/Linter/TextBased.lean defines the linter; the other changes are from the previous PR or PRed separately.)

I am looking particularly for feedback on

• any performance aspects I have overlooked? I've gone through at least one round of macro-optimising all checkers; now they're not abyssimally slow any more: but I'm sure they could be faster!
• thoughts on integrating this into mathlib
• taking a look at the spin-off PRs, particularly #12928 and #13212 (but #13203 is also welcome)

[Michael Rothgang]

Help rewriting the remaining linters is also most welcome: these are

• the "missing module docstring" linter -> can or should this become part of the docBlame linter?
• "the second line is not correctly indented" -> long-term, this should become part of a formatter...
• "space after "←", in tactic lists (but not when this refers to monads) -> this should become a syntax linter
• rewriting the non-terminal simp linter: I think the best way is to land #11821, after ironing out whatever kinks remain.

[Thomas Murrills]

For writing the remaining linters, note that #11520 (which isn’t quite ready, but does work) might be relevant/convenient: it allows us to lint syntax by matching on it in macro_rules style, e.g.

linting_rules : style
| `(foo_stx) => return msg

[Thomas Murrills]

(“String-based” linters like “space after ←” in this context could involve inspecting the source info, and the syntax match means we know we’re looking “at the right thing”. Though the motivation for #11520 is really the ability to deprecate syntax.)

[Damiano Testa]

This is great, thanks! I left two "bureaucratic" comments on the PR.

[Michael Rothgang]

Thanks for the feedback. A status update:

• the performance issue has been resolved (compiling instead of running the interpreter really helps)
• I have hooked up the linter to the build workflow and verified that new linter's errors are caught in CI
• In short: there are no conceptual questions remaining with the rewrite, mostly reviewing and landing code! Reviews are welcome on
  • #13240, rewriting the copyright header check (and basic infrastructure)
  • #13245, rewriting update_style_exceptions.py in Lean: an important pre-requisite for moving the later linters
  • #12928, rewriting the set_option linter: this is a syntax linter, hence this PR is independent of the others

This is one of my first programming projects in Lean: I'm sure there's the occasional language feature making my life easier. Even a look from the "code style" perspective is useful!

[Richard Osborn]

In #12928, I was looking at setOptionLinter and was thinking of ways of flattening the code. Ultimately, the code is essentially "if b then return" repeated, so it seems like there should be a way of writing this without the repetition. My first thought is there must be a way of wrapping CommandElabM Unit with an Alternative instance, so that it's failure is just return. The following is a partial flattening, but I feel like it could be made to look much nicer.

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, name) := do
      let head ← stx.find? is_set_option
      let name := (toString (← parse_set_option head)).drop 1
      guard <| name.startsWith "pp." || name.startsWith "profiler." || name.startsWith "trace."
      return (head, name)
    then
      Linter.logLint linter.setOption head m!"Forbidden set_option `{name}`; please remove"

I'd love to know if what I'm imagining is possible or if I'm just sleep deprived :sweat_smile:

[Richard Osborn]

Ok, I managed to get the following working.

def setOptionLinter : Linter where run := withSetOptionIn fun stx => return <* OptionT.run do
  guard <| getLinterHash (← getOptions)
  guard ¬ (← MonadState.get).messages.hasErrors
  let head ← stx.find? is_set_option
  -- Drop a leading backtick.
  let name := (toString (← parse_set_option head)).drop 1
  guard <| name.startsWith "pp." || name.startsWith "profiler." || name.startsWith "trace."
  Linter.logLint linter.setOption head m!"Forbidden set_option `{name}`; please remove"

[Richard Osborn]

@Michael Rothgang Does the above code seems like an improvement? Feel free to use it or if you want I can submit a patch to the PR. You will need to import Lake.Util.Lift for the Monad lifting instances.

[Michael Rothgang]

@Richard Osborn Thanks for thinking about this! To me, this code is denser, but not necessarily clearer... you're aiming at removing the initial "if b then return" pattern?

[Jon Eugster]

My reasoning is not really rational, but somehow I find the following the easiest to parse:

def setOptionLinter : Linter where run := withSetOptionIn fun stx => return <* OptionT.run do
  guard <| getLinterHash (← getOptions)
  guard ¬ (← MonadState.get).messages.hasErrors
  let head ← stx.find? is_set_option
  let name := (toString (← parse_set_option head)).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"

[Richard Osborn]

I like Jon's suggestion as well. It'd also look nicer if guard wasn't a function, but notation. I realize the "monadic style" is still not as common as the normal imperative if-then, but I mainly find the nested if let some ... fairly clunky looking. As lean is the only language I know of that does this imperative style do blocks, I'm not entirely sure what the right balance is.

[Patrick Massot]

Those string manipulations are not the right way to handle Lean names. You should use the Name api.

[Michael Rothgang]

Fair point, I'll read up on it and use it. (Might be in two or three weeks only.)

[Michael Rothgang]

Thanks for the pointer!