how to use trace.profiler.output

Stream: lean4

[Kevin Buzzard]

Sorry to be so clueless. I've seen several people talking about how they're profiling stuff using set_option trace.profiler.output but I don't know how to get anything to work.

Step 1: I put set_option trace.profiler.output "/tmp/out.json" into a file in mathlib, just above the declaration I want to profile.

Step 2: I recompile in VS Code and I don't get a file called /tmp/out.json.

Step 3: I type random stuff on the command line which I don't understand at all like lake env lake build Mathlib.FieldTheory.Galois.Basic and I still don't get one.

Step 4: even when I do get one, I won't know what to do with it other than the fact that I'm supposed to "use the Firefox profiler".

Sorry, I'm a long way from being a computer scientist and would really appreciate some basic instructions. I've looked at a PR to core where this stuff was being tinkered with but that didn't help me either. I also watched Sebastian's youtube video from Bonn but it just assumed that I knew the basics, which is what I'm struggling with. I'm confident I'll understand the output once it's up and running because I've looked at many mathlib traces in the past but always through piping lake output to a file and opening with a text editor (or just reading in the infoview) and I'd like to upgrade to 2024.

[Ruben Van de Velde]

Probably the idea is that you upload the trace (once you get it) to https://profiler.firefox.com/ ?

[Kevin Buzzard]

lake env lean Mathlib/FieldTheory/Galois/Basic.lean paused for a long time...but still no json file :-)

[Kevin Buzzard]

Aah, this works:

lake env lean -Dtrace.profiler=true -Dtrace.profiler.output=/tmp/profile.json Mathlib/FieldTheory/Galois/Basic.lean

(and but then I'm not sure what the point is of putting the set_option in the Lean file, and probably I also didn't use all the myriad mathlib options which would usually be fed to Lean?

[Kevin Buzzard]

Also, I only want to profile one declaration -- I think I might have just profiled an entire huge file?

[Sebastian Ullrich]

That's not something that is well-exposed currently - but you should be able to move the first option to where you want it in the file and only leave the second option on the cmdline

[Eric Wieser]

Is there any way to set the output without invoking the command line directly?

[Eric Wieser]

It's a little annoying to have to find all the --load_dynlib arguments that lake would pass automatically

[Eric Wieser]

(We tried to do this in Providence last week by changing the Lean server args, but ended up just having to reassemble the full command line)

[Mac Malone]

@Eric Wieser You can use lake lean to have Lake provide the poper arguments (and build any imports). For instance, adapting Kevin's example:

lake lean Mathlib/FieldTheory/Galois/Basic.lean -- -Dtrace.profiler=true -Dtrace.profiler.output=/tmp/profile.json

[Eric Wieser]

Perhaps Lean core should provide a linter warning that set_option trace.profiler.output "foo" doesn't actually do anything, and you have to use the command line?