wip: require all scripts to be documented

scripts/lint_style.lean

@@ -16,19 +16,44 @@ The linters themselves are defined in `Mathlib.Tactic.Linter.TextBased`.
 
 open Cli
 
+open System.FilePath
+
+/-- Verifies that every file in the `scripts` directory is documented in `scripts/README.md`. -/
+def checkScriptsDocumented : IO Bool := do
+  -- Retrieve all scripts (except for the `bench` directory).
+  let allScripts : Array System.FilePath ← walkDir "scripts"
+    fun p ↦ pure (p.components.getD 1 "" != "bench")
+  -- TODO: drop some false positives
+  --   "bench" and "README.md" should be ignored right away
+  --   nolint.json and noshake.json are data files; as are style-exceptions.txt and nolints-style.txt
+  --   these *could* be explicitly allows, or documented as well (perhaps the latter?)
+  -- Check if the README text contains each file enclosed in backticks.
+  let readme : String ← IO.FS.readFile (System.mkFilePath ["scripts", "README.md"])
+  --let sdf := (System.mkFilePath ["scripts", "README.md"])
+  --let sdf := sdf.components.headD ""
+  IO.println s!"found {allScripts.size} scripts: {",".intercalate (allScripts.map (·.toString)).toList}"
+  let undocumented := allScripts.filter fun script ↦ !readme.containsSubstr s!"`{script}`"
+  if undocumented.size > 0 then
+    IO.println s!"error: found {undocumented.size} undocumented scripts:\
+      please describe the scripts\n\
+      {String.intercalate "," (undocumented.map (·.fileName.get!)).toList}\n\
+     in 'scripts/README.md'"
+  return undocumented.size > 0
+
 /-- Implementation of the `lint_style` command line program. -/
 def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do
   let errorStyle := match (args.hasFlag "github", args.hasFlag "update") with
     | (true, _) => ErrorFormat.github
     | (false, true) => ErrorFormat.exceptionsFile
     | (false, false) => ErrorFormat.humanReadable
-  let mut numberErrorFiles : UInt32 := 0
+  let mut numberErrors : UInt32 := 0
   for s in ["Archive.lean", "Counterexamples.lean", "Mathlib.lean"] do
     let n ← lintAllFiles (System.mkFilePath [s]) errorStyle
-    numberErrorFiles := numberErrorFiles + n
+    numberErrors := numberErrors + n
+  if ← checkScriptsDocumented then numberErrors := numberErrors + 1
   -- Make sure to return an exit code of at most 125, so this return value can be used further
   -- in shell scripts.
-  return min numberErrorFiles 125
+  return min numberErrors 125
 
 /-- Setting up command line options and help text for `lake exe lint_style`. -/
 -- so far, no help options or so: perhaps that is fine?