Header linter can repeatedly reparse Verso document bodies

[ejgallego]

Short version

linter.style.header can spend significant time on a valid Verso/Blueprint
document module that does not use Mathlib's file-header layout.

The warning itself is expected: the file does not have a Mathlib copyright
header and module docstring immediately after the imports. The concern is the
failure path. Instead of reporting the first non-import command and stopping
there, the linter appears to repeatedly parse the later document body as
ordinary Lean commands.

In practice, this means Blueprint syntax such as %%% front matter and
{include ...} directives is parsed by the normal Lean module parser, fails,
falls back, and is then tried again for the next early command.

Observed behavior

In the file where this was found, a 15 second run emitted the same three-part
diagnostic once for each ordinary command before the document body:

Copyright too short!
The module doc-string for a file should be the first command after the imports.
linter.style.header:26:0: error: unexpected token '%'; expected command

Those repeats corresponded to:

open Verso.Genre
open Verso.Genre.Manual hiding citep citet citehere
open Informal
set_option doc.verso true
set_option linter.style.longLine false

An isolated compile of the file timed out after 45 seconds with the header
linter enabled. The same compile finished in 21.9 seconds with only
weak.linter.style.header=false. Adding a normal module docstring before the
open commands also made it finish in about the same time.

Likely cause

From the implementation, headerLinter runs once per command. If the file has
no Markdown or Verso module docstring near the top, it uses the end of the file
as the parse boundary and calls Parser.testParseModule on that prefix.

For a Verso/Blueprint document module, that prefix includes the document body.
At that point the linter is no longer checking only the header: it is asking
Lean's regular command parser to parse document markup that belongs to Verso.

It seems sufficient for the linter to report the missing Mathlib-style module
docstring once, after seeing the first non-import command.

Possible fix

Lean's linter framework runs command linters after every command. That makes
sense for declaration-local checks, but the header linter is checking a
file-level invariant.

Within the current Lean linter API, this would not reduce how often
Lean invokes the callback. Lean will still call headerLinter after each
command. Mathlib already has a closely related pattern:
Mathlib.Tactic.Linter.DeprecatedModule uses an IO.Ref to do real work only
on the first non-import command.

linter.style.header could use the same pattern. Conceptually:

initialize isLaterCommand : IO.Ref Bool ← IO.mkRef false

def headerLinter : Linter where run := withSetOptionIn fun stx => do
  -- existing option / library-root / error checks
  let laterCommand ← isLaterCommand.get
  if laterCommand || (Parser.isTerminalCommand stx && !laterCommand) then
    return
  isLaterCommand.set true

  -- do the file-header check once

That makes the expensive part of the linter one-shot, at the first command
after the import header. At that point the header is already decidable: either
that command is a module docstring, or the file is missing the expected
Mathlib-style module docstring.

One additional detail: on that single run, the no-module-docstring
case should not use the end of the file as the parse boundary. If no module
docstring has been found at the first post-import command, the linter can parse
only the import header plus the existing sentinel section and report the
missing module docstring. It does not need to parse the rest of the file.

Reducing the actual callback invocation frequency would require a new Lean-side
file/header-linter hook, for example a hook after parseHeader. For this issue,
following the existing deprecated.module one-shot pattern should be enough.

Minimal repro project

lean-toolchain:

leanprover/lean4:v4.30.0

lakefile.lean:

import Lake
open Lake DSL

require VersoBlueprint from git
  "https://github.com/leanprover/verso-blueprint.git" @ "v4.30.0"
require mathlib from git
  "https://github.com/leanprover-community/mathlib4" @ "v4.30.0"

package HeaderLinterVersoRepro where
  leanOptions := #[
    ⟨`experimental.module, true⟩,
    ⟨`weak.linter.style.header, true⟩
  ]

@[default_target]
lean_lib HeaderLinterVersoRepro where
  roots := #[`HeaderLinterVersoRepro]

HeaderLinterVersoRepro.lean:

import HeaderLinterVersoRepro.Repro

HeaderLinterVersoRepro/ReproChapter.lean:

import Verso
import VersoManual
import VersoBlueprint

open Verso.Genre
open Verso.Genre.Manual
open Informal

set_option doc.verso true

#doc (Manual) "Included chapter" =>

%%%
tag := "included"
%%%

# Included chapter

This is a small included chapter.

HeaderLinterVersoRepro/Repro.lean:

import Mathlib.Tactic.Linter.Header
import Verso
import VersoManual
import VersoBlueprint
import HeaderLinterVersoRepro.ReproChapter

open Verso.Genre
open Verso.Genre.Manual
open Informal

set_option doc.verso true

#doc (Manual) "Header linter repro" =>

%%%
shortTitle := "Header linter repro"
%%%

# Overview

This is a valid Blueprint document module, but it is not a Mathlib-style source
file with a module docstring immediately after the imports.

{include 0 HeaderLinterVersoRepro.ReproChapter}

{blueprint_graph}

{blueprint_summary}

Then run:

lake update
lake exe cache get
timeout 45s lake build +HeaderLinterVersoRepro.Repro

The first run may spend time fetching dependencies; the interesting behavior is
the target compile after dependencies are warm.

Expected behavior

Once the first non-import command is known not to be a module docstring, the
linter should report that cheaply. It should not repeatedly parse the later
document body or emit the same parser diagnostics once per early command.

Workaround

For these document modules we are disabling only this linter:

⟨`weak.linter.style.header, false⟩