Metavariables in profiler

Stream: general

[Heather Macbeth]

Is there a way of seeing the unassigned metavariables at each step in trace.profiler? I would like to see when each metavariable first appears and also when it is assigned.

[Kyle Miller]

Maybe you would have luck with set_option pp.instantiateMVars false?

[Heather Macbeth]

Thanks for the suggestion -- I have now set this option but I can't actually see any change, what does it do?

[Kyle Miller]

I think I misunderstood what you were asking. This makes mvars pretty print as mvars without substitution of their values, which could help if there were expressions that you knew had mvars only assigned later.

[Heather Macbeth]

I think I might be able to track the metavariables by hand if I could navigate the profiler output more easily. Is there a way of getting the profiler output as (say) a JSON?

[Heather Macbeth]

For example, I noticed in this message that debugging involved generating the following tree:
https://profiler.firefox.com/public/dp8e227v3hcwan5655zcjy9eqymawghrwkq90y8/calltree/?globalTrackOrder=0&thread=0&timelineType=category&v=10
How do I make one of these for myself?

[Heather Macbeth]

Ah: Now I discovered set_option trace.profiler.output "/tmp/out.json" from this thread. But this doesn't seem to export the full profiling information. For example, a step like

[Meta.isDefEq] [0.002270] ✅️ (E →L[ℂ] F) ≃ₗᵢ⋆[ℂ] F →L[ℂ] E =?= (?m.5180 →SL[?m.5189] F) ≃ₛₗᵢ[?m.5508] ?m.5503

will be summarized to Meta.isDefEq. Is there a way of getting the full information in the output?

[Heather Macbeth]

More stream-of-consciousness: I discovered set_option trace.profiler.output.pp true, which provides all the output information I wanted, but now I would love to have this less verbose. Is it possible to modify the pretty-printing settings for the profiler output? (For example, is there a way to set pp.universes false in the profiler output?)

[Sebastian Ullrich]

I believe it should work if you set all these options on the command line, that's how the export is intended to be used

[Heather Macbeth]

@Sebastian Ullrich Is this the right syntax? I tried this and it didn't eliminate pretty-printing of universes.

lake env lean -Dtrace.profiler=true -Dtrace.profiler.output="profile.json" -Dtrace.profiler.output.pp=true -Dtrace.profiler.threshold=1 -Dpp.universes=false MyFile.lean

[Kevin Buzzard]

I didn't know about set_option trace.profiler.output "/tmp/out.json" but when I've wanted to dump traces to a file I've just added the appropriate set_options to the file and then lake build <path.to.file> > traceoutput.txt on the command line. Apologies if you're well aware of this option!

[Heather Macbeth]

@Kevin Buzzard That's pretty clever and I didn't think of doing that! But it doesn't give JSON output, right? Just an implicit tree structure based on tabs.

[Kevin Buzzard]

Yes unfortunately it's just a text file. I don't know what JSON is, I just read it manually usually.

[Sebastian Ullrich]

@Heather Macbeth I think what is happening is that output.pp does not use the pretty printer at all but always prints the bare structure of the term, could you confirm there's no notations etc. at all? If so, could you open an issue?

[Sebastian Ullrich]

@Kevin Buzzard You're missing out! https://youtu.be/T0M5WpnuneE?si=6sABAh1pmWVqP4B0&t=1400

[Heather Macbeth]

Sebastian Ullrich said:

Heather Macbeth I think what is happening is that output.pp does not use the pretty printer at all but always prints the bare structure of the term, could you confirm there's no notations etc. at all? If so, could you open an issue?

@Sebastian Ullrich Here is a typical line of the profile.json output on the following test input:

notation "ℤ" => Int
theorem foo {a : ℤ} (h : 0 ≤ a) : 0 < a + 1 := Int.add_pos_of_nonneg_of_pos h Int.zero_lt_one

"Elab.step: Lean.Parser.Term.app: expected type: LT.lt.{0} Int Int.instLTInt (OfNat.ofNat.{0} Int 0 (instOfNat 0)) (HAdd.hAdd.{0, 0, 0} Int Int Int (instHAdd.{0} Int Int.instAdd) _uniq.1362 (OfNat.ofNat.{0} Int 1 (instOfNat 1))), term\n(Term.app `Int.add_pos_of_nonneg_of_pos [`h `Int.zero_lt_one])"

(So it is certainly not using the default pp options.). This is unchanged if I explicitly set certain pp options (which I think are default):

lake env lean -Dtrace.profiler=true -Dtrace.profiler.output="profile.json" -Dtrace.profiler.output.pp=true -Dtrace.profiler.threshold=0  -Dpp.notation=true -Dpp.universes=false FileName.lean

Does this confirm what you suspected? If so I'll open the issue.

[Sebastian Ullrich]

It does, thanks!

[Heather Macbeth]

OK, filed at lean4#5872.