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: Merlin Göttlinger <megoettlinger AT gmail.com>
  • 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 12:49:11 +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-io0-f171.google.com
  • Ironport-phdr: 9a23:Ne78txPf5+Mtkbko2Z8l6mtUPXoX/o7sNwtQ0KIMzox0Lfr4rarrMEGX3/hxlliBBdydt6odzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlViDanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgIOT428mHZhMJzgqxGvhyuuwdyzJTIbIyPLvdyYr/RcNEcSGFcXshRTStBAoakYoUIEeUBJ+JYr4j7p1QWrBWmAxWsBP/ryj9JgH/20rM10/48GgzB2QwvAd0OsHPKo9XpKKcSVeG1zK/HzTrddfNbwjj96I3SfRAgpfGAR65/cc3UyUQ2EQ7Ok1ueqYvgPzyP1+QNtXCW7+tmVeK1im4osRt9oja1xsoql4LHhZoVx0ja+SllxIs5P961RU5hbdK6DpdduTuWO5Z0T88/RWxjpTw0xaccuZGheSgH0JQnyADba/yAa4WI5wjsVOeVITthhXJlf66ziw+88US9yODwS9O40FlNripCndnMsm4C2wbP5ciAT/tx5kah2TCR2ADP8uxIP1w4mK7BJ5MiwrM8jIQfvVrNEyPshUn7jrKael0h+uey6uTnZrvmpoWbN49xkgz+N7ohmsO4AesmLggOQ2yb+eW61L3s40L5Wq5HjvIzkqbDsZDaId4XqbK+Aw9Qyooj8QqwDy+60NQEmnkKNE5KeBWej4TwJ17OJO34AuykjlS3kDZrwujGMaf7DpXMKHjDirbhcqxn505S0gpghexYsplTE/QKJO/5ck73rt3RSBEjYCKuxOOyLdhn0oIYbk0RHrOdMaXdvEXAsuciLO6BeJMRuTDyJuIN6PvnjHt/klgYK/r6laALYWy1S6w1a36SZmDh149YQDU6+zEmRemvs2WsFDtaZnK8RaU5v2hpB4evDIOFTYeo0uXYgHWLW6ZOb2UDMWiiVG/yftzdCfgJYSOWZMRml25cDOXze8oazRir8TTC5f9nI+7ToHNKsJvi0J104LWWm0htrHp7CMOS12zLRGZxzDsF
If I set the RAKAM option I get 
Error: Anomaly "Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.

when evaluating simpl on the term with the Parameter nat.
If I don't set that then it just does not reduce but it doesn't crash.

Cheers,
Merlin

Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> schrieb am So., 28. Jan. 2018 um 13:32 Uhr:
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