Stream: Coq devs & plugin devs

Topic: Qed performance vs Defined

Jason Gross (Apr 24 2023 at 22:51):

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.

Jason Gross (Apr 24 2023 at 22:55):

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

Matthieu Sozeau (Apr 25 2023 at 09:16):

Do you see differences in universes between the two defs ?

Jason Gross (Apr 25 2023 at 21:23):

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

Last updated: Dec 05 2023 at 11:01 UTC