I have a case where, with `Ltac admit := abstract case proof_admitted.`

`Time admit. Time Qed.`

takes 0.053+0.17 s`Time abstract (intros; lazymatch goal with |- @typing ?cf ?Σ ?Γ ?t ?T => pose proof (@quotation_check_valid config.strictest_checker_flags Σ0 Γ t T) as H' end; clear H'; admit). Time Qed.`

takes 0.195 + 7.062 s (!!!!)`Time abstract (intros; lazymatch goal with |- @typing ?cf ?Σ ?Γ ?t ?T => pose proof (@quotation_check_valid config.strictest_checker_flags Σ0 Γ t T) as H' end; clear H'; admit). Time Defined.`

takes 0.161 + 0.2 s

What might be going on such that simply posing and clearing a lemma, which takes practically no time to check on its own, makes `Qed`

take 40x longer than `Defined`

?

Some things of note:

- removing
`abstract`

does not change performance, neither of`Defined`

nor`Qed`

- before this line, there are no context variables (all have been reverted into the goal)
- I tried throwing in a
`match goal with |- ?T => refine (@id T _) end`

to ensure that the issue is not that the goal has an expensive type when checking in the kernel, to no avail.

(Reported at https://github.com/coq/coq/issues/17523, hopefully the bug minimizer can give a smaller test-case)

Do you see differences in universes between the two defs ?

As @Gaëtan Gilbert suggested here, it seems that `Unset Private Polymorphic Universes`

makes `Qed`

instantaneous

Last updated: Jul 13 2024 at 02:02 UTC