Stream: Coq devs & plugin devs

Topic: Profiling on Coq Plugin


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Feb 27 2023 at 17:01):

Basically, yes.

view this post on Zulip 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.

view this post on Zulip 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 13 2024 at 07:01 UTC