Profiling F* (Linux OCaml) - FStarLang/FStar GitHub Wiki

Profiling F* (Linux/OCaml)

There are multiple tools you can use to profile FStar (on Linux with OCaml extraction), in order of ease of use:

• Profiling F* with Linux perf: statistical profiler that requires no instrumentation and is quick to run. Results can be more involved to interpret.
• Profiling F* with OCaml Landmarks: Needs an OCaml rebuild, but the automatic mode can allow you to quickly hone in on where the time is spent.
• Profiling F* with Spacetime: Needs a custom switch and rebuild, but can show you where memory is allocated. Can be slow to run.
• Profiling F* with the OCaml statistical memory profiler: Needs a custom OCaml switch and rebuild, gives a fast execution with statistical sample of where memory allocation is occurring.