The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Nov 30, 2015, at 16:29 , Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

1) Typeclass resolution may be a reason for long rewrite times. If so, the following may help

Typeclasses eauto := 5 (* or a small number, to limit the depth of search  *)

Typeclasses eauto := debug

For more, see the last section of https://coq.inria.fr/refman/Reference-Manual022.html#sec673

Thanks!

I played with these options and experimentally determined that if I set:

  Typeclasses eauto := 7.

the ‘rewrite’ tactics application succeeds. Depths below 7 causes unresolved constraints. Any number above 7 works but takes exponentially longer time, which makes sense.  Apparently some non-essential branch goes too deep, but I am unsure which one. My intuition is to try to find which one and somehow  limit it, perhaps using  "Typeclasses Opaque”.

Any hints how to analyze the debug log? What should I look for? Here is partial log file:

http://bit.ly/1St2sZy

P.S. I tried breadth-first search as well.

Sincerely,
Vadim Zaliva

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060

Skype: vzaliva