Lean4
@[inherit_doc Mathlib.Linter.linter.style.header]
def headerLinter : Linter where
run :=
withSetOptionIn fun stx ↦ do
let mainModule ← getMainModule
let inMathlib? :=
←
match ← inMathlibRef.get with
| some d => return d
| none => do
let val ← isInMathlib mainModule
inMathlibRef.set (some val)
return val
unless
inMathlib? || mainModule == `MathlibTest.Header || mainModule == `MathlibTest.DirectoryDependencyLinter.Test do
return
unless getLinterValue linter.style.header (← getLinterOptions) do
return
if (← get).messages.hasErrors then
return
-- `Mathlib.lean` imports `Mathlib.Tactic`, which the broad imports check below would flag.
-- Since that file is imports-only, we can simply skip linting it.
if mainModule == `Mathlib then
return
let fm ← getFileMap
let md := (getMainModuleDoc (← getEnv)).toArray
let firstDocModPos :=
match md[0]? with
| none => fm.positions.back!
| some doc => fm.ofPosition doc.declarationRange.endPos
unless stx.getTailPos?.getD default ≤ firstDocModPos do
return
-- We try to parse the file up to `firstDocModPos`.
let upToStx ←
parseUpToHere firstDocModPos <|>
(do
-- If parsing failed, there is some command which is not a module docstring.
-- In that case, we parse until the end of the imports and add an extra `section` afterwards,
-- so we trigger a "no module doc-string" warning.
let fil ← getFileName
let (stx, _) ← Parser.parseHeader { inputString := fm.source, fileName := fil, fileMap := fm }
parseUpToHere (stx.raw.getTailPos?.getD default) "\nsection")
let importIds := getImportIds upToStx
broadImportsCheck importIds mainModule
duplicateImportsCheck importIds
let errors ← directoryDependencyCheck mainModule
if errors.size > 0 then
let mut msgs := ""
for msg in errors do
msgs := msgs ++ "\n\n" ++ (← msg.toString)
Linter.logLint linter.directoryDependency stx msgs.trimLeft
let afterImports := firstNonImport? upToStx
if afterImports.isNone then
return
let copyright :=
match upToStx.getHeadInfo with
| .original lead .. => lead.toString
| _ =>
""
-- Report any errors about the copyright line.
if mainModule != `Mathlib.Init then
for (stx, m) in copyrightHeaderChecks copyright do
Linter.logLint linter.style.header stx m! "* '{stx.getAtomVal }':\n{m}\n"
match afterImports with
| none =>
return
| some (.node _ ``Lean.Parser.Command.moduleDoc _) =>
return
| some rest =>
Linter.logLint linter.style.header rest
m! "The module doc-string for a file should be the first command after the imports.\n\
Please, add a module doc-string before `{stx}`."
