Skip to content

Timing your changes

Brian Milnes edited this page Oct 14, 2024 · 1 revision

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.

Clone this wiki locally