Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Debugging an apparently diverging Coq program

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Debugging an apparently diverging Coq program


Chronological Thread 
  • From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Debugging an apparently diverging Coq program
  • Date: Mon, 23 Sep 2019 15:05:27 +0000
  • Accept-language: en-CA, en-US
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=none; dmarc=none; dkim=none; arc=none
  • Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=P8KLKiq1vbZr+a6KkeO6SZ3oHfDDbBpUgK7+3dOjwIU=; b=m1kZxp66y14FparM3JR/EjM2gcdYWpK7q6dYvRGRjdpS3VhP0NfLmfL6MPybmVFgNWK2N8f6beAZnp/u6QwwSaSGdgX/D1InAcGFvLR9wuDAYeL/RhEAd9JzPlX+CMMhw+6+jlsc1+Le0PIOr25FivWA5mMcL+i7z9ndiaM+B6z/i65q5Izt8LYQGFskT3+Bs5aTfmDH52xYkpKtbbXVuZ4o2IZkM0iManhQez0oOSG3OxvrieOqy5iBhjqRQy3VyP3EFMKknUiEeuiV6dfyLWFyaoW4twP0AHv1lOQYKKV+Fl+nh0kmGZ+8Dd/fEZcC0FTa1anOq/yAGY14av3DAw==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=bY+HjyPws/rezAk3oaADVBuGZ/XXoKIjBtLpOl84q0+9skDus5JVIh3ZWDrvz1w226lktozla2XnWWwJlzdHRQf3j3eqp6FrKGknbCPWlxYjUrdr6cWza2ndeMwVc6NCd+QjDoUwMjbVT9daN9lKZr/TmUp2QPlHAH9jkewLEiv02PyW4PcnwNtFPpwvtSzHqqi+yJhwPCzrxiqP7vCHHLBVsY7mhaJxsQdSMUo4WjWXpU9DDvr1WNAtTydjOTWBfVU4ETeKxqdbSHyMTZzyD9tDJ0bvi4VZTEyO/GyQ88ltv/WPyVJ4w8bEQpRMddlY3gwOWt0P/WHuYiSQUFJzlw==
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM01-SN1-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:4LUHCBOvb4B+JcYxYZ8l6mtUPXoX/o7sNwtQ0KIMzox0I/v7rarrMEGX3/hxlliBBdydt6sfzbCG+PC4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCezbL9oMhm7rgrdu8oKjYB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRjnhjoaNz4i6GHYlNB/jL5VrhKmohxw2Y/UYIeIP/Z6ca7QedYWSGxcVchTSiNBGJuxYYsRAeQcIeZWoYrzp1UMohSiCgahH/ngxiNUinLswaE2z+QsHAfb1wIgBdIOt3HUoc3xOqgISuC1y6/IxijaY/xV2Tf9747Ich88qv+RXbJ/b8zRyUY2GwjYjFuQtJHuMjSb1usQs2ia7vFgWfyzh2I6tw18uTivxsAwionMnI0Vy1TE+T9lz4YyIN21UUh2asOqHptXsiGVLYp2QsU6Tm50vyY60LsGtoC/fCgO0pgo2QPQa+Gff4iH4xLjSOaRISpji35/ebK/gA6+8Uehyu3gVsm0zU1FojBZndnLs3AA0QHY5MufSvZl8UqtxSyD2gTN5u1eP0w4j7fXJ4Ihz7IomJocr0fOEjPzlUjzjaKbeUop9vat5uj6YLjrqYGQOopqhQz8KKshhsmyDvolPgQQQ2SW//m32qf58k3jWrpKi+U7kqnHv5DeIsQWvra3DhNS3Io/9hqzFiqo3swFkXUeK1JKYwyIg5LuO1HTPPD3FvC/g0mqkDh23fzGJqfhApLRLnfdjLjhYbd960layAYpytBf+o5UCrUGIPL0WU/9rsDXDhg8MwCswubnDsty1p8GVG+AHqOVKqffvUGS6u4xOeWAeZMZtTblJ/gg/fHujHs5mVEHfamu2JsacH64EelmI0SYenrgnMsNHXoWsgclTOzqj0GCUTtJaHazW6Iw/C00CIWjDYvbXICinKSB3DunHp1Rfm1JFleMEW7xe4qYX/cMdTmdL9R6kj0EULihU5Uu2QuvtA/80bpnL/Db9jcWtZL5h5BJ4LiZnhYrsDdwEs610meXTmgykHlCD2s927k6qkhgwH+C17J5irpWD4oAyelOV1IYPIXbyaQ/OdD1XA2JRdeETlnjCvW7SWU/QtIj2IVWOh5VG9K+ixnC22yhBLpDxO/DP4A97q+Jhyu5HM160XuTiPh40wsWB/BXPGjjvZZRshDJDteSwUWei6OjdKBa1ynIpj/anDi++XpAWQs1ap3rGHUWZ0/Yt9P8vxiQT7iyDL0mNk1KzsvQc/IXOO2stk1PQbLYAPqbY2+1nDvvVzCh4+vVKbHMIiAa1iibD1UYmQcO+3rALRI5Giqqv2PZCnppCE7rZETvt+J5rSHiQw==
have you tried to extract to ocaml or haskell to reduce noise from Prop?

Thanks,
Jason Hu
https://hustmphrrr.github.io/
From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of William J. Bowman <wilbowma AT ccs.neu.edu>
Sent: September 20, 2019 8:46 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Debugging an apparently diverging Coq program
 
I don’t think that’s the problem. Another model does get stuck on that equality and returns the if statement waiting for an interpretation of “==“. I didn’t expect Program to be efficient, but I do expect it to terminate quickly on this example, without using 20 GB of memory.

I’ll see if I can reduce the other model to something as small.

-- 
Sent from my phoneamajig

On Sep 20, 2019, at 17:35, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Perhaps they forgot to instantiate the atom type?  the computation would get stuck on (x == x'). `Program` often produces humongous functions.

On Fri, Sep 20, 2019 at 5:15 PM William J. Bowman <wjb AT williamjbowman.com> wrote:
All,

At the following URL is a model of a language with capture-avoiding substitution
that a student wrote:

  https://gist.github.com/wilbowma/acf125222c64ff715a33b26a0ce8b4ab

The program looks (to me) like it ought to terminate quickly, and it's proven
terminating using Program, yet when we run the substitution function on a small
example... coqtop eats about 20 GB of memory and doesn't terminate within 5
minutes.
I'm using Coq 8.9.1 on MacOS 10.14.2; the same behavior is also observed on
Windows 10.

I'd appreciate any help debugging this.

--
William J. Bowman

Archive powered by MHonArc 2.6.18.

Top of Page