coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Intuition tactic sometimes runs very slow

From: Matthieu Sozeau <mattam AT mattam.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Intuition tactic sometimes runs very slow
Date: Mon, 23 May 2016 18:41:02 +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-f45.google.com
Ironport-phdr: 9a23:fMY4YhYp5F81kegv+34sc2P/LSx+4OfEezUN459isYplN5qZpc+ybnLW6fgltlLVR4KTs6sC0LqH9fuxEjVavN6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDjvcaCKFwS2XKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzAzmwZUAwnI8VnBWYX8uzay4u90xDWTOOXzRKwoUDHk6L1kHky7wBwbPiI0pTmEwvd7i7hW9Uqs

Hi,

It might be because intuition is using auto with * by default, you can try intuition idtac to see if that's the problem.

Best,

-- Matthieu

On Mon, May 23, 2016 at 8:35 PM scott constable <sdconsta AT syr.edu> wrote:

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