Instances created with ':= ltac:(_)' are much slower than Definitions

Using Coq
1

I’m trying to have a succinct notation for defining instances using a tactic. However, it seems that defining instances this way may cause a significant slowdown. I’m afraid a self-contained example will be hard to extract, but my situation is similar to the following:

Class C (arg : Prop) :=
   class_def : arg -> arg. (* some complicated prop dependent on arg *)

Ltac solve := unfold C; intros a; exact a. (* some expensive tactic *)

Instance holds1 : C True := ltac:(solve). (* takes 3 minutes for the actual instance *)
Definition holds2 : C True := ltac:(solve). (* takes 25 seconds .. *)
Instance holds3 : C True. Proof. solve. Defined. (* takes 25 seconds .. *)
Instance holds4 : C True. Proof. solve. Qed. (* takes 25 seconds .. *)

Does anyone have an idea what might cause this? I would expect that at least holds1 and holds2 take the same amount of time.

2

Hi @snyke7 , this is to some extent a known issue [which must be documented], but IMHO, given the slowdown you are observing, I’d suggest you submit a bug upstream, thanks!