feat: the trailingWhitespace linter

[adomani]

The trailingWhitespace linter is a syntax linter. It emits a warning whenever a line ends with a space or a file does not end with a line break.

Zulip thread

[digama0]

I think this should be disabled by default, or only enabled in CI. For people using vscode with the "remove trailing whitespace on save" option, it will only ever be a false positive triggering between keystrokes.

[adomani]

That's true: it was not easy to get the test file to work, since I could not save it!

Would the "script-style" code below be better than a linter, then?

import Lean.Elab.Command

open Lean in
run_cmd
  for fil in ← System.FilePath.walkDir ((← IO.currentDir) / "Batteries") do
    if let some "lean" := fil.extension then
      let lines ← IO.FS.lines fil
      for l in [:lines.size] do
        let line := lines[l]!
        let tr := line.takeRightWhile (·.isWhitespace)
        if !tr.isEmpty then
          logWarning
            m!"{fil}:{l} ends with {tr.length} space{if tr.length == 1 then "" else "s"}"
      if (← IO.FS.readFile fil).back != '\n' then
        logWarning m!"{fil} does not end with a line break"

This has the advantage that you do not need to make sure that the linter is imported everywhere and you can run the script on itself as well.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch batteries-pr-testing-920 has successfully built against this PR. (2024-10-01 09:05:49) View Log
• ✅ Mathlib branch batteries-pr-testing-920 has successfully built against this PR. (2024-10-02 17:48:58) View Log

[digama0]

We don't really have a place to put scripts like this. Ideally we could put it somewhere such that lake would make it available to downstream packages.