Stream: Coq devs & plugin devs

Topic: Qed performance vs Defined


view this post on Zulip Jason Gross (Apr 24 2023 at 22:51):

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

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:

view this post on Zulip 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)

view this post on Zulip Matthieu Sozeau (Apr 25 2023 at 09:16):

Do you see differences in universes between the two defs ?

view this post on Zulip 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: Jul 13 2024 at 02:02 UTC