Merge pull request 'feat: Error reporting in frontend' (#107) from frontend/error into dev

Reviewed-on: #107
This commit is contained in:
Leni Aniva 2024-10-05 22:39:23 -07:00
commit 22ddfaaf21
4 changed files with 63 additions and 44 deletions

View File

@ -42,6 +42,14 @@ structure CompilationStep where
msgs : List Message
trees : List Elab.InfoTree
namespace CompilationStep
@[export pantograph_frontend_compilation_step_message_strings_m]
def messageStrings (step: CompilationStep) : IO (Array String) := do
List.toArray <$> step.msgs.mapM (·.toString)
end CompilationStep
/--
Process one command, returning a `CompilationStep` and

View File

@ -298,11 +298,18 @@ structure InvokedTactic where
goalAfter: String
tactic: String
deriving Lean.ToJson
structure FrontendProcessResult where
structure CompilationUnit where
-- String boundaries of compilation units
units: List (Nat × Nat)
boundary: (Nat × Nat)
-- Tactic invocations
invocations?: Option (List InvokedTactic) := .none
goalStates?: Option (List (Nat × Array Goal)) := .none
goalStateId?: Option Nat := .none
goals: Array Goal := #[]
messages: Array String := #[]
deriving Lean.ToJson
structure FrontendProcessResult where
units: List CompilationUnit
deriving Lean.ToJson
abbrev CR α := Except InteractionError α

View File

@ -216,35 +216,36 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let env ← Lean.MonadEnv.getEnv
pure <| .some env
let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
let m := Frontend.mapCompilationSteps λ step => do
let unitBoundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
let tacticInvocations ← if args.invocations then
Frontend.collectTacticsFromCompilationStep step
let frontendM := Frontend.mapCompilationSteps λ step => do
let boundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
let invocations?: Option (List Protocol.InvokedTactic) ← if args.invocations then
let invocations ← Frontend.collectTacticsFromCompilationStep step
pure $ .some invocations
else
pure []
pure .none
let sorrys := if args.sorrys then
Frontend.collectSorrys step
else
[]
return (unitBoundary, tacticInvocations, sorrys)
let li ← m.run context |>.run' state
let units := li.map λ (unit, _, _) => unit
let invocations? := if args.invocations then
.some $ li.bind λ (_, invocations, _) => invocations
else
.none
let goalStates? ← if args.sorrys then do
let stateIds ← li.filterMapM λ (_, _, sorrys) => do
if sorrys.isEmpty then
return .none
let messages ← step.messageStrings
return (boundary, invocations?, sorrys, messages)
let li ← frontendM.run context |>.run' state
let units ← li.mapM λ (boundary, invocations?, sorrys, messages) => do
let (goalStateId?, goals) ← if sorrys.isEmpty then do
pure (.none, #[])
else do
let goalState ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
let stateId ← newGoalState goalState
let goals ← goalSerialize goalState options
return .some (stateId, goals)
pure $ .some stateIds
else
pure .none
return .ok { units, invocations?, goalStates? }
pure (.some stateId, goals)
return {
boundary,
invocations?,
goalStateId?,
goals,
messages,
}
return .ok { units }
catch e =>
return .error $ errorI "frontend" (← e.toMessageData.toString)

View File

@ -176,19 +176,21 @@ def test_frontend_process : Test :=
("sorrys", .bool false),
]
({
units := [(0, file.utf8ByteSize)],
invocations? := .some [
{
goalBefore := "⊢ ∀ (p : Prop), p → p",
goalAfter := goal1,
tactic := "intro p h",
},
{
goalBefore := goal1 ,
goalAfter := "",
tactic := "exact h",
},
]
units := [{
boundary := (0, file.utf8ByteSize),
invocations? := .some [
{
goalBefore := "⊢ ∀ (p : Prop), p → p",
goalAfter := goal1,
tactic := "intro p h",
},
{
goalBefore := goal1 ,
goalAfter := "",
tactic := "exact h",
},
]
}],
}: Protocol.FrontendProcessResult),
]
@ -212,13 +214,14 @@ def test_frontend_process_sorry : Test :=
("sorrys", .bool true),
]
({
units := [
(0, solved.utf8ByteSize),
(solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
],
goalStates? := [
(0, #[goal1]),
]
units := [{
boundary := (0, solved.utf8ByteSize),
}, {
boundary := (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
goalStateId? := .some 0,
goals := #[goal1],
messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
}],
}: Protocol.FrontendProcessResult),
]