(trace)

Stream: lean4

[Marcus Rossel]

When I use a custom trace class, all I see is (trace):

-- Test.Basic.lean
import Lean

initialize Lean.registerTraceClass `foo

elab "foo" : tactic => do
  trace[foo] "message"

-- Main.lean
import Test.Basic

set_option trace.foo true

example : True := by
  foo -- shows "(trace)"

Other examples I've found seem to do nothing different than what I am doing here. What's wrong with my example?

[Tomas Skrivan]

What happens if you put the initialize in a separate file?

[Marcus Rossel]

Tomas Skrivan said:

What happens if you put the initialize in a separate file?

Same result.

[Marcus Rossel]

Interestingly, if I lake build it shows:

[0/4] Building Test.Basic
[1/4] Compiling Test.Basic
[1/4] Building Main
stdout:
[foo] message
[2/4] Compiling Main
[4/4] Linking test

[Mario Carneiro]

this is expected (?). The info hover shows (trace) but the actual trace message is visible in the infoview as another widget-like thing

[Mario Carneiro]

this happens for all trace messages

[Wojciech Nawrocki]

This happens because many traces are huge in practice and you don't want to print them out. That said, the system could print a prefix up to some fixed limit.

[Mario Carneiro]

why does it even show (trace)? I don't see the point of an info hover that just says (trace) (trace) (trace)

[Wojciech Nawrocki]

The output is the same as what you see in the terminal. Should it just not report a message at all?

[Mario Carneiro]

I don't really understand the mechanism by which the stdout is different from the info hover

[Mario Carneiro]

I only ever see (trace) in hovers

[Wojciech Nawrocki]

You're right, it is different on the CLI. I spoke too early. The hover is the standard LSP message reported by the server, whereas the interactive trace is an interactive version of the same message. Perhaps they should be more aligned.

[Thomas Murrills]

I’d love a truncated-after-too-many-characters trace message (ending in …) in hover instead of (trace). Lots of times, especially when debugging fresh code, traces can be small! :)