no more `make`

Stream: batteries

[Kim Morrison]

I just want to call attention to a minor triumph at batteries#918, and congratulate @Mac Malone (for lake), @Austin Letson (for lean-action), and @Mario Carneiro (for the environment linter framework) for making this possible: there is no more makefile in Batteries, and everything can be driven just by lake build, lake test, and lake lint.

[Kim Morrison]

(Now if someone just wants to rewrite scripts/lintWhitespace.sh and scripts/updateBatteries.sh in Lean, we can ignore the mess of yml files in CI, and claim that Batteries is entirely in Lean!)

[Damiano Testa]

lintWhitespace is just checking that lines do not end in space and that the last character of a file is a line break, right?

[Damiano Testa]

That should be easy to write in lean!

[Damiano Testa]

Here is an attempt: batteries#920

[Damiano Testa]

Alternatively, this could be a non-syntax linter option:

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"