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.

added 2 commits

• d0961b67 - Make `mapset_countable` a global instance.
• dfec102c - Make `gset` a `Definition` instead of `Notation`.

Compare with previous version

Sounds good! 3% for such a tiny change is big.

mentioned in commit e2eb2948

merged

Merged!

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*

That's good.

The difference in time is much bigger, 7.3%. Does it fluctuate that much between runs? I.e. are these differences normal even if nothing much changed.

Yeah 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*

But even when using "instructions" there are huge differences in the numbers at the link you just posted.

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...?

Oh, now I see. I was just looking at the table, totally ignoring the graph.

It 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

Hmm, theories/algebra/gset.v became 78.65% slower. That's suspicious indeed.

Should I open an issue to track this?

Please do.

mentioned in issue iris#232 (closed)

FWIW, the diff for this perf change contains a few other commits as well: b938e033...e2eb2948