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
eg https://gitlab.com/coq/coq/-/jobs/805870575 (but the other test suite jobs passed)
For once that somebody complains that Coq is getting faster...
It might just be the runner that is faster?
Such tests are known to be quite fragile anyways.
I never understood why we had tests ensuring that we stay slow, TBH
speed limits are important
why did the coq cross the road? because it was going too fast to stop
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.
the two lines are the same, aren't they?
Like, we're literally checking that some command takes a minimal amount of time, not that it's algorithmically prohibitive???
and why does the comment contradict the
any chance this was a sensible part of a sensible performance bug, but turning it into a test was an oversight?
Last updated: Jun 05 2023 at 09:01 UTC