Make `gset` a `Definition` instead of `Notation`.
I mainly did do this because it often confused me that when using Set Printing All
occurrences of gset
are turned into mapset ...
.
However, it turned out this also has a positive effect on performance. On my machine, compilation of LambdaRust went from 34m2s to 33m1s, so that's an improvement of 3%. It had no significant effect on compilation times of Iris itself.
Merge request reports
Activity
mentioned in commit e2eb2948
Looks more like 1.5%, but still a nice improvement: https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&from=1552558081222&to=1552563078537&var-metric=instructions&var-project=lambda-rust&var-branch=master&var-config=All&var-group=(.*)%2F%5B%5E%2F%5D*
Edited by Ralf JungYeah I think there's a lot of noise in that... look at what happens when you include the prior change (which is a heap_lang only change and should have pretty much 0 effect on lambda-rust): https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&from=1552392472760&to=1552563977928&var-metric=time&var-project=lambda-rust&var-branch=master&var-config=All&var-group=(.*)%2F%5B%5E%2F%5D*
Yes, that's two changes. That's why we have three dots in the graph. The first change is the lambda locking, the second the gset change. The first changes hardly anything with "instructions", the second gives the 1.5% I mentioned here. What did you expect...?
Edited by Ralf JungIt seems to actually have a small negative impact on Iris itself though? https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&from=1552558727491&to=1552560733442
mentioned in issue iris#232 (closed)
FWIW, the diff for this perf change contains a few other commits as well: b938e033...e2eb2948