I am curious -- has anyone done profiling on Coq plugin implemented by OCaml? I couldn't find any material online.
I do that on a regular basis. For low-level profiling I rely on the linux perf tool. You need to use the +fp switch of OCaml, but apart from that it's fairly robust.
Pierre-Marie Pédrot said:
I do that on a regular basis. For low-level profiling I rely on the linux perf tool. You need to use the +fp switch of OCaml, but apart from that it's fairly robust.
When you say "low-level profiling in Linux perf", do you mean after the profiling, when check the perf record file, there will be a "map" corresponding to the source code (of the plugin) and illustrate the "hotness"?
So I just compile plugin with +fp switch of OCaml, and run perf with coqc on a .v
file that uses my plugin, and that will be fine?
Basically, yes.
You have to use a program to exploit the output, but the built-in perf report command does that.
My goto process is to perf record -g COMMAND
and then perf report -g fractal,callee
or such.
Last updated: Sep 25 2023 at 12:01 UTC