Profiling F* with the OCaml statistical memory profiler

Profiling F* with the OCaml statistical memory profiler

There is experimental statistical memory profiler support based on: https://github.com/jhjourdan/ocaml/tree/memprof

To install the compiler support along with an opam universe using it:

 $ opam switch export opam_existing_universe
 $ opam  create 4.07.1+statistical-memprof
 $ opam switch import opam_existing_universe

To use this memory profiler with FStar, you need to patch FStar:

• you need to add an option to turn on the memory profiling, set its sampling rate and where to output data
• you need to add a stub to output the samples to file

An example of doing this is here: https://github.com/ctk21/FStar/tree/feature/ctk21/statmemprof_example

With this patch you can run FStar as follows:

 $ fstar.exe --memory_profile memory_profile.out,0.1,20,100 <other-arguments-to-fstar>

it will produce a statistical memory profile to memory_profile.out