Janno (Oct 20 2020 at 19:28): Janno (Oct 20 2020 at 19:28):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..)
Gaëtan Gilbert (Oct 20 2020 at 19:57):It's a feature to improve your metrics
Emilio Jesús Gallego Arias (Oct 20 2020 at 22:12):Actually that seems quite weird @Janno , Time Qed should take the whole Qed into account, unless the STM is doing something bizarre, I dunno.
Enrico Tassi (Oct 21 2020 at 06:04):It's a bug, please report with a way to reproduce
Janno (Oct 21 2020 at 08:16):Done! https://github.com/coq/coq/issues/13230
Janno (Oct 21 2020 at 08:16):It's really a bummer. I need to redo the last few weeks of measurements :(
Janno (Oct 21 2020 at 08:17):Can anybody think of a workaround for this? I am stuck with 8.11 for the foreseeable future.
Gaëtan Gilbert (Oct 21 2020 at 09:21):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
Janno (Oct 21 2020 at 10:24):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.
Janno (Oct 21 2020 at 10:28):abstract seems to work. Thanks!
Pierre-Marie Pédrot (Oct 21 2020 at 10:39):@Janno universe printing being slow is likely a bug, if you have a small reproducible example I could have a look
Enrico Tassi (Oct 21 2020 at 12:40):The beg is likely someone messed up with partial application. Eg with_time f x y instead of with_time (f x) y
Enrico Tassi (Oct 21 2020 at 12:41):I don't have time today, sorry
Gaëtan Gilbert (Oct 21 2020 at 13:11):isn't it because we close_proof outside the timer? https://github.com/coq/coq/blob/9db73ef18c45238223f30a462fc2c6d20493d1d2/stm/stm.ml#L2256
Enrico Tassi (Oct 21 2020 at 14:33):You are right, that is the bug.
Paolo Giarrusso (Oct 21 2020 at 15:40):can one just swap record_pb_time with let proof, and is that easy to backport?
Paolo Giarrusso (Oct 21 2020 at 15:40):(just in case we do the backport internally, I’m not asking to release 8.11.3 for this)
Gaëtan Gilbert (Oct 21 2020 at 16:25):record_pb_time is about aux files, not the Time command modifier
Paolo Giarrusso (Oct 21 2020 at 18:00):nevermind my silly question; I look forward to an MR.
Emilio Jesús Gallego Arias (Oct 21 2020 at 18:23):@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.
Emilio Jesús Gallego Arias (Oct 21 2020 at 18:23):Ping me for more details in a different topic
Paolo Giarrusso (Oct 21 2020 at 18:25):forwarding ping to @Janno
Last updated: Oct 12 2024 at 12:01 UTC