Explore performance implications of gen_proofmode
a74b8077 (more control over typeclass search) made lambdaRust noticeably slower. Also see the conversation following https://mattermost.mpi-sws.org/iris/pl/btp695ny3prqjdqzojw9sj5i9w. In particular:
yeah, the bottelneck is definitely notypeclasses refine: https://gitlab.mpi-sws.org/FP/LambdaRust-coq/-/jobs/9346 took 29:47 user time
btw we also have a 1min regression in this range: https://gitlab.mpi-sws.org/FP/LambdaRust-coq/compare/8799209d9c00f825e9ac059b3b864119e34f9aec...00b0c7704278028c4a73c9f0686a9070e92d3a06
and ~30sec over https://gitlab.mpi-sws.org/FP/LambdaRust-coq/compare/474f82283e423b03ccf0adeb367e36eb68346a29...8799209d9c00f825e9ac059b3b864119e34f9aec
Looking at the performance graph, the two commit ranges with the most sustained impact are LambdaRust-coq@c2c2b874eea8...00b0c7704278 and LambdaRust-coq@00b0c7704278...158d46797c99. They correspond to iris-coq@aa5b93f6319b9cb2d17a1c9f61947233b4033484...1a092f96 and iris-coq@1a092f96b1350896c3801edb90b453f5b4d2a4cf...a74b8077 in Iris. The latter is just a74b8077 (more control over typeclass search), but the former is just a whole bunch of commits that, altogether, seem to have made things slower by 40sec in LambdaRust.
There is also some variation in this part of the graph but I am not sure if that's real or just noise.