measure instruction counts locally

Stream: general

[Christian Merten]

I use lake env lean -Dtrace.profiler=true -Dtrace.profiler.output=profile.json <filename.lean> to measure build time. Can I also get from this the number of instructions as in the output by the speed center?

[Henrik Böving]

Those are measured using perf

[Christian Merten]

How do I run this? lake env perf <filename>.lean gives could not execute external process 'perf'

[Christian Merten]

Aha, perf refers to a general tool, right?

[Henrik Böving]

Yes perf is a general Linux utility for performance profiling

[Christian Merten]

Thanks!