Stream: Coq devs & plugin devs

Topic: 3395


view this post on Zulip Gaëtan Gilbert (Oct 22 2020 at 13:18):

Did unification get faster recently? I've been seeing unreliable ci failures on https://github.com/coq/coq/blob/fe095cd8b63e363e82953503cb84a851296c1965/test-suite/bugs/opened/bug_3395.v#L218

view this post on Zulip Gaëtan Gilbert (Oct 22 2020 at 13:18):

eg https://gitlab.com/coq/coq/-/jobs/805870575 (but the other test suite jobs passed)

view this post on Zulip Pierre-Marie Pédrot (Oct 22 2020 at 13:30):

For once that somebody complains that Coq is getting faster...

view this post on Zulip Pierre-Marie Pédrot (Oct 22 2020 at 13:31):

It might just be the runner that is faster?

view this post on Zulip Pierre-Marie Pédrot (Oct 22 2020 at 13:31):

Such tests are known to be quite fragile anyways.

view this post on Zulip Maxime Dénès (Oct 22 2020 at 13:32):

I never understood why we had tests ensuring that we stay slow, TBH

view this post on Zulip Gaëtan Gilbert (Oct 22 2020 at 13:32):

speed limits are important

view this post on Zulip Maxime Dénès (Oct 22 2020 at 13:32):

lol

view this post on Zulip Gaëtan Gilbert (Oct 22 2020 at 13:33):

why did the coq cross the road? because it was going too fast to stop

view this post on Zulip Pierre-Marie Pédrot (Oct 22 2020 at 13:35):

If anything, it's not the unification, in the example that is supposed to fail it's kernel conversion that is taking all the time.

view this post on Zulip Pierre-Marie Pédrot (Oct 22 2020 at 13:36):

the two lines are the same, aren't they?

view this post on Zulip Pierre-Marie Pédrot (Oct 22 2020 at 13:37):

Like, we're literally checking that some command takes a minimal amount of time, not that it's algorithmically prohibitive???

view this post on Zulip Paolo Giarrusso (Oct 22 2020 at 18:14):

and why does the comment contradict the Fail Timeout?

view this post on Zulip Paolo Giarrusso (Oct 22 2020 at 18:15):

any chance this was a sensible part of a sensible performance bug, but turning it into a test was an oversight?


Last updated: Oct 16 2021 at 07:02 UTC