I'm seeing some weird numbers in CI for the Gaia project:

- Coq-master on mathcomp-master takes around 8 min
- everything else (e.g., Coq-8.15 on mathcomp-1.13) takes 12-13 min

What has changed to give this kind of speedup?

This is strange... where do you read these numbers?

compare:

- https://github.com/coq-community/gaia/runs/5642992424?check_suite_focus=true (8min, 26s)
- https://github.com/coq-community/gaia/runs/5642992471?check_suite_focus=true (13min, 21s)

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 `rewrite (foo,bar,baz)`

?

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 `rewrite (X,Y)`

OK, I tried `time make`

locally for Gaia, and I get:

- 3m4s on Coq master + MC master
- 4m30s on Coq 8.15 + MC 1.14

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: Jul 24 2024 at 12:02 UTC