coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] eauto loops

From: Matthieu Sozeau <mattam AT mattam.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] eauto loops
Date: Mon, 27 Jun 2016 17:14:46 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f41.google.com
Ironport-phdr: 9a23:uLo3KhctYTndFHryX7GmdjYulGMj4u6mDksu8pMizoh2WeGdxc65Zh7h7PlgxGXEQZ/co6odzbGH6+a5ACdZucvJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/mj6brotaKO1gArQH+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBK79ZuEzSaFSJDUgKWE8osPx5jfZSg7aw3IATmUXnwcAOA/X4RjnFsP0uzfmv+9V3SCGIcTzC7cuVmLxvO9QVBb0hXJfZHYC+2bNh5kogQ==

Hi Vadim,

could you give a bit more context about this? Are you calling eauto or

typeclasses eauto for example?

Best,

-- Matthieu

On Mon, Jun 27, 2016 at 5:40 PM Vadim Zaliva <vzaliva AT cmu.edu> wrote:

Hi

I am facing a situation where eauto loops in type class resolution. Log fragment:

Debug: (* debug eauto : *)
Debug: 1 depth=5
Debug: 1.1: exact CarrierAsetoid on (@Setoid CarrierA CarrierAe)
Debug: 1.1: exact CarrierAsetoid on (@Setoid CarrierA CarrierAe)
Debug: 1.1: exact CarrierAsetoid on (@Setoid CarrierA CarrierAe)
Debug: 1.1: exact CarrierAsetoid on (@Setoid CarrierA CarrierAe)
Debug: 1.1: exact CarrierAsetoid on (@Setoid CarrierA CarrierAe)
Debug: 1.1: exact CarrierAsetoid on (@Setoid CarrierA CarrierAe)
Debug: 1.1: exact CarrierAsetoid on (@Setoid CarrierA CarrierAe)
Debug: 1.1: exact CarrierAsetoid on (@Setoid CarrierA CarrierAe)
Debug: 1.1: exact CarrierAsetoid on (@Setoid CarrierA CarrierAe)
Debug: 1.1: exact CarrierAsetoid on (@Setoid CarrierA CarrierAe)
...

What could be causing this and how to debug? It is a bit weird, as it loops
on applying single assumption indefinitely.

Vadim

--
CMU ECE PhD candidate
Mobile: +1(510)220-1060

[Coq-Club] eauto loops, Vadim Zaliva, 06/27/2016
- Re: [Coq-Club] eauto loops, Matthieu Sozeau, 06/27/2016
  - Re: [Coq-Club] eauto loops, Vadim Zaliva, 06/28/2016
    - Re: [Coq-Club] eauto loops, Matthieu Sozeau, 06/28/2016
      - Re: [Coq-Club] eauto loops, Vadim Zaliva, 06/28/2016