Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] [Coq-club] Way to check what is taking Coq so long to compute
  • Date: Sun, 28 Jan 2018 13:32:13 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay2-d.mail.gandi.net
  • Ironport-phdr: 9a23:qVWKIB/J1D1VA/9uRHKM819IXTAuvvDOBiVQ1KB30OocTK2v8tzYMVDF4r011RmVBdyds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+54Dfbx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRgL2hicJNzA382/ZhcJ/g61ZvB2vqAdyw5LXbYyPKPZyYq3QcNEcSGFcXshRTStBAoakYoUOFeUGIfpYoJP7p1QWrBW+BA2sC/jxxT9Smn/9wKo30+s7Hg7YwAwvBdQOvG7brNX0MKcdSv66zLPUzTjYdPNW2jf86JPLchAgpPGMWKx/cdDLxUkpCQzFkkydpIr4ND2WzuQAq3aX4/diWO61iWMrtxt9riWsy8oikIXFm4YYx1/c+Sln2ok5OcC0RUtlbtOqEJZdsiKXOJB3T88/Rmxnpjg2x70atZO+cigHx5UqyhzaZvCZb4SH/BzuWeOeLDp2n31qZreyiha9/ES+1+LxUNS/3kxQoSpfiNbMs2gA1xzN5ciDTftw5l2h1iiL1w/J6uBIP1k4mrfBJ54k2LEwl54TvV7MHiDsnkX5ka6Wel8i+ue29+TrerTmppmCOI9okgzyLLkil86lDek6LgQCRXWX9Oey2bH54EH0RLpHguUzkqbDsZDaIcobprS+Aw9Qyosj5AywACm60NsCm3kLNl1FeBODj4fyJV7OOuz4AOykg1SvkDZr3PPGPrzkApXIMHfDiq3tfbBj5E5A0AYz18xQ54pICrEdJ/L+QlP+tNvBDhMgLwO0x/vnB85m24MFWWOPB7eZP7nIvV+J4OIvOeiMa5UPtDbzMfh2r8Lp2HQ+gBoWebSj9ZoRcnGxWPp8cGuDZn+5rd6CDW4MiSU/SObnkkHKBTFaamq7WeQz5zUxBZi6JZzAV5uugbmE0T39GJBKMDMVQmuQGGvlIt3XE8wHbzifd5c4w240EIO5Qopk7imA8Qrzyr5pNO3Ro3NKrpHyz9t04ujej1c0+CAmVp3BgVHIdHl9myYzfxFzxLp2+BIv0VSSyqt5hvlVD5pV6u8bCl5nZ66Z9PRzDpXJYiyEftqNTwz7EM+rBTggFJc9hdoHYkI7FNykghGF2Se2UecY
Set Debug RAKAM for cbn
Set Debug Cbv for cbv (compute is an alias for cbv)

Gaëtan Gilbert

On 28/01/2018 10:15, Merlin Göttlinger wrote:
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

Archive powered by MHonArc 2.6.18.

Top of Page