Stream: Coq users

Topic: Instance resolution takes a long time


view this post on Zulip Lef Ioannidis (Nov 09 2023 at 18:41):

A strange thing, instance resolution for the Reflexive instance of my relation takes a long time. But when I debug with Typeclasses eauto := debug very few instances are actually searched. How to debug what is taking so long? See attached images.

image.png
image.png

view this post on Zulip Gaëtan Gilbert (Nov 09 2023 at 18:42):

Set Debug "unification,tactic-unification".

view this post on Zulip Lef Ioannidis (Nov 09 2023 at 18:56):

Yes it seems tactic-unification is happening thousands of times over the same terms again and again. What is tactic-unification and what are some potential causes of this explosion?

view this post on Zulip Ike Mulder (Nov 09 2023 at 19:13):

I encountered something similar a while ago, but in my case the individual tactic-unification calls were slow.. Dropping this here since it might be helpful to you.

The problem there was that I had convertable terms, but the unification algorithm took a long time to actually establish this. This was due to unfortunate mismatch between some coercions and canonical structures.
It might be good to take a look at the implicit arguments of equ (?) and see if they look suspicious?

view this post on Zulip Ike Mulder (Nov 09 2023 at 19:17):

Ah and for debugging, you can follow the steps typeclass resolution takes with the autoapplytactic. When the TC log says it's doing simple apply @some_instance, it is actually doing something more along the lines of autoapply @some_instance with typeclass_instances. See also here.

view this post on Zulip Lef Ioannidis (Nov 09 2023 at 20:17):

Thanks for that answer, I did not know about autoapply. Some good news and bad news, setting
Typeclasses Filtered Unification makes this reflexivity instant but other lemmas (specifically rewrites) fail.

Another hint, like @Ike Mulder mentioned I thought canonical structures might causing the search space for unification to explode but I have eliminated all canonical projections I think, or at least
Print Canonical Projections. is empty.

Yeah I have no clue why this is happening. I can also try to disable overlapping instances one-by-one.

view this post on Zulip Janno (Nov 09 2023 at 21:52):

Try Set Typeclasses Debug Verbosity 2 to get some more output. It might show more failed attempts.

view this post on Zulip Janno (Nov 09 2023 at 21:53):

Set Ltac Profiling and Show Ltac Profile could be helpful to rule out Hint Extern but I am fuzzy on whether those actually show up in the profile

view this post on Zulip Janno (Nov 09 2023 at 21:56):

Another helpful trick is to turn the verbosity to 2, run the file through coqc and have the output timestamped line by line (using https://github.com/zmwangx/ets for example), ideally showing the difference to the previous line. This can help when individual instances take a long time. But beware that printing terms is very slow so large goals can skew the result quite a lot. Reducing the printing depth can sometimes help with that particular problem.

view this post on Zulip Janno (Nov 09 2023 at 22:00):

If nothing else helps you can get the list of hints (instances) from Print Hint Reflexive and remove all of them using Remove Hints (except for Hint Extern which cannot be removed). Then you can stop removing them one by one to see which one is slow. If there are a lot of instances there's a chance that it's just the sheer amount and no single one is responsible but it takes many hints to get to a point where a single search becomes noticeably slow.

view this post on Zulip Paolo Giarrusso (Nov 09 2023 at 22:01):

Generally, unification becomes generally unsafe when too many definitions can be unfolded, that's why math-comp uses sealing sometimes.

view this post on Zulip Paolo Giarrusso (Nov 09 2023 at 22:04):

This only answers about "potential causes", not how to find out — I think you'd see many unfoldings being attempted in a single unification call, but I've never debugged that through logs... I'd say this is mostly relevant if a single application takes a long time.


Last updated: Jun 13 2024 at 21:01 UTC