-
Notifications
You must be signed in to change notification settings - Fork 232
Profiling F* (Linux OCaml)
Tom Kelly edited this page Jul 12, 2019
·
2 revisions
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.