From c24d2186fc180615f3eed70235d4c774a4c62caa Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 8 Aug 2024 12:28:22 +0200 Subject: [PATCH] doc: `stderrAsMessages` is now the default on the cmdline as well (#4955) --- doc/dev/debugging.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/doc/dev/debugging.md b/doc/dev/debugging.md index 87836249d83b..a742f9b6431b 100644 --- a/doc/dev/debugging.md +++ b/doc/dev/debugging.md @@ -5,7 +5,7 @@ Some notes on how to debug Lean, which may also be applicable to debugging Lean ## Tracing -In `CoreM` and derived monads, we use `trace![traceCls] "msg with {interpolations}"` to fill the structured trace viewable with `set_option trace.traceCls true`. +In `CoreM` and derived monads, we use `trace[traceCls] "msg with {interpolations}"` to fill the structured trace viewable with `set_option trace.traceCls true`. New trace classes have to be registered using `registerTraceClass` first. Notable trace classes: @@ -22,7 +22,9 @@ Notable trace classes: In pure contexts or when execution is aborted before the messages are finally printed, one can instead use the term `dbg_trace "msg with {interpolations}"; val` (`;` can also be replaced by a newline), which will print the message to stderr before evaluating `val`. `dbgTraceVal val` can be used as a shorthand for `dbg_trace "{val}"; val`. Note that if the return value is not actually used, the trace code is silently dropped as well. -In the language server, stderr output is buffered and shown as messages after a command has been elaborated, unless the option `server.stderrAsMessages` is deactivated. + +By default, such stderr output is buffered and shown as messages after a command has been elaborated, which is necessary to ensure deterministic ordering of messages under parallelism. +If Lean aborts the process before it can finish the command or takes too long to do that, using `-DstderrAsMessages=false` avoids this buffering and shows `dbg_trace` output (but not `trace`s or other diagnostics) immediately. ## Debuggers