FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

Use nanosecond timing from monotonic clock mtime for profiling #3587

Closed nikswamy closed 1 month ago

nikswamy commented 1 month ago

This PR uses the mtime package for measuring time, providing more accurate profiling. Previously, we were accumulating only millisecond timings in the profiling counters, which led to incorrect accounting.

Thanks to @LukeXuan for reporting the issue.

Note: This PR adds mtime to the list of opam dependences

nikswamy commented 1 month ago

check world succeeds too