From bace69d44daa1b11a8fef70d6afd3608d297aed0 Mon Sep 17 00:00:00 2001 From: Paul-Lez Date: Wed, 26 Nov 2025 16:08:43 +0000 Subject: [PATCH 1/2] Improve error messages in sorry extraction --- LeanUtils/ExtractSorry.lean | 4 ++-- LeanUtils/Utils.lean | 18 ++++++++++++++---- bins/ExtractSorry.lean | 1 + 3 files changed, 17 insertions(+), 6 deletions(-) diff --git a/LeanUtils/ExtractSorry.lean b/LeanUtils/ExtractSorry.lean index a30429e..9760732 100644 --- a/LeanUtils/ExtractSorry.lean +++ b/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/... diff --git a/LeanUtils/Utils.lean b/LeanUtils/Utils.lean index 9ac154b..9ec5f5d 100644 --- a/LeanUtils/Utils.lean +++ b/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) diff --git a/bins/ExtractSorry.lean b/bins/ExtractSorry.lean index 49e60d2..7a05394 100644 --- a/bins/ExtractSorry.lean +++ b/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}." From de76c24ea981b1af32f1ad32575adc5fd3dc0ccd Mon Sep 17 00:00:00 2001 From: Paul-Lez Date: Wed, 26 Nov 2025 16:13:13 +0000 Subject: [PATCH 2/2] add printing --- LeanUtils/Utils.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanUtils/Utils.lean b/LeanUtils/Utils.lean index 6604327..8aa01d1 100644 --- a/LeanUtils/Utils.lean +++ b/LeanUtils/Utils.lean @@ -101,7 +101,7 @@ def extractInfoTrees (fileName : System.FilePath) : IO (FileMap × List InfoTree let frontendState ← IO.processCommands inputCtx parserState commandState if Lean.MessageLog.hasErrors frontendState.commandState.messages then IO.eprintln s!"Ran into errors whist processing the commands in {fileName}" - MessageLog.printErrors messages + MessageLog.printErrors frontendState.commandState.messages let fileMap := FileMap.ofString input return (fileMap, frontendState.commandState.infoState.trees.toList)