coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] [Coq-club] Way to check what is taking Coq so long to compute

From: Merlin Göttlinger <megoettlinger AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] [Coq-club] Way to check what is taking Coq so long to compute
Date: Sun, 28 Jan 2018 09:15:28 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=megoettlinger AT gmail.com; spf=Pass smtp.mailfrom=megoettlinger AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f54.google.com
Ironport-phdr: 9a23:9FQPCx8NtHN//f9uRHKM819IXTAuvvDOBiVQ1KB41+scTK2v8tzYMVDF4r011RmVBdyds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+54Dfbx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRxDohikJNDA37X/ZhdBrga1BvB6svQZyz5LIbIyXMvd1Y6PTfckdRWpERstfUDJOApm4b4sOCeoOJedWt4/hp1sSqRu+BA+sBOzxxT9Sm3T72qg63PouEQHBwgMgA84OsHDVrNXzO6cdT/q1wbLHzTXGdfxW2DP95JLUfRAmpPGBRLR9etfSx0k3Dw7JkEmcpIj/Mz6W1ukBqXaX4/dvWO61i2MqpAd8qSW1yMg2kInGnIcVx0jE9SpnxIY1IsW1SEthbt6lFJtcriCaN5dqTs87TWFluCk3xqcJuZ68eygKx5AnyADFZ/ObdIiI5wrvVOeXIThmmHJoYKyziwq2/ES6yeDxVtO43EhXoidKiNXBtn8A2wTW6sedS/t9+kmh2SyI1wDW8uxEJF47laXcK5E/3r4wip4TsUXFHi/5hkr2lrSbdkoh+uey6uTnZq/qqYObN49xkg3+KLghmtSjAeQkNQgDR3SU+eOl1LH64UL5RKhKgeYtn6nCsJHaINwbqbSjDw9U1IYj8Re/AC283NQWh3lUZG5CLViMiJGsMFXTKtj5C+2+ihKiin0jk/vBJ/jqBojHBnnFirboO7hnvR1y0g02mPVS/ZZVDIYuvu7vXk73u9HCRks8PgOzzvr7DNR72Y4EcW2KC66ddqjVtAnbtaoUP+CQadpN637GIP8/6qu21C5rqRomZaCsmKAvRjW9F/ViLV+eZCO10NgEGGYO+AE5Sb6z0QHQYXtof3+3GpkEyHQjEov/VNXMQ4mshPqK2yLpRsQLNFADMUiFFDLTT6vBW/oIb3jPcMpokzhBVKT5DoF8iVehswj1z7chJe3RqHUV

Hi,

I have a complicated computation on which Coq takes a very long time (or never terminates?) to execute (Compute statement or simpl in interactive proofs) even on rather simple inputs (extremely simple inputs terminate immediately though).

Is there some option to debug what Coq is currently doing, similar to Set Typeclass Debug?

Or what is the recommended way to hunt down such complications?

Cheers,

Merlin

[Coq-Club] [Coq-club] Way to check what is taking Coq so long to compute, Merlin Göttlinger, 01/28/2018
- Re: [Coq-Club] [Coq-club] Way to check what is taking Coq so long to compute, Matthieu Sozeau, 01/28/2018
  - Re: [Coq-Club] [Coq-club] Way to check what is taking Coq so long to compute, Merlin Göttlinger, 01/28/2018
    - Re: [Coq-Club] [Coq-club] Way to check what is taking Coq so long to compute, Maxime Dénès, 01/28/2018
- Re: [Coq-Club] [Coq-club] Way to check what is taking Coq so long to compute, Gaëtan Gilbert, 01/28/2018
  - Re: [Coq-Club] [Coq-club] Way to check what is taking Coq so long to compute, Merlin Göttlinger, 01/28/2018