Stream: math-comp devs

Topic: 40%+ speedup in master?

Karl Palmskog (Mar 22 2022 at 11:42):

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?

Cyril Cohen (Mar 22 2022 at 11:59):

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

Karl Palmskog (Mar 22 2022 at 12:04):

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)

Karl Palmskog (Mar 22 2022 at 12:05):

one of the opam subpackages goes from 2min2s to 3min43s

Karl Palmskog (Mar 22 2022 at 12:06):

Docker-Coq CI is obviously not completely time-reliable, but this is probably way beyond the margin of error

Karl Palmskog (Mar 22 2022 at 12:10):

I saw it repeating across several CI runs, but I think will actually try to replicate locally

Enrico Tassi (Mar 22 2022 at 12:12):

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)

Enrico Tassi (Mar 22 2022 at 12:12):

Here the bench we had: https://gitlab.com/coq/coq/-/jobs/2189555265

Enrico Tassi (Mar 22 2022 at 12:13):

I mean, mathcomp is very similar, but on projects using ssr rewrite like metacoq it was a 20% speedup.

Enrico Tassi (Mar 22 2022 at 12:14):

Do you use a lot the multi-rule rewrite feature, as in rewrite (foo,bar,baz)?

Cyril Cohen (Mar 22 2022 at 12:16):

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...

Karl Palmskog (Mar 22 2022 at 12:28):

Gaia uses quite a lot of multiple-rule rewrites, but not the syntax rewrite (X,Y)

Karl Palmskog (Mar 22 2022 at 12:36):

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

Karl Palmskog (Mar 22 2022 at 12:37):

possibly the highest proportional speedup I've seen for a project across a version

Karl Palmskog (Mar 22 2022 at 12:40):

based on skimming the discussion, seems likely PR 15782 is the "culprit"

Pierre-Marie Pédrot (Mar 22 2022 at 12:40):

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

Pierre-Marie Pédrot (Mar 22 2022 at 12:42):

(there are other non-MC related performance PRs in master, that may also have an effect)

Last updated: May 31 2023 at 03:30 UTC