coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] very long setoid_rewirte

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] very long setoid_rewirte
Date: Tue, 30 May 2017 15:40:34 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wr0-f176.google.com
Ironport-phdr: 9a23:jFZmURMN5F1LI7IdNlMl6mtUPXoX/o7sNwtQ0KIMzox0Lfj5rarrMEGX3/hxlliBBdydsKMazbeJ++C4ACpbsMnH6ChDOLV3FDY7yuwu3DYcSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9FYHdldm42P6v8JPPfQpImCC9YbRvJxmqsAndrMcbjI9jJ6oryhbEoGZDd+BKyW91P16ekRLx68Wq8JJ/7yhcvu8q+tJdX6n9Y6k3QrtUASg8PWwy+MPlqwTIQxGV5nsbXGUWkx5IDBbA4RrnQJr/sTb0u/Rk1iWCMsL4Ub47WTK576d2UxDokzsINyQ48G7MlMN9ir9QrQ+7qBx+x47UZ5yVNOZ7c6jAc94WWXZNU8BMXCFHH4iybZYAD/AZMOhYoYfzpEYAowWiCgS3Huzj1iVFi2Xq0aEm0eksFxzN0gw6H9IJtXTZtNr6O70PXuC0yanD0DbMYOlS2Tf89ojHaA0qrPaSXbNxa8XRzUgvFx3fgViLtYPlOi6V2v4TvGeG8uptTOSigHMkpQFpujWj2Nsgh43Tio8Wyl3I7zh1zJg2KNGiVUJ2Y9+pHZ1NvC+ALYR2WNktQ2RwtSY61LIGvZm7cTAPyJs9xh7fb+WLcoaS4h7/TeqRLyp0iXBkdb6liBay9k+gyuL4VsaqylpFsi1FktzUunAM0Rzc9NSHR+Nj8ku93TuDzQPe5+FeLUwpi6bWKIQtzqMym5cSqUjDGzX5mETyjK+YbEUk/e2o5vz5Yrr8u5CcNop0hhv/M6s0nsy/APo4PRIVUmmV5+u8z6Hj8VflT7VPk/06iLfWv43HJcgDvK62HxdV0po/6xa4FzqpzNMYnWAeIF1ZfBKHkpPmNkrVIPH4CPe/m06jnC1qx/DAJL3hA4/CImLNkLf7Lv5B7BtXzxN2xtRC7bpVDKsAKbT9QBzfrtvdWyEwPw2xi9TuDNRj38tKR3CGBq6HOYvZtELO6+4ydbrfLLQJsSrwfqB2r8XlimU0zAcQ

Hi!

I am performing a sequence of setoid rewrites using lemmas in the form of "Foo: equiv A B". The _expression_ is not very complex and typical application of 'setoid_rewrite' tactics take from seconds to few minutes with most time spent in type class resolution for Proper morphisms. However, for the next rewrite I am trying to perform it suddenly took 6 hours! Most interestingly it is not a type resolution which takes the longest. I tried to enable all kind of debug and here is what it looks like:

Set Typeclasses Debug.

Set Typeclasses Debug Verbosity 2.

Set Debug Auto.

Set Debug Eauto.

Set Ltac Debug.

setoid_rewrite Foo

Stepping through LTAC debug I get the following messages:

1. Going to execute: setoid_rewrite Foo

2. g_rewrite::setoid_rewrite@0> $o $c

2. Evaluated term: Foo (repeated 49 times)

After that Coq goes silent for about 6 hours and finally says:

Debug: Starting resolution with 7 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded

At this point, it quickly resolves type classes and finishes.

I am wondering what is taking so much time and how I can debug and optimize it. Thanks!

CMU ECE PhD candidate

Mobile: +1(510)220-1060

[Coq-Club] very long setoid_rewirte, Vadim Zaliva, 05/31/2017