Stream: Coq users

Topic: Performance Debugging Typeclass Resolution


view this post on Zulip Jason Gross (Mar 01 2023 at 04:17):

Does anyone have tips for performance debugging / optimizing typeclass resolution in cases where it's slow (43 seconds for one goal), the typeclass log is short (177 Debug lines), there's almost no backtracking (only 4 instances of no match), and it does not seem to be the case that external tactics are particularly slow? (Do I just have too many instances in my tc database?)

If anyone else wants to take a stab at debugging, the code is here, and here's the TC debug log at verbosities 1 and 2 with each line annotated with the number of seconds Coq spent between printing the previous line and printing that line. tclog-verbosity-1.log tclog-verbosity-2.log

view this post on Zulip Jason Gross (Mar 01 2023 at 04:42):

Here is a particularly egregious example:

Debug:
Calling typeclass resolution with flags: depth = ,unique = false,do_split = true,fail = false
Debug:
1: looking for (ground_quotable (option Kernames.kername)) without backtracking
Debug: 1.1: simple apply @Init.quote_option on
(ground_quotable (option Kernames.kername)), 2 subgoal(s)
Debug: 1.1-1 : (quotation_of Kernames.kername)
Debug: 1.1-1: looking for (quotation_of Kernames.kername) without backtracking
Debug: 1.1-1.1: exact qkername on (quotation_of Kernames.kername), 0 subgoal(s)
Debug: 1.1-2 : (ground_quotable Kernames.kername)
Debug: 1.1-2: looking for (ground_quotable Kernames.kername) without backtracking
Debug: 1.1-2.1: exact Kernames.quote_kername on
(ground_quotable Kernames.kername), 0 subgoal(s)

Finished transaction in 3.407 secs (3.407u,0.s) (successful)

view this post on Zulip Gaëtan Gilbert (Mar 01 2023 at 07:40):

if you Time Definition foo := @quote_extend. after is it fast?
maybe there's something interesting if you also enable unification or tactic unification debug?
maybe you can run perf?

view this post on Zulip Paolo Giarrusso (Mar 01 2023 at 07:59):

+1 to (tactic) unification debug

view this post on Zulip Jason Gross (Mar 01 2023 at 22:12):

It does seem to be the case that Coq is spending a lot of time doing conversion problems that eventually fail.

If I have an instance for @foo nat with no arguments and a goal @foo nat, is there any way to get Coq to not try the dozens of other @foo _ instances I have, invoking conversion problems that eventually fail, before trying my @foo nat instance?

view this post on Zulip Pierre-Marie Pédrot (Mar 01 2023 at 22:14):

You can try to put explicit patterns in your instances. That will filter the goal syntactically.

view this post on Zulip Jason Gross (Mar 01 2023 at 22:19):

@Pierre-Marie Pédrot What does this look like? For example, I want to prevent

Debug: 1.1-1.1: exact Universes.QuoteUniverses2.ConstraintType.quote_t on
(ground_quotable nat) failed with: Cannot unify (ground_quotable ConstraintType.t) and (ground_quotable nat)

from showing up in the typeclass log (verbosity 2). Do I need to emit #[export] Typeclasses Opaque foo for every single ground_quotable foo instance? (And even this doesn't work if my goal is unfoldable, because then, instead of being sensible and unfolding my goal one step when there's no match, Coq seems to blindly simple apply every typeclass instance to the goal, repeatedly invoking the same conversion problem dozens or hundreds of times.)

view this post on Zulip Jason Gross (Mar 01 2023 at 22:19):

Are you saying that I need to do Hint Extern rather than Instance for every single typeclass hint?

view this post on Zulip Jason Gross (Mar 01 2023 at 22:20):

Maybe I should just do #[local] Hint Constants Opaque : typeclass_instances?

view this post on Zulip Paolo Giarrusso (Mar 01 2023 at 22:40):

Hint Externs are one strategy, otherwise you'll need opacity for heads both of goals and of instances — the alternative isn't sound

view this post on Zulip Paolo Giarrusso (Mar 01 2023 at 22:41):

If at least one is transparent, it could unfold to the other; so the dnet can only filter instances ahead soundly if both heads are opaque.

view this post on Zulip Paolo Giarrusso (Mar 01 2023 at 22:42):

(filtering isn't restricted to the head, but the head is still crucial)

view this post on Zulip Paolo Giarrusso (Mar 01 2023 at 22:45):

OTOH you might end up needing some things to be transparent for application to succeed (not in this case, I don't think); IIUC, opacity is used both by the dnet filtering and by the actual unification in class_apply

view this post on Zulip Paolo Giarrusso (Mar 01 2023 at 22:46):

(the debug logs mention simple apply but that's not accurate; class_apply is much closer)

view this post on Zulip Paolo Giarrusso (Mar 01 2023 at 22:46):

Everything I'm saying I've learned from @Janno ; mistakes are all mine


Last updated: Jun 15 2024 at 05:01 UTC