Zulip Chat Archive

Stream: lean4

Topic: Benchmarking Tactics

Tomaz Gomes Mascarenhas (Nov 01 2022 at 18:13):

Hi! I am writting some tactics and I would like to know how much time they are taking to run in a given context, for benchmarking purposes. Is there a way to get the current time in the TacticM monad?

Wojciech Nawrocki (Nov 01 2022 at 18:17):

@Tomaz Gomes Mascarenhas try IO.monoNanosNow

Wojciech Nawrocki (Nov 01 2022 at 18:17):

or IO.monoMsNow if millisecond resolution is enough

Tomaz Gomes Mascarenhas (Nov 01 2022 at 18:18):

awesome! Thanks @Wojciech Nawrocki

Last updated: Dec 20 2023 at 11:08 UTC