Using the Firefox profiler dashboard for trace.profiler

Stream: lean4

[Yann Herklotz]

Being able to use the firefox profiler dashboard to look at trace.profiler output seems really useful, however, I'm having trouble getting the profiler to output the report.

import Lean

set_option trace.profiler.output "/tmp/out.json"
set_option trace.profiler.output.pp true
set_option trace.profiler true

example : True := by
  sleep 2000
  constructor

I can't seem to find a file at /tmp/out.json if I run this in vscode or Emacs.

If I run lean manually on the command-line, I can get an output, but then I can't use lake and can't import additional modules, but maybe I can figure out how to do that.

lean -Dtrace.profiler=true -Dtrace.profiler.output=profile.json main.lean

[Sebastian Ullrich]

You can prefix the command with lake env for that

[Yann Herklotz]

Ah thank you that works perfectly!