Improve error messages in sorry extraction

Author: Paul-Lez

LeanUtils/ExtractSorry.lean

@@ -14,7 +14,6 @@ def ppGoalIfNoMVar (mvar : MVarId) : MetaM (Option Format) := do
   catch _ =>
     return none
 
-
 /-- Traverses an info tree and applies `x` on the type of each sorry,
 while iteratively reconstructing the MetaM context.
 
@@ -37,9 +36,10 @@ where
 def extractSorries (T : InfoTree) : IO (List <| SorryData Format) :=
   traverseInfoTree ppGoalIfNoMVar T
 
-
 /-- `parseFile myLeanFile` extracts the sorries contained in the Lean file `myLeanFile`. -/
 def parseFile (path : System.FilePath) : IO (List ParsedSorry) := do
+  -- Throw an error if the oleans of the file can't be found...
+  path.checkOLeans
   let (fileMap, trees) ← extractInfoTrees path
   -- TODO(Paul-Lez): here ideally we should filter `trees` so we only run
   -- `extractSorries` on infotrees that arise from theorems/lemmas/definitions/...

LeanUtils/Utils.lean

@@ -56,7 +56,11 @@ def SorryData.toParsedSorry {Out} [ToString Out] (fileMap : FileMap) : SorryData
 instance : ToString ParsedSorry where
   toString a := ToString.toString <| ToJson.toJson a
 
-#check Frontend.State
+def Lean.Message.printIfError (m : Message) : IO Unit := do
+  if m.severity == .error then IO.eprintln <| ← m.toString
+
+def Lean.MessageLog.printErrors (m : MessageLog) : IO Unit := do
+  for message in m.reported ++ m.unreported do message.printIfError
 
 /-- `extractInfoTree myLeanFile` takes as input the path to a Lean file and outputs
 the infotrees of the file, together with the `FileMap`. -/
@@ -65,15 +69,18 @@ def extractInfoTrees (fileName : System.FilePath) : IO (FileMap × List InfoTree
   let inputCtx := Parser.mkInputContext input fileName.toString
   let (header, parserState, messages) ← Parser.parseHeader inputCtx
   if Lean.MessageLog.hasErrors messages then
-    IO.println s!"Ran into errors while parsing the header of {fileName}"
+    IO.eprintln s!"Ran into errors while parsing the header of {fileName}"
+    MessageLog.printErrors messages
   -- TODO: do we need to specify the main module here?
   let (env, messages) ← processHeader header {} messages inputCtx
   if Lean.MessageLog.hasErrors messages then
-    IO.println s!"Ran into errors whist processing the header of {fileName}"
+    IO.eprintln s!"Ran into errors whist processing the header of {fileName}"
+    MessageLog.printErrors messages
   let commandState := Command.mkState env messages
   let frontendState ← IO.processCommands inputCtx parserState commandState
   if Lean.MessageLog.hasErrors frontendState.commandState.messages then
-    IO.println s!"Ran into errors whist processing the commands in {fileName}"
+    IO.eprintln s!"Ran into errors whist processing the commands in {fileName}"
+    MessageLog.printErrors messages
   let fileMap := FileMap.ofString input
   return (fileMap, frontendState.commandState.infoState.trees.toList)
 
@@ -117,3 +124,6 @@ def getProjectSearchPath (path : System.FilePath) : IO (System.SearchPath) := do
   let paths ← getAllLakePaths rootDir
   let originalSearchPath ← getBuiltinSearchPath (← findSysroot)
   return originalSearchPath.append paths.toList
+
+def System.FilePath.checkOLeans (path : System.FilePath) : IO Unit := do
+  discard <| Lean.findOLean (← moduleNameOfFileName path none)

bins/ExtractSorry.lean

@@ -13,6 +13,7 @@ only have to run them once per project, rather than once per Lean file.
 -/
 
 def main (args : List String) : IO Unit := do
+  Lean.initSearchPath (← Lean.findSysroot)
   logRun
   if let some path := args[0]? then
     IO.println s!"Running sorry extraction on file {path}."