From 38cff088883e4eb9654e2d1a17f84d226ac4efe3 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 22 Nov 2024 18:12:30 +0100 Subject: [PATCH] feat: creation and reporting for asynchronous elaboration tasks (#6170) This PR adds core metaprogramming functions for forking off background tasks from elaboration such that their results are visible to reporting and the language server --- src/Lean/CoreM.lean | 83 ++++++++++++- src/Lean/Elab/Command.lean | 114 ++++++++++-------- src/Lean/Elab/Term.lean | 20 +++ src/Lean/Language/Basic.lean | 25 ++-- src/Lean/Language/Lean.lean | 66 ++++++---- src/Lean/Language/Lean/Types.lean | 5 +- src/Lean/Language/Util.lean | 29 +++++ src/Lean/Util/Trace.lean | 29 ++++- tests/lean/run/structuralMutual.lean | 4 +- .../lean/unfoldReduceMatch.lean.expected.out | 2 +- 10 files changed, 277 insertions(+), 100 deletions(-) create mode 100644 src/Lean/Language/Util.lean diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index abbce6e771c3..e0e44300d683 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -11,6 +11,7 @@ import Lean.ResolveName import Lean.Elab.InfoTree.Types import Lean.MonadEnv import Lean.Elab.Exception +import Lean.Language.Basic namespace Lean register_builtin_option diagnostics : Bool := { @@ -72,6 +73,13 @@ structure State where messages : MessageLog := {} /-- Info tree. We have the info tree here because we want to update it while adding attributes. -/ infoState : Elab.InfoState := {} + /-- + Snapshot trees of asynchronous subtasks. As these are untyped and reported only at the end of the + command's main elaboration thread, they are only useful for basic message log reporting; for + incremental reporting and reuse within a long-running elaboration thread, types rooted in + `CommandParsedSnapshot` need to be adjusted. + -/ + snapshotTasks : Array (Language.SnapshotTask Language.SnapshotTree) := #[] deriving Nonempty /-- Context for the CoreM monad. -/ @@ -180,7 +188,8 @@ instance : Elab.MonadInfoTree CoreM where modifyInfoState f := modify fun s => { s with infoState := f s.infoState } @[inline] def modifyCache (f : Cache → Cache) : CoreM Unit := - modify fun ⟨env, next, ngen, trace, cache, messages, infoState⟩ => ⟨env, next, ngen, trace, f cache, messages, infoState⟩ + modify fun ⟨env, next, ngen, trace, cache, messages, infoState, snaps⟩ => + ⟨env, next, ngen, trace, f cache, messages, infoState, snaps⟩ @[inline] def modifyInstLevelTypeCache (f : InstantiateLevelCache → InstantiateLevelCache) : CoreM Unit := modifyCache fun ⟨c₁, c₂⟩ => ⟨f c₁, c₂⟩ @@ -355,13 +364,83 @@ instance : MonadLog CoreM where if (← read).suppressElabErrors then -- discard elaboration errors, except for a few important and unlikely misleading ones, on -- parse error - unless msg.data.hasTag (· matches `Elab.synthPlaceholder | `Tactic.unsolvedGoals) do + unless msg.data.hasTag (· matches `Elab.synthPlaceholder | `Tactic.unsolvedGoals | `trace) do return let ctx ← read let msg := { msg with data := MessageData.withNamingContext { currNamespace := ctx.currNamespace, openDecls := ctx.openDecls } msg.data }; modify fun s => { s with messages := s.messages.add msg } +/-- +Includes a given task (such as from `wrapAsyncAsSnapshot`) in the overall snapshot tree for this +command's elaboration, making its result available to reporting and the language server. The +reporter will not know about this snapshot tree node until the main elaboration thread for this +command has finished so this function is not useful for incremental reporting within a longer +elaboration thread but only for tasks that outlive it such as background kernel checking or proof +elaboration. +-/ +def logSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) : CoreM Unit := + modify fun s => { s with snapshotTasks := s.snapshotTasks.push task } + +/-- Wraps the given action for use in `EIO.asTask` etc., discarding its final monadic state. -/ +def wrapAsync (act : Unit → CoreM α) : CoreM (EIO Exception α) := do + let st ← get + let ctx ← read + let heartbeats := (← IO.getNumHeartbeats) - ctx.initHeartbeats + return withCurrHeartbeats (do + -- include heartbeats since start of elaboration in new thread as well such that forking off + -- an action doesn't suddenly allow it to succeed from a lower heartbeat count + IO.addHeartbeats heartbeats.toUInt64 + act () : CoreM _) + |>.run' ctx st + +/-- Option for capturing output to stderr during elaboration. -/ +register_builtin_option stderrAsMessages : Bool := { + defValue := true + group := "server" + descr := "(server) capture output to the Lean stderr channel (such as from `dbg_trace`) during elaboration of a command as a diagnostic message" +} + +open Language in +/-- +Wraps the given action for use in `BaseIO.asTask` etc., discarding its final state except for +`logSnapshotTask` tasks, which are reported as part of the returned tree. +-/ +def wrapAsyncAsSnapshot (act : Unit → CoreM Unit) (desc : String := by exact decl_name%.toString) : + CoreM (BaseIO SnapshotTree) := do + let t ← wrapAsync fun _ => do + IO.FS.withIsolatedStreams (isolateStderr := stderrAsMessages.get (← getOptions)) do + let tid ← IO.getTID + -- reset trace state and message log so as not to report them twice + modify ({ · with messages := {}, traceState := { tid } }) + try + withTraceNode `Elab.async (fun _ => return desc) do + act () + catch e => + logError e.toMessageData + finally + addTraceAsMessages + get + let ctx ← readThe Core.Context + return do + match (← t.toBaseIO) with + | .ok (output, st) => + let mut msgs := st.messages + if !output.isEmpty then + msgs := msgs.add { + fileName := ctx.fileName + severity := MessageSeverity.information + pos := ctx.fileMap.toPosition <| ctx.ref.getPos?.getD 0 + data := output + } + return .mk { + desc + diagnostics := (← Language.Snapshot.Diagnostics.ofMessageLog msgs) + traces := st.traceState + } st.snapshotTasks + -- interrupt or abort exception as `try catch` above should have caught any others + | .error _ => default + end Core export Core (CoreM mkFreshUserName checkSystem withCurrHeartbeats) diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index fa2f3fef00aa..4e33521c4bf9 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -84,6 +84,7 @@ structure State where ngen : NameGenerator := {} infoState : InfoState := {} traceState : TraceState := {} + snapshotTasks : Array (Language.SnapshotTask Language.SnapshotTree) := #[] deriving Nonempty structure Context where @@ -114,8 +115,7 @@ structure Context where -/ suppressElabErrors : Bool := false -abbrev CommandElabCoreM (ε) := ReaderT Context $ StateRefT State $ EIO ε -abbrev CommandElabM := CommandElabCoreM Exception +abbrev CommandElabM := ReaderT Context $ StateRefT State $ EIO Exception abbrev CommandElab := Syntax → CommandElabM Unit structure Linter where run : Syntax → CommandElabM Unit @@ -198,36 +198,6 @@ instance : AddErrorMessageContext CommandElabM where let msg ← addMacroStack msg ctx.macroStack return (ref, msg) -def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity) : Message := - let pos := ref.getPos?.getD ctx.cmdPos - let endPos := ref.getTailPos?.getD pos - mkMessageCore ctx.fileName ctx.fileMap msgData severity pos endPos - -private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog := Id.run do - if traceState.traces.isEmpty then return log - let mut traces : Std.HashMap (String.Pos × String.Pos) (Array MessageData) := ∅ - for traceElem in traceState.traces do - let ref := replaceRef traceElem.ref ctx.ref - let pos := ref.getPos?.getD 0 - let endPos := ref.getTailPos?.getD pos - traces := traces.insert (pos, endPos) <| traces.getD (pos, endPos) #[] |>.push traceElem.msg - let mut log := log - let traces' := traces.toArray.qsort fun ((a, _), _) ((b, _), _) => a < b - for ((pos, endPos), traceMsg) in traces' do - let data := .tagged `trace <| .joinSep traceMsg.toList "\n" - log := log.add <| mkMessageCore ctx.fileName ctx.fileMap data .information pos endPos - return log - -private def addTraceAsMessages : CommandElabM Unit := do - let ctx ← read - -- do not add trace messages if `trace.profiler.output` is set as it would be redundant and - -- pretty printing the trace messages is expensive - if trace.profiler.output.get? (← getOptions) |>.isNone then - modify fun s => { s with - messages := addTraceAsMessagesCore ctx s.messages s.traceState - traceState.traces := {} - } - private def runCore (x : CoreM α) : CommandElabM α := do let s ← get let ctx ← read @@ -253,6 +223,7 @@ private def runCore (x : CoreM α) : CommandElabM α := do nextMacroScope := s.nextMacroScope infoState.enabled := s.infoState.enabled traceState := s.traceState + snapshotTasks := s.snapshotTasks } let (ea, coreS) ← liftM x modify fun s => { s with @@ -261,6 +232,7 @@ private def runCore (x : CoreM α) : CommandElabM α := do ngen := coreS.ngen infoState.trees := s.infoState.trees.append coreS.infoState.trees traceState.traces := coreS.traceState.traces.map fun t => { t with ref := replaceRef t.ref ctx.ref } + snapshotTasks := coreS.snapshotTasks messages := s.messages ++ coreS.messages } return ea @@ -268,10 +240,6 @@ private def runCore (x : CoreM α) : CommandElabM α := do def liftCoreM (x : CoreM α) : CommandElabM α := do MonadExcept.ofExcept (← runCore (observing x)) -private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : Message := - let ref := getBetterRef ref ctx.macroStack - mkMessageAux ctx ref (toString err) MessageSeverity.error - @[inline] def liftIO {α} (x : IO α) : CommandElabM α := do let ctx ← read IO.toEIO (fun (ex : IO.Error) => Exception.error ctx.ref ex.toString) x @@ -294,9 +262,8 @@ instance : MonadLog CommandElabM where logMessage msg := do if (← read).suppressElabErrors then -- discard elaboration errors on parse error - -- NOTE: unlike `CoreM`'s `logMessage`, we do not currently have any command-level errors that - -- we want to allowlist - return + unless msg.data.hasTag (· matches `trace) do + return let currNamespace ← getCurrNamespace let openDecls ← getOpenDecls let msg := { msg with data := MessageData.withNamingContext { currNamespace := currNamespace, openDecls := openDecls } msg.data } @@ -322,6 +289,61 @@ def runLinters (stx : Syntax) : CommandElabM Unit := do finally modify fun s => { savedState with messages := s.messages } +/-- +Catches and logs exceptions occurring in `x`. Unlike `try catch` in `CommandElabM`, this function +catches interrupt exceptions as well and thus is intended for use at the top level of elaboration. +Interrupt and abort exceptions are caught but not logged. +-/ +@[inline] def withLoggingExceptions (x : CommandElabM Unit) : CommandElabM Unit := fun ctx ref => + EIO.catchExceptions (withLogging x ctx ref) (fun _ => pure ()) + +@[inherit_doc Core.wrapAsync] +def wrapAsync (act : Unit → CommandElabM α) : CommandElabM (EIO Exception α) := do + return act () |>.run (← read) |>.run' (← get) + +open Language in +@[inherit_doc Core.wrapAsyncAsSnapshot] +-- `CoreM` and `CommandElabM` are too different to meaningfully share this code +def wrapAsyncAsSnapshot (act : Unit → CommandElabM Unit) + (desc : String := by exact decl_name%.toString) : + CommandElabM (BaseIO SnapshotTree) := do + let t ← wrapAsync fun _ => do + IO.FS.withIsolatedStreams (isolateStderr := Core.stderrAsMessages.get (← getOptions)) do + let tid ← IO.getTID + -- reset trace state and message log so as not to report them twice + modify ({ · with messages := {}, traceState := { tid } }) + try + withTraceNode `Elab.async (fun _ => return desc) do + act () + catch e => + logError e.toMessageData + finally + addTraceAsMessages + get + let ctx ← read + return do + match (← t.toBaseIO) with + | .ok (output, st) => + let mut msgs := st.messages + if !output.isEmpty then + msgs := msgs.add { + fileName := ctx.fileName + severity := MessageSeverity.information + pos := ctx.fileMap.toPosition <| ctx.ref.getPos?.getD 0 + data := output + } + return .mk { + desc + diagnostics := (← Language.Snapshot.Diagnostics.ofMessageLog msgs) + traces := st.traceState + } st.snapshotTasks + -- interrupt or abort exception as `try catch` above should have caught any others + | .error _ => default + +@[inherit_doc Core.logSnapshotTask] +def logSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) : CommandElabM Unit := + modify fun s => { s with snapshotTasks := s.snapshotTasks.push task } + protected def getCurrMacroScope : CommandElabM Nat := do pure (← read).currMacroScope protected def getMainModule : CommandElabM Name := do pure (← getEnv).mainModule @@ -532,12 +554,6 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro let mut msgs := (← get).messages for tree in (← getInfoTrees) do trace[Elab.info] (← tree.format) - if (← isTracingEnabledFor `Elab.snapshotTree) then - if let some snap := (← read).snap? then - -- We can assume that the root command snapshot is not involved in parallelism yet, so this - -- should be true iff the command supports incrementality - if (← IO.hasFinished snap.new.result) then - liftCoreM <| Language.ToSnapshotTree.toSnapshotTree snap.new.result.get |>.trace modify fun st => { st with messages := initMsgs ++ msgs infoState := { st.infoState with trees := initInfoTrees ++ st.infoState.trees } @@ -668,14 +684,6 @@ def runTermElabM (elabFn : Array Expr → TermElabM α) : CommandElabM α := do Term.addAutoBoundImplicits' xs someType fun xs _ => Term.withoutAutoBoundImplicit <| elabFn xs -/-- -Catches and logs exceptions occurring in `x`. Unlike `try catch` in `CommandElabM`, this function -catches interrupt exceptions as well and thus is intended for use at the top level of elaboration. -Interrupt and abort exceptions are caught but not logged. --/ -@[inline] def withLoggingExceptions (x : CommandElabM Unit) : CommandElabCoreM Empty Unit := fun ctx ref => - EIO.catchExceptions (withLogging x ctx ref) (fun _ => pure ()) - private def liftAttrM {α} (x : AttrM α) : CommandElabM α := do liftCoreM x diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index d375462ba75f..0858e0357f3c 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -473,6 +473,26 @@ def withoutTacticReuse [Monad m] [MonadWithReaderOf Context m] [MonadOptions m] return !cond } }) act +@[inherit_doc Core.wrapAsync] +def wrapAsync (act : Unit → TermElabM α) : TermElabM (EIO Exception α) := do + let ctx ← read + let st ← get + let metaCtx ← readThe Meta.Context + let metaSt ← getThe Meta.State + Core.wrapAsync fun _ => + act () |>.run ctx |>.run' st |>.run' metaCtx metaSt + +@[inherit_doc Core.wrapAsyncAsSnapshot] +def wrapAsyncAsSnapshot (act : Unit → TermElabM Unit) + (desc : String := by exact decl_name%.toString) : + TermElabM (BaseIO Language.SnapshotTree) := do + let ctx ← read + let st ← get + let metaCtx ← readThe Meta.Context + let metaSt ← getThe Meta.State + Core.wrapAsyncAsSnapshot (desc := desc) fun _ => + act () |>.run ctx |>.run' st |>.run' metaCtx metaSt + abbrev TermElabResult (α : Type) := EStateM.Result Exception SavedState α /-- diff --git a/src/Lean/Language/Basic.lean b/src/Lean/Language/Basic.lean index db975b482cec..baa99e92d011 100644 --- a/src/Lean/Language/Basic.lean +++ b/src/Lean/Language/Basic.lean @@ -10,9 +10,8 @@ Authors: Sebastian Ullrich prelude import Init.System.Promise -import Lean.Message import Lean.Parser.Types -import Lean.Elab.InfoTree +import Lean.Util.Trace set_option linter.missingDocs true @@ -205,20 +204,6 @@ structure SnapshotTree where children : Array (SnapshotTask SnapshotTree) deriving Inhabited -/-- Produces trace of given snapshot tree, synchronously waiting on all children. -/ -partial def SnapshotTree.trace (s : SnapshotTree) : CoreM Unit := - go none s -where go range? s := do - let file ← getFileMap - let mut desc := f!"{s.element.desc}" - if let some range := range? then - desc := desc ++ f!"{file.toPosition range.start}-{file.toPosition range.stop} " - desc := desc ++ .prefixJoin "\n• " (← s.element.diagnostics.msgLog.toList.mapM (·.toString)) - if let some t := s.element.infoTree? then - trace[Elab.info] (← t.format) - withTraceNode `Elab.snapshotTree (fun _ => pure desc) do - s.children.toList.forM fun c => go c.range? c.get - /-- Helper class for projecting a heterogeneous hierarchy of snapshot classes to a homogeneous representation. -/ @@ -303,6 +288,14 @@ def SnapshotTree.runAndReport (s : SnapshotTree) (opts : Options) (json := false def SnapshotTree.getAll (s : SnapshotTree) : Array Snapshot := s.forM (m := StateM _) (fun s => modify (·.push s)) |>.run #[] |>.2 +/-- Returns a task that waits on all snapshots in the tree. -/ +def SnapshotTree.waitAll : SnapshotTree → BaseIO (Task Unit) + | mk _ children => go children.toList +where + go : List (SnapshotTask SnapshotTree) → BaseIO (Task Unit) + | [] => return .pure () + | t::ts => BaseIO.bindTask t.task fun _ => go ts + /-- Context of an input processing invocation. -/ structure ProcessingContext extends Parser.InputContext diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean index a411ffafe501..79a13ffb0244 100644 --- a/src/Lean/Language/Lean.lean +++ b/src/Lean/Language/Lean.lean @@ -10,6 +10,7 @@ Authors: Sebastian Ullrich prelude import Lean.Language.Basic +import Lean.Language.Util import Lean.Language.Lean.Types import Lean.Parser.Module import Lean.Elab.Import @@ -166,13 +167,6 @@ namespace Lean.Language.Lean open Lean.Elab Command open Lean.Parser -/-- Option for capturing output to stderr during elaboration. -/ -register_builtin_option stderrAsMessages : Bool := { - defValue := true - group := "server" - descr := "(server) capture output to the Lean stderr channel (such as from `dbg_trace`) during elaboration of a command as a diagnostic message" -} - /-- Lean-specific processing context. -/ structure LeanProcessingContext extends ProcessingContext where /-- Position of the first file difference if there was a previous invocation. -/ @@ -519,6 +513,7 @@ where diagnostics := .empty, stx := .missing, parserState elabSnap := .pure <| .ofTyped { diagnostics := .empty : SnapshotLeaf } finishedSnap := .pure { diagnostics := .empty, cmdState } + reportSnap := default tacticCache := (← IO.mkRef {}) nextCmdSnap? := none } @@ -529,6 +524,7 @@ where -- definitely resolved in `doElab` task let elabPromise ← IO.Promise.new let finishedPromise ← IO.Promise.new + let reportPromise ← IO.Promise.new -- (Try to) use last line of command as range for final snapshot task. This ensures we do not -- retract the progress bar to a previous position in case the command support incremental -- reporting but has significant work after resolving its last incremental promise, such as @@ -547,22 +543,46 @@ where let nextCmdSnap? := next?.map ({ range? := some ⟨parserState.pos, ctx.input.endPos⟩, task := ·.result }) let diagnostics ← Snapshot.Diagnostics.ofMessageLog msgLog - if minimalSnapshots && !Parser.isTerminalCommand stx then - prom.resolve { - diagnostics, finishedSnap, tacticCache, nextCmdSnap? - stx := .missing - parserState := {} - elabSnap := { range? := stx.getRange?, task := elabPromise.result } - } + let (stx', parserState') := if minimalSnapshots && !Parser.isTerminalCommand stx then + (default, default) else - prom.resolve { - diagnostics, stx, parserState, tacticCache, nextCmdSnap? - elabSnap := { range? := stx.getRange?, task := elabPromise.result } - finishedSnap - } + (stx, parserState) + prom.resolve { + diagnostics, finishedSnap, tacticCache, nextCmdSnap? + stx := stx', parserState := parserState' + elabSnap := { range? := stx.getRange?, task := elabPromise.result } + reportSnap := { range? := endRange?, task := reportPromise.result } + } let cmdState ← doElab stx cmdState beginPos { old? := old?.map fun old => ⟨old.stx, old.elabSnap⟩, new := elabPromise } finishedPromise tacticCache ctx + let traceTask ← + if (← isTracingEnabledForCore `Elab.snapshotTree cmdState.scopes.head!.opts) then + -- We want to trace all of `CommandParsedSnapshot` but `traceTask` is part of it, so let's + -- create a temporary snapshot tree containing all tasks but it + let snaps := #[ + { range? := none, task := elabPromise.result.map (sync := true) toSnapshotTree }, + { range? := none, task := finishedPromise.result.map (sync := true) toSnapshotTree }] ++ + cmdState.snapshotTasks + let tree := SnapshotTree.mk { diagnostics := .empty } snaps + BaseIO.bindTask (← tree.waitAll) fun _ => do + let .ok (_, s) ← EIO.toBaseIO <| tree.trace |>.run + { ctx with options := cmdState.scopes.head!.opts } { env := cmdState.env } + | pure <| .pure <| .mk { diagnostics := .empty } #[] + let mut msgLog := MessageLog.empty + for trace in s.traceState.traces do + msgLog := msgLog.add { + fileName := ctx.fileName + severity := MessageSeverity.information + pos := ctx.fileMap.toPosition beginPos + data := trace.msg + } + return .pure <| .mk { diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog) } #[] + else + pure <| .pure <| .mk { diagnostics := .empty } #[] + reportPromise.resolve <| + .mk { diagnostics := .empty } <| + cmdState.snapshotTasks.push { range? := endRange?, task := traceTask } if let some next := next? then -- We're definitely off the fast-forwarding path now parseCmd none parserState cmdState next (sync := false) ctx @@ -573,7 +593,9 @@ where LeanProcessingM Command.State := do let ctx ← read let scope := cmdState.scopes.head! - let cmdStateRef ← IO.mkRef { cmdState with messages := .empty, traceState := {} } + -- reset per-command state + let cmdStateRef ← IO.mkRef { cmdState with + messages := .empty, traceState := {}, snapshotTasks := #[] } /- The same snapshot may be executed by different tasks. So, to make sure `elabCommandTopLevel` has exclusive access to the cache, we create a fresh reference here. Before this change, the @@ -588,8 +610,8 @@ where cancelTk? := some ctx.newCancelTk } let (output, _) ← - IO.FS.withIsolatedStreams (isolateStderr := stderrAsMessages.get scope.opts) do - liftM (m := BaseIO) do + IO.FS.withIsolatedStreams (isolateStderr := Core.stderrAsMessages.get scope.opts) do + EIO.toBaseIO do withLoggingExceptions (getResetInfoTrees *> Elab.Command.elabCommandTopLevel stx) cmdCtx cmdStateRef diff --git a/src/Lean/Language/Lean/Types.lean b/src/Lean/Language/Lean/Types.lean index 1f40dafc12c0..0ac51a0f4cec 100644 --- a/src/Lean/Language/Lean/Types.lean +++ b/src/Lean/Language/Lean/Types.lean @@ -46,6 +46,8 @@ structure CommandParsedSnapshot extends Snapshot where elabSnap : SnapshotTask DynamicSnapshot /-- State after processing is finished. -/ finishedSnap : SnapshotTask CommandFinishedSnapshot + /-- Additional, untyped snapshots used for reporting, not reuse. -/ + reportSnap : SnapshotTask SnapshotTree /-- Cache for `save`; to be replaced with incrementality. -/ tacticCache : IO.Ref Tactic.Cache /-- Next command, unless this is a terminal command. -/ @@ -55,7 +57,8 @@ partial instance : ToSnapshotTree CommandParsedSnapshot where toSnapshotTree := go where go s := ⟨s.toSnapshot, #[s.elabSnap.map (sync := true) toSnapshotTree, - s.finishedSnap.map (sync := true) toSnapshotTree] |> + s.finishedSnap.map (sync := true) toSnapshotTree, + s.reportSnap] |> pushOpt (s.nextCmdSnap?.map (·.map (sync := true) go))⟩ /-- State after successful importing. -/ diff --git a/src/Lean/Language/Util.lean b/src/Lean/Language/Util.lean new file mode 100644 index 000000000000..139450445cbe --- /dev/null +++ b/src/Lean/Language/Util.lean @@ -0,0 +1,29 @@ +/- +Copyright (c) 2023 Lean FRO. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Additional snapshot functionality that needs further imports. + +Authors: Sebastian Ullrich +-/ + +prelude +import Lean.Language.Basic +import Lean.CoreM +import Lean.Elab.InfoTree + +namespace Lean.Language + +/-- Produces trace of given snapshot tree, synchronously waiting on all children. -/ +partial def SnapshotTree.trace (s : SnapshotTree) : CoreM Unit := + go none s +where go range? s := do + let file ← getFileMap + let mut desc := f!"{s.element.desc}" + if let some range := range? then + desc := desc ++ f!"{file.toPosition range.start}-{file.toPosition range.stop} " + desc := desc ++ .prefixJoin "\n• " (← s.element.diagnostics.msgLog.toList.mapM (·.toString)) + if let some t := s.element.infoTree? then + trace[Elab.info] (← t.format) + withTraceNode `Elab.snapshotTree (fun _ => pure desc) do + s.children.toList.forM fun c => go c.range? c.get diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index 35162376f421..5b9be976b1de 100644 --- a/src/Lean/Util/Trace.lean +++ b/src/Lean/Util/Trace.lean @@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich, Leonardo de Moura -/ prelude -import Lean.Exception +import Lean.Elab.Exception +import Lean.Log /-! # Trace messages @@ -101,9 +102,12 @@ where else false +def isTracingEnabledForCore (cls : Name) (opts : Options) : BaseIO Bool := do + let inherited ← inheritedTraceOptions.get + return checkTraceOption inherited opts cls + def isTracingEnabledFor (cls : Name) : m Bool := do - let inherited ← (inheritedTraceOptions.get : IO _) - pure (checkTraceOption inherited (← getOptions) cls) + (isTracingEnabledForCore cls (← getOptions) : IO _) @[inline] def getTraces : m (PersistentArray TraceElem) := do let s ← getTraceState @@ -357,4 +361,23 @@ def withTraceNodeBefore [MonadRef m] [AddMessageContext m] [MonadOptions m] addTraceNode oldTraces data ref msg MonadExcept.ofExcept res +def addTraceAsMessages [Monad m] [MonadRef m] [MonadLog m] [MonadTrace m] : m Unit := do + if trace.profiler.output.get? (← getOptions) |>.isSome then + -- do not add trace messages if `trace.profiler.output` is set as it would be redundant and + -- pretty printing the trace messages is expensive + return + let traces ← getResetTraces + if traces.isEmpty then + return + let mut pos2traces : Std.HashMap (String.Pos × String.Pos) (Array MessageData) := ∅ + for traceElem in traces do + let ref := replaceRef traceElem.ref (← getRef) + let pos := ref.getPos?.getD 0 + let endPos := ref.getTailPos?.getD pos + pos2traces := pos2traces.insert (pos, endPos) <| pos2traces.getD (pos, endPos) #[] |>.push traceElem.msg + let traces' := pos2traces.toArray.qsort fun ((a, _), _) ((b, _), _) => a < b + for ((pos, endPos), traceMsg) in traces' do + let data := .tagged `trace <| .joinSep traceMsg.toList "\n" + logMessage <| Elab.mkMessageCore (← getFileName) (← getFileMap) data .information pos endPos + end Lean diff --git a/tests/lean/run/structuralMutual.lean b/tests/lean/run/structuralMutual.lean index cf243b665f26..b8ad61f2509d 100644 --- a/tests/lean/run/structuralMutual.lean +++ b/tests/lean/run/structuralMutual.lean @@ -250,8 +250,8 @@ theorem eq_false_of_not_eq_true {b : Bool} : (! b) = true → b = false := by si /-- info: n : Nat -h : EvenOdd.isOdd (n + 1) = false -⊢ EvenOdd.isEven n = true +h : isOdd (n + 1) = false +⊢ isEven n = true -/ #guard_msgs in theorem ex1 (n : Nat) (h : isEven (n+2) = true) : isEven n = true := by diff --git a/tests/lean/unfoldReduceMatch.lean.expected.out b/tests/lean/unfoldReduceMatch.lean.expected.out index 72c499c4bbb5..4460afe799d1 100644 --- a/tests/lean/unfoldReduceMatch.lean.expected.out +++ b/tests/lean/unfoldReduceMatch.lean.expected.out @@ -1,3 +1,3 @@ unfoldReduceMatch.lean:2:0-2:7: warning: declaration uses 'sorry' n : Nat -⊢ (Nat.zero.add n).succ = n.succ +⊢ (zero.add n).succ = n.succ