Ende Jin (Feb 27 2023 at 16:45): Ende Jin (Feb 27 2023 at 16:45):I am curious -- has anyone done profiling on Coq plugin implemented by OCaml? I couldn't find any material online.
Pierre-Marie Pédrot (Feb 27 2023 at 16:46):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.
Ende Jin (Feb 27 2023 at 17:00):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?
Pierre-Marie Pédrot (Feb 27 2023 at 17:01):Basically, yes.
Pierre-Marie Pédrot (Feb 27 2023 at 17:02):You have to use a program to exploit the output, but the built-in perf report command does that.
Pierre-Marie Pédrot (Feb 27 2023 at 17:03):My goto process is to perf record -g COMMAND and then perf report -g fractal,callee or such.
Last updated: Jun 09 2023 at 08:01 UTC