How to view stderr buffer in neovim

Stream: new members

[Jakub Nowak]

It says in the README of https://github.com/Julian/lean.nvim, that "The default implementation will redirect to a dedicated stderr window", but I don't see any new window even though I've used dbgTrace. It works in vscode, I get a "Lean server printed an error:" notification.
@Julian Berman

[Julian Berman]

Can you give me a full example I can try?

[Jakub Nowak]

With this code the message "here be dragons" is not found in infoview. Lean prints it on stderr. VS Code prints this in a notification.

import Lean

open Lean PrettyPrinter.Delaborator

opaque x : Prop

@[delab app.x]
def my_delab : Delab := do
  dbgTrace "here be dragons" fun () => `(42)

example : x := by
  -- put cursor here

image.png

[Julian Berman]

Thanks, I don't really understand what causes Lean to decide whether to send that dbgTrace to stderr, I was trying #eval dbgTrace "foo" fun _ ↦ 37 which goes to normal LSP diagnostics which is why I asked you for the example.
Anyways, fixed now in f567bd8 if you update. I'll try and turn that into a test at some point later, it's been on the list of known test gaps.

[Jakub Nowak]

Yeah, I've also tried with #eval when you asked for mwe, and noticed it's different. I was working on delaboration in mathlib. I don't know why it works that way, but in delaboration function also neither trace nor logInfo works.
Thanks for the fix!

[Julian Berman]

(I am being lazy and not checking but maybe it depends on what monad we're inside or something, or maybe Lean is not happy if a delaborator fails...)