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

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

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

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

@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 :)

Laurent Théry has marked this topic as resolved.

Laurent Théry has marked this topic as unresolved.

John Wiegley has marked this topic as resolved.

Last updated: Jun 14 2024 at 18:01 UTC