Stream: Coq devs & plugin devs

Topic: Qed timing & universes


view this post on Zulip 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..)

view this post on Zulip Gaëtan Gilbert (Oct 20 2020 at 19:57):

It's a feature to improve your metrics

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Oct 21 2020 at 06:04):

It's a bug, please report with a way to reproduce

view this post on Zulip Janno (Oct 21 2020 at 08:16):

Done! https://github.com/coq/coq/issues/13230

view this post on Zulip Janno (Oct 21 2020 at 08:16):

It's really a bummer. I need to redo the last few weeks of measurements :(

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Janno (Oct 21 2020 at 10:28):

abstract seems to work. Thanks!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Oct 21 2020 at 12:41):

I don't have time today, sorry

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Oct 21 2020 at 14:33):

You are right, that is the bug.

view this post on Zulip Paolo Giarrusso (Oct 21 2020 at 15:40):

can one just swap record_pb_time with let proof, and is that easy to backport?

view this post on Zulip 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)

view this post on Zulip Gaëtan Gilbert (Oct 21 2020 at 16:25):

record_pb_time is about aux files, not the Time command modifier

view this post on Zulip Paolo Giarrusso (Oct 21 2020 at 18:00):

nevermind my silly question; I look forward to an MR.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 21 2020 at 18:23):

Ping me for more details in a different topic

view this post on Zulip Paolo Giarrusso (Oct 21 2020 at 18:25):

forwarding ping to @Janno


Last updated: Oct 16 2021 at 02:03 UTC