You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
MetaCoq adds many typeclass instances for commonly used classes such as Equivalence, Reflexive, PreOrder, etc. Unfortunately almost all of them are on hint transparent terms which means there is a very noticeable cost from failing unification attempts when calling reflexivity and other standard tactics.
While porting to 8.18 I noticed that the number of instances has almost doubled and with it the cost of (failing) calls to reflexivity in our development. It's hard to get exact numbers since the version bump changes other things but I estimate that the extra instances account for an overall slowdown between 2 and 4% in our development although there are (usually smaller) files where it accounts for double digit percentage points.
AFAICT there isn't a way to import sub libraries such as template-coq without also getting all these instances automatically.
I recommend adopting the usual policy of never declaring instances on terms whose head is hint transparent.
The text was updated successfully, but these errors were encountered:
We now have a more detailed data point on this: we actually got a 10% speedup overall (on our whole Coq development) by removing all imports of MetaCoq, which we only really relied on for lens generation (we now use elpi instead).
We are however still interested in getting this fixed, because we might need to use MetaCoq again in the future, and other projects would certainly benefit as well.
MetaCoq adds many typeclass instances for commonly used classes such as
Equivalence
,Reflexive
,PreOrder
, etc. Unfortunately almost all of them are on hint transparent terms which means there is a very noticeable cost from failing unification attempts when callingreflexivity
and other standard tactics.While porting to 8.18 I noticed that the number of instances has almost doubled and with it the cost of (failing) calls to
reflexivity
in our development. It's hard to get exact numbers since the version bump changes other things but I estimate that the extra instances account for an overall slowdown between 2 and 4% in our development although there are (usually smaller) files where it accounts for double digit percentage points.AFAICT there isn't a way to import sub libraries such as template-coq without also getting all these instances automatically.
I recommend adopting the usual policy of never declaring instances on terms whose head is hint transparent.
The text was updated successfully, but these errors were encountered: