Timing your changes - FStarLang/FStar GitHub Wiki

If you make changes to the system you can test its performance with rlim and a script in FStar/.scripts/res_summary.py.

Install an rlim which has the -p switch to propagate return codes from https://github.com/arminbiere/runlim.

export your FSTAR_HOME and export RESOURCEMONITOR=1.

When you run make in FStar it will collect *.runlim files in ulib/.cache and when you run examples make it will collect them in examples/_cache.

FStar/.scripts/res_summary.py will find the .runlim files and write out a summary.

Run this single threaded for best timings.