I'm seeing some weird numbers in CI for the Gaia project:
What has changed to give this kind of speedup?
This is strange... where do you read these numbers?
one of the opam subpackages goes from 2min2s to 3min43s
Docker-Coq CI is obviously not completely time-reliable, but this is probably way beyond the margin of error
I saw it repeating across several CI runs, but I think will actually try to replicate locally
What about this? https://github.com/coq/coq/pull/15782 (see also https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Very.20slow.20algorithmic.20in.20Ssreflect.20rewrite)
Here the bench we had: https://gitlab.com/coq/coq/-/jobs/2189555265
I mean, mathcomp is very similar, but on projects using ssr rewrite like metacoq it was a 20% speedup.
Do you use a lot the multi-rule rewrite feature, as in
Could it also be a delayed sideffect of this: https://github.com/math-comp/math-comp/issues/698? Where most of the time was lost in cbn...
Gaia uses quite a lot of multiple-rule rewrites, but not the syntax
OK, I tried
time make locally for Gaia, and I get:
possibly the highest proportional speedup I've seen for a project across a version
based on skimming the discussion, seems likely PR 15782 is the "culprit"
it could also be an arbitrary composition of https://github.com/coq/coq/pull/15753, https://github.com/coq/coq/pull/15770 and the other PR
(there are other non-MC related performance PRs in master, that may also have an effect)
Last updated: Aug 11 2022 at 02:03 UTC