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: Matthieu Sozeau <mattam AT mattam.org>
  • 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 10:24:19 +0000
  • Authentication-results: mail3-smtp-sop.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-f51.google.com
  • Ironport-phdr: 9a23:P7lYDhYMtV/x2l1BXRaOs2z/LSx+4OfEezUN459isYplN5qZocWzbnLW6fgltlLVR4KTs6sC17KP9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCagbb9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjE2/mHYiMx+gqxYrhy8uRJw35XZb5uJOPdkZK7RYc8WSGhHU81MVyJBGIS8b44XAuQGJ+lYs5X9p1sPrRSgGAmnGf7hyjhJh3Dox6I6zvkqHAbD3AM6A9IOrG7brNDuOacXS++10LXIwi/Gb/9M3jf98ofIfwknrPqRXrxwadLcxEsgGg/fk1mct4zoMymW2+gTqWSW7/dsWOSygGA9sQ5xuCKgxsI0h4nJmI0VzlfE+D18wIkvJN24TFd3YNChEJdMri2aOYt7Tt44T2FnvyY6zbIGuZqlcyQQ1JsnwBvfZ+SGc4iO/B3jSP6cLDV3iX5/Zb6zmRa//VKjx+HiTMW50EtGojJAktbWt3AN0xLT6tKASvt45kqh3CyA1xzP6uFEIEA7i7fbJ4Q6wr43l5scr17MHjLtlUX5ia+ZbEQk+uyy5+v7ZbXmo4eQN5VohQHmLqQuhsu/DPwkPQgJRmiX4Piz1Ln+/ULiW7hKlf03kqzBsJ/AP8gbp6i5AxVU0ok58Rq/AS2mg5wkmiwMK0sAcxaahaDoPUvPKbb2F6SRmVOpxRJi2+zGP7D8Sq7KPHXKjf+1eL9h90dZ4A860cxW4tRTEL5Xc6G7YVP4qNGNVkxxCAez2euyUIwshLNbYnqGB+qiCI2XtFaJ4uw1JOzVPd0avT/8L74u4Pu81CZly29YRrGg2N4sUF79Bu5veh/LZHPwnt4EV2AQsVhmFbG4uBi5STdWIk2Kcec86zU8Ut/0CI7CQsWyheTE0nriWJJRYW9CBxaHFnK6L4g=
Hi Merlin,

There might be many factors to slow computation, e.g. representation of data types, proofs in terms, mismatch between your assume evaluation strategy and the one implemented by Coq’s reduction functions. You might first want to try vm_compute or native_compute to have an idea if it is your encoding or just Coq’s relatively naïve default evaluator that is the culprit.

My 2 cents,
— Matthieu
Le dim. 28 janv. 2018 à 10:15, Merlin Göttlinger <megoettlinger AT gmail.com> a écrit :
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