Is it a bug that
Time Qed does not report the actual time taken by the command but that it instead only reports the time it takes to check the term? In particular, the call to
Evd.minimize_universes does not seem to be tracked. (Guess how I found out..)
It's a feature to improve your metrics
Actually that seems quite weird @Janno ,
Time Qed should take the whole
Qed into account, unless the STM is doing something bizarre, I dunno.
It's a bug, please report with a way to reproduce
It's really a bummer. I need to redo the last few weeks of measurements :(
Can anybody think of a workaround for this? I am stuck with 8.11 for the foreseeable future.
going through abstract might work, but may be inconvenient depending on your proof script
Time Show Universes may work as an approximation of minimize time if that's the only concern
abstract is a good idea. I'll try that. The problem with
Show Universes is that printing the universes takes way longer than minimizing them.
abstract seems to work. Thanks!
@Janno universe printing being slow is likely a bug, if you have a small reproducible example I could have a look
The beg is likely someone messed up with partial application. Eg
with_time f x y instead of
with_time (f x) y
I don't have time today, sorry
isn't it because we close_proof outside the timer? https://github.com/coq/coq/blob/9db73ef18c45238223f30a462fc2c6d20493d1d2/stm/stm.ml#L2256
You are right, that is the bug.
can one just swap
let proof, and is that easy to backport?
(just in case we do the backport internally, I’m not asking to release
8.11.3 for this)
record_pb_time is about aux files, not the Time command modifier
nevermind my silly question; I look forward to an MR.
@Paolo Giarrusso this bug may take a while to fix IMO, on the other hand, if you need to measure now, there is a branch called "simple compiler" that should help you.
Ping me for more details in a different topic
forwarding ping to @Janno
Last updated: Dec 07 2023 at 17:01 UTC