feat: initial TraceExplorer
Motivation: trace messages from systems such as instance synthesis or defeq checks can be massive and it is hard to find the relevant info within. We provide an interactive TraceExplorer component to do this.
This commit is contained in:
Wojciech Nawrocki
Leonardo de Moura
parent
8207ca6493
commit
e3d866bc03
6 changed files with 42 additions and 34 deletions
|
|
@ -172,8 +172,8 @@ private partial def be (w : Nat) [Monad m] [MonadPrettyFormat m] : List WorkGrou
|
|||
else
|
||||
pushGroup flb [{ i with f }] (gs' is) w >>= be w
|
||||
|
||||
def prettyM (f : Format) (w : Nat) [Monad m] [MonadPrettyFormat m] : m Unit :=
|
||||
be w [{ flb := FlattenBehavior.allOrNone, flatten := false, items := [{ f := f, indent := 0, activeTags := 0 }]}]
|
||||
def prettyM (f : Format) (w : Nat) (indent : Nat := 0) [Monad m] [MonadPrettyFormat m] : m Unit :=
|
||||
be w [{ flb := FlattenBehavior.allOrNone, flatten := false, items := [{ f := f, indent, activeTags := 0 }]}]
|
||||
|
||||
@[inline] def bracket (l : String) (f : Format) (r : String) : Format :=
|
||||
group (nest l.length $ l ++ f ++ r)
|
||||
|
|
|
|||
|
|
@ -116,7 +116,12 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
|
|||
| nCtx, some ctx, ofGoal mvarId => ppGoal (mkPPContext nCtx ctx) mvarId
|
||||
| nCtx, _, withContext ctx d => formatAux nCtx ctx d
|
||||
| _, ctx, withNamingContext nCtx d => formatAux nCtx ctx d
|
||||
| nCtx, ctx, tagged _ d => formatAux nCtx ctx d
|
||||
| nCtx, ctx, tagged t d =>
|
||||
if let Name.str cls "_traceCtx" _ := t then do
|
||||
let d₁ ← formatAux nCtx ctx d
|
||||
return f!"[{cls}] {d₁}"
|
||||
else
|
||||
formatAux nCtx ctx d
|
||||
| nCtx, ctx, nest n d => Format.nest n <$> formatAux nCtx ctx d
|
||||
| nCtx, ctx, compose d₁ d₂ => do let d₁ ← formatAux nCtx ctx d₁; let d₂ ← formatAux nCtx ctx d₂; pure $ d₁ ++ d₂
|
||||
| nCtx, ctx, group d => Format.group <$> formatAux nCtx ctx d
|
||||
|
|
|
|||
|
|
@ -91,7 +91,7 @@ private def addNode (oldTraces : PersistentArray TraceElem) (cls : Name) (ref :
|
|||
if traces.isEmpty then
|
||||
oldTraces
|
||||
else
|
||||
let d := MessageData.tagged cls m!"[{cls}] {MessageData.node (traces.toArray.map fun elem => elem.msg)}"
|
||||
let d := MessageData.tagged (cls ++ `_traceCtx) (MessageData.node (traces.toArray.map fun elem => elem.msg))
|
||||
oldTraces.push { ref := ref, msg := d }
|
||||
|
||||
private def getResetTraces : m (PersistentArray TraceElem) := do
|
||||
|
|
@ -106,7 +106,7 @@ def addTrace (cls : Name) (msg : MessageData) : m Unit := do
|
|||
let ref ← getRef
|
||||
let msg ← addMessageContext msg
|
||||
let msg := addTraceOptions msg
|
||||
modifyTraces fun traces => traces.push { ref := ref, msg := MessageData.tagged cls m!"[{cls}] {msg}" }
|
||||
modifyTraces fun traces => traces.push { ref := ref, msg := MessageData.tagged (cls ++ `_traceMsg) m!"[{cls}] {msg}" }
|
||||
where
|
||||
addTraceOptions : MessageData → MessageData
|
||||
| MessageData.withContext ctx msg => MessageData.withContext { ctx with opts := ctx.opts.setBool `pp.analyze false } msg
|
||||
|
|
|
|||
|
|
@ -42,15 +42,12 @@ def pretty (g : InteractiveGoal) : String :=
|
|||
|
||||
end InteractiveGoal
|
||||
|
||||
-- TODO
|
||||
structure LazyTrace where
|
||||
contents : String
|
||||
deriving Inhabited, FromJson, ToJson
|
||||
deriving instance RpcEncoding with { withRef := true } for MessageData
|
||||
|
||||
inductive MsgEmbed where
|
||||
| expr : CodeWithInfos → MsgEmbed
|
||||
| goal : InteractiveGoal → MsgEmbed
|
||||
| lazyTrace : LazyTrace → MsgEmbed
|
||||
| lazyTrace : Nat → Name → WithRpcRef MessageData → MsgEmbed
|
||||
deriving Inhabited
|
||||
|
||||
namespace MsgEmbed
|
||||
|
|
@ -58,20 +55,20 @@ namespace MsgEmbed
|
|||
-- TODO(WN): `deriving RpcEncoding` for `inductive`
|
||||
private inductive RpcEncodingPacket where
|
||||
| expr : TaggedText Lsp.RpcRef → RpcEncodingPacket
|
||||
| goal : Nat → RpcEncodingPacket
|
||||
| lazyTrace : LazyTrace → RpcEncodingPacket
|
||||
| goal : Nat → RpcEncodingPacket -- TODO
|
||||
| lazyTrace : Nat → Name → Lsp.RpcRef → RpcEncodingPacket
|
||||
deriving Inhabited, FromJson, ToJson
|
||||
|
||||
instance : RpcEncoding MsgEmbed RpcEncodingPacket where
|
||||
rpcEncode a := match a with
|
||||
| expr t => return RpcEncodingPacket.expr (← rpcEncode t)
|
||||
| goal t => return RpcEncodingPacket.goal 0
|
||||
| lazyTrace t => return RpcEncodingPacket.lazyTrace (← rpcEncode t)
|
||||
| expr t => return RpcEncodingPacket.expr (← rpcEncode t)
|
||||
| goal t => return RpcEncodingPacket.goal 0
|
||||
| lazyTrace col n t => return RpcEncodingPacket.lazyTrace col n (← rpcEncode t)
|
||||
|
||||
rpcDecode a := match a with
|
||||
| RpcEncodingPacket.expr t => return expr (← rpcDecode t)
|
||||
| RpcEncodingPacket.goal t => return unreachable!
|
||||
| RpcEncodingPacket.lazyTrace t => return lazyTrace (← rpcDecode t)
|
||||
| RpcEncodingPacket.expr t => return expr (← rpcDecode t)
|
||||
| RpcEncodingPacket.goal t => return unreachable!
|
||||
| RpcEncodingPacket.lazyTrace col n t => return lazyTrace col n (← rpcDecode t)
|
||||
|
||||
end MsgEmbed
|
||||
|
||||
|
|
@ -85,9 +82,9 @@ open MsgEmbed
|
|||
|
||||
def pretty (msg : InteractiveMessage) : String :=
|
||||
let tt : TaggedText MsgEmbed := msg.rewrite fun
|
||||
| expr tt, _ => TaggedText.text tt.stripTags
|
||||
| goal g, _ => TaggedText.text g.pretty
|
||||
| lazyTrace t, _ => TaggedText.text t.contents
|
||||
| expr tt, _ => TaggedText.text tt.stripTags
|
||||
| goal g, _ => TaggedText.text g.pretty
|
||||
| lazyTrace _ _ _, subTt => subTt
|
||||
tt.stripTags
|
||||
|
||||
end InteractiveMessage
|
||||
|
|
|
|||
|
|
@ -84,12 +84,12 @@ def formatExplicitInfos (e : Expr) : MetaM (Format × Std.RBMap Nat Elab.Info co
|
|||
formatWithOpts e optsPerPos
|
||||
|
||||
/-- Tags a pretty-printed `Expr` with infos from the delaborator. -/
|
||||
partial def tagExprInfos (ctx : Elab.ContextInfo) (lctx : LocalContext) (infos : Std.RBMap Nat Elab.Info compare) (tt : TaggedText Nat)
|
||||
partial def tagExprInfos (ctx : Elab.ContextInfo) (lctx : LocalContext) (infos : Std.RBMap Nat Elab.Info compare) (tt : TaggedText (Nat × Nat))
|
||||
: CodeWithInfos :=
|
||||
go tt
|
||||
where
|
||||
go (tt : TaggedText Nat) :=
|
||||
tt.rewrite fun n subTt =>
|
||||
go (tt : TaggedText (Nat × Nat)) :=
|
||||
tt.rewrite fun (n, _) subTt =>
|
||||
match infos.find? n with
|
||||
| none => go subTt
|
||||
| some i => TaggedText.tag (WithRpcRef.mk { ctx, lctx, info := i }) (go subTt)
|
||||
|
|
@ -101,7 +101,8 @@ def inferType (e : Expr) : MetaM ExprWithCtx := do
|
|||
options := ← getOptions
|
||||
currNamespace := ← getCurrNamespace
|
||||
openDecls := ← getOpenDecls
|
||||
fileMap := arbitrary }
|
||||
fileMap := arbitrary
|
||||
}
|
||||
return { ctx, lctx := ← getLCtx, expr := e}
|
||||
|
||||
def tagged (e : Expr) : MetaM CodeWithInfos := do
|
||||
|
|
@ -113,7 +114,8 @@ def tagged (e : Expr) : MetaM CodeWithInfos := do
|
|||
options := ← getOptions
|
||||
currNamespace := ← getCurrNamespace
|
||||
openDecls := ← getOpenDecls
|
||||
fileMap := arbitrary }
|
||||
fileMap := arbitrary
|
||||
}
|
||||
tagExprInfos ctx (← getLCtx) infos tt
|
||||
|
||||
def taggedExplicit (e : Expr) : MetaM CodeWithInfos := do
|
||||
|
|
@ -125,7 +127,8 @@ def taggedExplicit (e : Expr) : MetaM CodeWithInfos := do
|
|||
options := ← getOptions
|
||||
currNamespace := ← getCurrNamespace
|
||||
openDecls := ← getOpenDecls
|
||||
fileMap := arbitrary }
|
||||
fileMap := arbitrary
|
||||
}
|
||||
tagExprInfos ctx (← getLCtx) infos tt
|
||||
|
||||
builtin_initialize
|
||||
|
|
|
|||
|
|
@ -72,23 +72,26 @@ instance [RpcEncoding α β] : RpcEncoding (TaggedText α) (TaggedText β) where
|
|||
rpcDecode a := a.mapM rpcDecode
|
||||
|
||||
private structure TaggedState where
|
||||
out : TaggedText Nat := TaggedText.text ""
|
||||
tagStack : List (Nat × TaggedText Nat) := []
|
||||
column : Nat := 0
|
||||
out : TaggedText (Nat × Nat) := TaggedText.text ""
|
||||
tagStack : List (Nat × Nat × TaggedText (Nat × Nat)) := []
|
||||
column : Nat := 0
|
||||
deriving Inhabited
|
||||
|
||||
instance : Std.Format.MonadPrettyFormat (StateM TaggedState) where
|
||||
pushOutput s := modify fun ⟨out, ts, col⟩ => ⟨out.appendText s, ts, col + s.length⟩
|
||||
pushNewline indent := modify fun ⟨out, ts, col⟩ => ⟨out.appendText ("\n".pushn ' ' indent), ts, indent⟩
|
||||
currColumn := return (←get).column
|
||||
startTag n := modify fun ⟨out, ts, col⟩ => ⟨TaggedText.text "", (n, out) :: ts, col⟩
|
||||
startTag n := modify fun ⟨out, ts, col⟩ => ⟨TaggedText.text "", (n, col, out) :: ts, col⟩
|
||||
endTags n := modify fun ⟨out, ts, col⟩ =>
|
||||
let (ended, left) := (ts.take n, ts.drop n)
|
||||
let out' := ended.foldl (init := out) fun acc (n, top) => top.appendTag n acc
|
||||
let out' := ended.foldl (init := out) fun acc (n, col', top) => top.appendTag (n, col') acc
|
||||
⟨out', left, col⟩
|
||||
|
||||
def prettyTagged (f : Format) (w : Nat := Std.Format.defWidth) : TaggedText Nat :=
|
||||
(f.prettyM w : StateM TaggedState Unit) {} |>.snd.out
|
||||
/-- The output is tagged with `(tag, indent)` where `tag` is from the input `Format` and `indent`
|
||||
is the indentation level at this point. The latter is used to print sub-trees accurately by passing
|
||||
it again as the `indent` argument. -/
|
||||
def prettyTagged (f : Format) (indent := 0) (w : Nat := Std.Format.defWidth) : TaggedText (Nat × Nat) :=
|
||||
(f.prettyM w indent : StateM TaggedState Unit) {} |>.snd.out
|
||||
|
||||
/-- Remove tags, leaving just the pretty-printed string. -/
|
||||
partial def stripTags (tt : TaggedText α) : String :=
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue