Stream: Coq users

Topic: ✔ Coq 8.17 is *fast*


view this post on Zulip John Wiegley (Feb 03 2023 at 20:42):

Just wanted to note here something that at first I thought was an anamoly: 8.17 builds my category-theory library in half the time of 8.14-8.16.

8.17: make  616.46s user 12.84s system 99% cpu 10:31.18 total
8.16: make  1263.15s user 11.21s system 99% cpu 21:16.27 total
8.15: make  1220.32s user 11.18s system 99% cpu 20:33.46 total
8.14: make  1230.05s user 13.58s system 99% cpu 20:45.65 total

view this post on Zulip Gaëtan Gilbert (Feb 03 2023 at 20:53):

to a large degree because of https://github.com/coq/coq/pull/15807

view this post on Zulip Enrico Tassi (Feb 03 2023 at 21:06):

Well done! @Gaëtan Gilbert @Pierre-Marie Pédrot @Janno

view this post on Zulip Gaëtan Gilbert (Feb 03 2023 at 21:28):

there was also a significant speedup in https://github.com/coq/coq/pull/16371

view this post on Zulip Gaëtan Gilbert (Feb 03 2023 at 21:36):

Figure_1.svg
y = percent change for category-theory, negative is good
y = gitlab job number

the 2 big down spikes are https://github.com/coq/coq/pull/15807
the 1st big up spike is https://gitlab.com/coq/coq/-/jobs/2575167592
the 1st medium down spike is https://github.com/coq/coq/pull/16371
the 2nd medium down spike is https://gitlab.com/coq/coq/-/jobs/3131414631 (flambda vs not flambda)
the small down spike near the end is https://github.com/coq/coq/pull/16995

we also see small speed ups in https://github.com/coq/coq/pull/16107 and https://github.com/coq/coq/pull/15693

view this post on Zulip Janno (Feb 04 2023 at 09:34):

@Joshua Yanovski (Gitter import) deserves all the credit for the the initial implementation of delayed universe substitution. The PR is only in my name because we happened to be in my office at the time. All I did was complain loudly to anybody who would listen :)

view this post on Zulip Notification Bot (Feb 04 2023 at 16:53):

Laurent Théry has marked this topic as resolved.

view this post on Zulip Notification Bot (Feb 04 2023 at 19:17):

Laurent Théry has marked this topic as unresolved.

view this post on Zulip Notification Bot (Feb 06 2023 at 18:12):

John Wiegley has marked this topic as resolved.


Last updated: Jun 14 2024 at 18:01 UTC