feat: Error reporting in frontend #107

Merged
aniva merged 1 commits from frontend/error into dev 2024-10-05 22:39:24 -07:00
4 changed files with 63 additions and 44 deletions

View File

@ -42,6 +42,14 @@ structure CompilationStep where
msgs : List Message msgs : List Message
trees : List Elab.InfoTree 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 Process one command, returning a `CompilationStep` and

View File

@ -298,11 +298,18 @@ structure InvokedTactic where
goalAfter: String goalAfter: String
tactic: String tactic: String
deriving Lean.ToJson deriving Lean.ToJson
structure FrontendProcessResult where
structure CompilationUnit where
-- String boundaries of compilation units -- String boundaries of compilation units
units: List (Nat × Nat) boundary: (Nat × Nat)
-- Tactic invocations
invocations?: Option (List InvokedTactic) := .none 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 deriving Lean.ToJson
abbrev CR α := Except InteractionError α abbrev CR α := Except InteractionError α

View File

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

View File

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