From e3d866bc03bae856b58be156d18fc893bed3dbbb Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 10 Aug 2021 21:47:59 -0400 Subject: [PATCH] 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. --- src/Init/Data/Format/Basic.lean | 4 ++-- src/Lean/Message.lean | 7 ++++++- src/Lean/Util/Trace.lean | 4 ++-- src/Lean/Widget/Data.lean | 29 +++++++++++++---------------- src/Lean/Widget/ExprWithCtx.lean | 15 +++++++++------ src/Lean/Widget/TaggedText.lean | 17 ++++++++++------- 6 files changed, 42 insertions(+), 34 deletions(-) diff --git a/src/Init/Data/Format/Basic.lean b/src/Init/Data/Format/Basic.lean index b2d685f525..3fc386e58c 100644 --- a/src/Init/Data/Format/Basic.lean +++ b/src/Init/Data/Format/Basic.lean @@ -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) diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 4d74369f0d..3e261db7c3 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -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 diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index dcaed0cd86..67ae1512e9 100644 --- a/src/Lean/Util/Trace.lean +++ b/src/Lean/Util/Trace.lean @@ -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 diff --git a/src/Lean/Widget/Data.lean b/src/Lean/Widget/Data.lean index 6fe6bc8259..7cbf51a4d9 100644 --- a/src/Lean/Widget/Data.lean +++ b/src/Lean/Widget/Data.lean @@ -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 diff --git a/src/Lean/Widget/ExprWithCtx.lean b/src/Lean/Widget/ExprWithCtx.lean index 570c1c6565..d467129586 100644 --- a/src/Lean/Widget/ExprWithCtx.lean +++ b/src/Lean/Widget/ExprWithCtx.lean @@ -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 diff --git a/src/Lean/Widget/TaggedText.lean b/src/Lean/Widget/TaggedText.lean index 564bf180a6..01ed95fe74 100644 --- a/src/Lean/Widget/TaggedText.lean +++ b/src/Lean/Widget/TaggedText.lean @@ -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 :=