coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Intuition tactic sometimes runs very slow

From: scott constable <sdconsta AT syr.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Intuition tactic sometimes runs very slow
Date: Mon, 23 May 2016 11:34:57 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=sdconsta AT syr.edu; spf=None smtp.mailfrom=sdconsta AT syr.edu; spf=None smtp.helo=postmaster AT smtp1.syr.edu
Ironport-phdr: 9a23:rbeR5xyryKwg+5XXCy+O+j09IxM/srCxBDY+r6Qd0ekRIJqq85mqBkHD//Il1AaPBtWKrakVwLOM6ejJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6DyZ/mnLnoodX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVWqLjOq88ULZwDTI8Mmlz6te4mwPESF6U7XwATi0dlRxTHwHP6ByyCoz9uSz8rfZ08DKLJ4v7Qa1iCmfq1LtiVBK90HRPDDU+6myC0sE=

Hi All,

On my latest project, I have noticed that the intuition tactic can sometimes run for an extraordinary amount of time, for instance 26 seconds in the worst case. I can't seem to replicate this behavior with a small example. The project in which I'm noticing the slowdown is roughly 2000 LoC. Is this the expected behavior for the intuition tactic? And what might be causing this?

Thanks in advance,

~Scott Constable

[Coq-Club] Intuition tactic sometimes runs very slow, scott constable, 05/23/2016
- Re: [Coq-Club] Intuition tactic sometimes runs very slow, Matthieu Sozeau, 05/23/2016
- Re: [Coq-Club] Intuition tactic sometimes runs very slow, Tej Chajed, 05/23/2016