Stream: math-comp devs

Topic: 40%+ speedup in master?


view this post on Zulip Karl Palmskog (Mar 22 2022 at 11:42):

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

What has changed to give this kind of speedup?

view this post on Zulip Cyril Cohen (Mar 22 2022 at 11:59):

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

view this post on Zulip Karl Palmskog (Mar 22 2022 at 12:04):

compare:

view this post on Zulip Karl Palmskog (Mar 22 2022 at 12:05):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Enrico Tassi (Mar 22 2022 at 12:12):

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

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Mar 22 2022 at 12:14):

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

view this post on Zulip 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...

view this post on Zulip Karl Palmskog (Mar 22 2022 at 12:28):

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

view this post on Zulip Karl Palmskog (Mar 22 2022 at 12:36):

OK, I tried time make locally for Gaia, and I get:

view this post on Zulip Karl Palmskog (Mar 22 2022 at 12:37):

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

view this post on Zulip Karl Palmskog (Mar 22 2022 at 12:40):

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

view this post on Zulip 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

view this post on Zulip 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