Lean4
@[inherit_doc Mathlib.Linter.linter.style.commandStart]
def commandStartLinter : Linter where
run :=
withSetOptionIn fun stx ↦ do
unless Linter.getLinterValue linter.style.commandStart (← getLinterOptions) do
return
if (← get).messages.hasErrors then
return
if stx.find? (·.isOfKind ``runCmd) |>.isSome then
return
-- If a command does not start on the first column, emit a warning.
if let some pos := stx.getPos? then
let colStart := ((← getFileMap).toPosition pos).column
if colStart ≠ 0 then
Linter.logLint linter.style.commandStart stx
m! "'{stx }' starts on column {colStart}, \
but all commands should start at the beginning of the line."
if stx.find? (·.isOfKind `Lean.Parser.Command.macro_rules) |>.isSome then
return
let some upTo := CommandStart.endPos stx |
return
let fmt : Option Format :=
←
try
liftCoreM <| PrettyPrinter.ppCategory `command stx
catch _ =>
Linter.logLintIf linter.style.commandStart.verbose (stx.getHead?.getD stx)
m!"The `commandStart` linter had some parsing issues: \
feel free to silence it and report this error!"
return none
if let some fmt := fmt then
let st := fmt.pretty
let origSubstring := stx.getSubstring?.getD default
let orig := origSubstring.toString
let scan := parallelScan orig st
let docStringEnd := stx.find? (·.isOfKind ``Parser.Command.docComment) |>.getD default
let docStringEnd := docStringEnd.getTailPos? |>.getD default
let forbidden := getUnlintedRanges unlintedNodes ∅ stx
for s in scan do
let center := origSubstring.stopPos - s.srcEndPos
let rg : String.Range := ⟨center, center + s.srcEndPos - s.srcStartPos + ⟨1⟩⟩
if s.msg.startsWith "Oh no" then
Linter.logLintIf linter.style.commandStart.verbose (.ofRange rg)
m!"This should not have happened: please report this issue!"
Linter.logLintIf linter.style.commandStart.verbose (.ofRange rg)
m! "Formatted string:\n{fmt }\nOriginal string:\n{origSubstring}"
continue
unless isOutside forbidden rg do
continue
unless rg.stop ≤ upTo do
return
unless docStringEnd ≤ rg.start do
return
let ctx :=
4 -- the number of characters after the mismatch that linter prints
let srcWindow := mkWindow orig s.srcNat (ctx + s.length)
let expectedWindow := mkWindow st s.fmtPos (ctx + (1))
Linter.logLint linter.style.commandStart (.ofRange rg)
m! "{s.msg } in the source\n\n\
This part of the code\n '{srcWindow }'\n\
should be written as\n '{expectedWindow}'\n"
Linter.logLintIf linter.style.commandStart.verbose (.ofRange rg)
m! "Formatted string:\n{fmt }\nOriginal string:\n{origSubstring}"
