[Merged by Bors] - chore(scripts): require all scripts to be documented in the README

scripts/README.md

@@ -0,0 +1,39 @@
+## Miscellaneous scripts for working on mathlib
+
+This directory contains miscellaneous scripts that are useful for working on or with mathlib.
+When adding a new script, please make sure to document it here, so other readers have a chance
+to learn about it as well!
+
+**Current scripts and their purpose.**
+TODO: add real content for all these entries!
+
+Part of mathlib
+- `polyrith_sage.py`, `polyrith_sage_helper.py`
+
+Part of CI workflow
+- `mk_all.lean`
+- `lint-style.py` and `lint-style.lean`, `print-style-errors.sh`
+- `lint-bib.sh`
+- `yaml_check.py`, `check-yaml.lean`
+
+Managing and tracking technical debt
+- `update_nolints_CI.sh` (maintenance, runs once a week)
+- `technical-debt-metrics.sh`
+- `init_creation.sh` (supposed to be run manually; might be removed soon?)
+
+- `create-adaptation-pr.sh`, `lean-pr-testing-comments.sh`
+
+- `bench_summary.lean`, `autolabel.lean`, `get_tlabel.sh`
+
+- `install_debian.sh`, `install_macos.sh`
+
+- `declarations_diff.sh`, `count-trans-deps.py`, `import_trans_difference.sh`, `update_PR_comment.sh`;
+`import-graph-report.py`
+
+
+Data files with exclusions for style linters: all of these should tend to zero over time
+- `nolints.json`: TODO document!
+- `no_lints_prime_decls.txt`: TODO document this
+
+Other
+- `fix_unused.py`

scripts/lint-style.lean

@@ -12,10 +12,34 @@ import Cli.Basic
 
 This files defines the `lint-style` executable which runs all text-based style linters.
 The linters themselves are defined in `Mathlib.Tactic.Linter.TextBased`.
+
+In addition, this checks that every file in `scripts` is documented in its top-level README.
 -/
 
 open Cli Mathlib.Linter.TextBased
 
+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 ← (walkDir "scripts" fun p ↦ pure (p.components.getD 1 "" != "bench"))
+  let allScripts := allScripts.erase ("scripts" / "bench")|>.erase ("scripts" / "README.md")
+  -- Check if the README text contains each file enclosed in backticks.
+  let readme : String ← IO.FS.readFile ("scripts" / "README.md")
+  IO.println s!"found {allScripts.size} scripts: {",".intercalate (allScripts.map (·.toString)).toList}"
+  -- These are data files for linter exceptions: don't complain about these *for now*.
+  let dataFiles := #["noshake.json", "nolints-style.txt"]
+  -- For now, there are no scripts in sub-directories that should be documented.
+  let fileNames := allScripts.map (·.fileName.get!)
+  let undocumented := fileNames.filter fun script ↦
+    !readme.containsSubstr s!"`{script}`" && !dataFiles.contains script
+  if undocumented.size > 0 then
+    IO.println s!"error: found {undocumented.size} undocumented scripts: \
+      please describe the scripts in 'scripts/README.md'\n\
+      {String.intercalate "," undocumented.toList}"
+  return undocumented.size > 0
+
 /-- Implementation of the `lint-style` command line program. -/
 def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do
   let style : ErrorFormat := match args.hasFlag "github" with
@@ -26,15 +50,16 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do
   let mut allModules := #[]
   for s in ["Archive.lean", "Counterexamples.lean", "Mathlib.lean"] do
     allModules := allModules.append ((← IO.FS.lines s).map (·.stripPrefix "import "))
-  -- note: since we manually add "Batteries" to "Mathlib.lean", we remove it here manually
+  -- Note: since we manually add "Batteries" to "Mathlib.lean", we remove it here manually.
   allModules := allModules.erase "Batteries"
-  let numberErrorFiles ← lintModules allModules style fix
+  let mut numberErrors := 0 --← lintModules allModules style fix
+  if !(← checkScriptsDocumented) then numberErrors := numberErrors + 1
   -- If run with the `--fix` argument, return a zero exit code.
   -- Otherwise, make sure to return an exit code of at most 125,
   -- so this return value can be used further in shell scripts.
   if args.hasFlag "fix" then
     return 0
-  else return min numberErrorFiles 125
+  else 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?