def Lake.mkParserErrorMessage (ictx : Lean.Parser.InputContext) (s : Lean.Parser.ParserState) (e : Lean.Parser.Error) : Lean.Message

def Lake.mkExceptionMessage (ictx : Lean.Parser.InputContext) (e : Lean.Exception) : Lean.Message

def Lake.mkMessageNoPos (ictx : Lean.Parser.InputContext) (data : Lean.MessageData) (severity : Lean.MessageSeverity := Lean.MessageSeverity.error) : Lean.Message

def Lake.mkMessageStringCore (severity : Lean.MessageSeverity) (fileName caption body : String) (pos : Lean.Position) (endPos? : Option Lean.Position := none) (infoWithPos : Bool := false) : String

def Lake.mkMessageString (msg : Lean.Message) (includeEndPos infoWithPos : Bool := false) : BaseIO String

def Lake.mkMessageLogString (log : Lean.MessageLog) : BaseIO String