ci: wire up lake lint to run runLinter (leanprover-community#39934)

This PR configures the `mathlib` package so that the standard `lake lint` command is equivalent to `lake exe runLinter Mathlib`, by setting

```
lintDriver := "batteries/runLinter"
lintDriverArgs := #["Mathlib"]
```

on the `package mathlib` declaration. `runLinter` is already a `lean_exe` in batteries, so the `<pkg>/<name>` syntax lets mathlib reuse it directly.

The CI workflows in `build_template.yml` and `nolints.yml` are also switched from invoking `lake exe runLinter [args] Mathlib` to `lake lint -- [args]` so there's a single source of truth for "lint mathlib", and so that local users get the same behaviour as CI.

### Behavior change for local users

Before this PR, `lake lint` in a Mathlib checkout errored out with "no lint driver configured" and was essentially unused. After this PR, `lake lint` runs the full Batteries linter over all of Mathlib, which is a substantial multi-minute job. Anyone who has scripts or muscle memory expecting `lake lint` to be a no-op should be aware. The previous direct invocation, `lake exe runLinter Mathlib`, continues to work for anyone who prefers it.

The `scripts/bench/lint/` benchmark intentionally keeps the direct `lake exe runLinter Mathlib` invocation so its measurements are not affected by anything `lake lint` may do above the linter.

Motivated by a recent Zulip discussion in which it became clear that very few people know `lake lint` exists, partly because few packages bother to configure a lint driver:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Using.20.60lake.20test.60.20effectively

Companion to leanprover/reference-manual#855 (which documents the mechanism in the Lean reference manual).

🤖 Prepared with Claude Code

Author: kim-em

.github/workflows/build_template.yml

@@ -513,19 +513,19 @@ jobs:
         run: |
           cd pr-branch
           set -o pipefail
-          # Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
+          # If lint fails because the PR predates lake-lint configuration or the
+          # old --trace argument-parsing behavior, ask the author to merge master.
           # We use .lake/ for the output file because landrun restricts /tmp access
           for attempt in 1 2; do
-            if timeout 10m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
+            if timeout 10m env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake lint -- --trace 2>&1 | tee ".lake/lint_output_attempt_${attempt}.txt"; then
               break
             fi
             status=${PIPESTATUS[0]}
-            if grep -q "cannot parse arguments" ".lake/lint_output_attempt_${attempt}.txt"; then
+            if grep -qE "cannot parse arguments|no lint driver configured" ".lake/lint_output_attempt_${attempt}.txt"; then
               echo ""
               echo "=============================================================================="
-              echo "ERROR: Your branch uses an older version of runLinter that doesn't support"
-              echo "the --trace flag. Please merge 'master' into your PR branch to get the"
-              echo "updated linter, then push again."
+              echo "ERROR: Your branch predates the current 'lake lint' configuration."
+              echo "Please merge 'master' into your PR branch and push again."
               echo ""
               echo "You can do this with:"
               echo "  git fetch upstream"

.github/workflows/nolints.yml

@@ -26,7 +26,7 @@ jobs:
       - name: update nolints.json
         shell: bash
         run: |
-          env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --trace --update Mathlib
+          env LEAN_ABORT_ON_PANIC=1 lake lint -- --trace --update
 
       - name: Generate app token
         id: app-token

lakefile.lean

@@ -48,6 +48,8 @@ abbrev mathlibLeanOptions := #[
 
 package mathlib where
   testDriver := "MathlibTest"
+  lintDriver := "batteries/runLinter"
+  lintDriverArgs := #["Mathlib"]
   -- These are additional settings which do not affect the lake hash,
   -- so they can be enabled in CI and disabled locally or vice versa.
   -- Warning: Do not put any options here that actually change the olean files,