different dbg_traces

Stream: lean4

[Damiano Testa]

Dear All,

I am slowly learning my way around Lean 4 and was wondering about the different options that dbg_trace has. I could not tell the difference between them. Below is an example where they give the same output. What are the difference between them?

Thanks!

import Lean.Elab.Tactic

elab "traces" : tactic => do
  let tgt ← Lean.Elab.Tactic.getMainTarget
  dbg_trace f!"with f:\n{tgt}"
  dbg_trace s!"with s:\n{tgt}"
  dbg_trace "neither f nor s:\n{tgt}"

theorem trace {a : Nat} : a = 0 := by
  traces
/-  The three traces produce the same outputs:
with f:
Eq.{1} Nat _uniq.588 (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))
with s:
Eq.{1} Nat _uniq.588 (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))
neither f nor s:
Eq.{1} Nat _uniq.588 (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))
-/

[Mario Carneiro]

Those aren't options of dbg_trace

[Damiano Testa]

Ok, but with those, dbg_trace does not complain, with any other single character it does.

[Mario Carneiro]

dbg_trace takes a format string, or an expression that implements ToString

[Mario Carneiro]

f!"fmt_string" is the latter

[Mario Carneiro]

My guess is that the latter two are equivalent

[Damiano Testa]

Ah, are you saying that the f! or s! are attached to the stuff in quotations and have nothing to do with dbg_trace? So, dbg_trace simply prints out the outcome of f!"..." or s!"..."?

[Mario Carneiro]

yes

[Damiano Testa]

Ok, so is there a difference between s!"..." and f!"..."?

[Mario Carneiro]

the same is also true for m!, but MessageData doesn't implement ToString so it doesn't work

[Damiano Testa]

or is this what you answered when you said "My guess is that the latter two are equivalent"?

[Mario Carneiro]

f! uses ToFormat instead of ToString and produces a Format

[Mario Carneiro]

I think dbg_trace s!"str" and dbg_trace "str" are exactly equivalent in terms of the functions that get called

[Mario Carneiro]

dbg_trace f!"str" is a bit different since it is being formatted using the ToFormat implementation and then the format is converted to a string

[Damiano Testa]

Ok, so in my situation above, ToFormat and ToString produce the same output and dbg_trace traces the same thing on either one of them and also on the plain "...", right?

[Mario Carneiro]

But most likely it won't be noticeably different in most cases

[Mario Carneiro]

right

[Mario Carneiro]

It's possible that the f! version might result in better looking output when the data is large enough to appear on multiple lines ...?

[Mario Carneiro]

assuming the type's ToString implementation isn't just defined as x.toFormat.toString

[Damiano Testa]

I'll write a longet goal and see if it prints differently.

[Mario Carneiro]

I would guess that Expr has a pretty solid formatter implementation so you aren't likely to see a difference there

[Mario Carneiro]

I'm thinking something like ToString on a List (String x String) or so

[Mario Carneiro]

indeed, take a look:

elab "traces" : tactic => do
  let tgt := (List.range 20).map (fun i => (i, i))
  dbg_trace f!"with f:\n{tgt}"
  dbg_trace s!"with s:\n{tgt}"
  dbg_trace "neither f nor s:\n{tgt}"

theorem trace {a : Nat} : a = 0 := by
  traces
-- with f:
-- [(0, 0),
--  (1, 1),
--  (2, 2),
--  (3, 3),
--  (4, 4),
--  (5, 5),
--  (6, 6),
--  (7, 7),
--  (8, 8),
--  (9, 9),
--  (10, 10),
--  (11, 11),
--  (12, 12),
--  (13, 13),
--  (14, 14),
--  (15, 15),
--  (16, 16),
--  (17, 17),
--  (18, 18),
--  (19, 19)]
-- with s:
-- [(0, 0), (1, 1), (2, 2), (3, 3), (4, 4), (5, 5), (6, 6), (7, 7), (8, 8), (9, 9), (10, 10), (11, 11), (12, 12), (13, 13), (14, 14), (15, 15), (16, 16), (17, 17), (18, 18), (19, 19)]
-- neither f nor s:
-- [(0, 0), (1, 1), (2, 2), (3, 3), (4, 4), (5, 5), (6, 6), (7, 7), (8, 8), (9, 9), (10, 10), (11, 11), (12, 12), (13, 13), (14, 14), (15, 15), (16, 16), (17, 17), (18, 18), (19, 19)]

[Damiano Testa]

Ah, thanks! I was fiddling with strings and did not get anywhere!

[Mario Carneiro]

The reason for this is that the ToString (List A) instance doesn't really have enough information to do line wrapping correctly

[Mario Carneiro]

but if it's ToFormat then it can delay the wrapping decisions to the ToString Format instance

[Damiano Testa]

Mario, do you mind if a variation of this goes into the metaprogramming in lean 4 book?

[Mario Carneiro]

of course not, please go ahead

[Damiano Testa]

Turns out, 15 iterations are sufficient for wrapping!

[Mario Carneiro]

you could also do something like List.replicate 5 (List.range 8) which probably looks a bit more tidy

[Damiano Testa]

That's great, thanks!

[Damiano Testa]

One final detail, then. Is it possible to observe a difference between s! and neither f nor s?

[Mario Carneiro]

No, because it macro expands to the same thing

[Damiano Testa]

Perfect, thanks!

[Damiano Testa]

So, just to make sure that I understand.

• f!"..." produces a Format out of ... which then dbg_trace prints, thanks for a Format.toString instance.
• s!"..." produces a String out of ... which then dbg_trace prints.
• "..." produces a String out of ... which then dbg_trace prints passing it via s! first, since this is how dbg_trace is implemented.

Is this correct?

[Damiano Testa]

That is, at a minimum, the string passed to dbg_trace gets an s! applied, unless you specify that you want something else?

[Damiano Testa]

#26 :smile:

[Mario Carneiro]

The only function of s! is to transform s!"bla {x} bla" to ("bla " ++ toString x ++ " bla")

[Mario Carneiro]

f! does the same thing but with toFormat instead of toString and the append instance on Format

[Mario Carneiro]

That is, these macros are all just to make it easier to use interpolated strings where possible, since otherwise dbg_trace "foo {x}" would actually print "foo {x}" which isn't what we want

[Damiano Testa]

Ok, thanks for the explanation!

I feel very unsure about these things and cannot always understand the source code, so I value and appreciate very much these confirmations and corrections! :smile: