John Wiegley (Feb 03 2023 at 20:42): 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
to a large degree because of https://github.com/coq/coq/pull/15807
Enrico Tassi (Feb 03 2023 at 21:06):Well done! @Gaëtan Gilbert @Pierre-Marie Pédrot @Janno
Gaëtan Gilbert (Feb 03 2023 at 21:28):there was also a significant speedup in https://github.com/coq/coq/pull/16371
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
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 :)
Notification Bot (Feb 04 2023 at 16:53):Laurent Théry has marked this topic as resolved.
Notification Bot (Feb 04 2023 at 19:17):Laurent Théry has marked this topic as unresolved.
Notification Bot (Feb 06 2023 at 18:12):John Wiegley has marked this topic as resolved.
Last updated: Oct 04 2023 at 19:01 UTC
