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 <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Debugging an apparently diverging Coq program
  • Date: Sat, 21 Sep 2019 00:47:58 +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=Sbpfn3wfLUfxYk+RTnT3C/4FhTbUlyOBSjdAniIb1B4=; b=dISYZdBlcS1QY80zUq3bk5kMhlFo/b+2QrCZjqLaAplIjYArEaXGl5hP+ux/e6q87vCMtfuvGgGK2G8BI4PegWIEDFH6J1AuIj0NhE8tGmoLuM8MyvZO2zIkfFD/UcVJKLOqmfJpqt76XFec0afyBupIrijdp30ocgb+cbyk4WPy1gEclXa9fqTGq6cRnXYOBHZIU150QuL6I4y2NKWw1FtjxF12IuTdeHQqWwMewjc8b6ntZJ8I/jc2PF9ESrbYBMgRBS0huZs72k83JnLL1GgcNQnX/DDnHg5ECZgiD0CVNnwEh/xDhaHaCfAwBzo/UeH5gCXxOJfdIHTYP7d2Kg==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=R9Sy8AKOU41PtsJtAaRf67BTi7JNnWQsv++48YtABSPlXGfTl9VjsnO4dEqGn0UWaKxK+64nMfEcaYJpFDWqHZ/M+uoU4PtOnw7znlkiGQc0HSrUSTOf1Nt6MszY2TLU/MomM3TELv3ic5s8SKahtuLQVNgxKjHraViU7XTigwsRJzBs4qj8+GMwlnNmMV82LvZwfLppBzOLDHHP8q9vTqt6P7wBLqk+q+BRjO7NqlrAOlGpD7T1S6zHvy2It6Ov2Gt+UdFYfvyb3EtAtL+9+ClEq6/fTANuubJqdzYrhEtvGb/RFGNqWH1CUO6uKwrBAoPHL5w3H0DzSnoi12uTbA==
  • 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 NAM03-CO1-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:pr5UlhxZXyDm+xHXCy+O+j09IxM/srCxBDY+r6Qd0uoWI/ad9pjvdHbS+e9qxAeQG9mCsLQe0KGN7OigATVGvc/b9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfQV6Kf7oFYHMks+5y/69+4HJYwVPmTGxfa5+IA+5oAnMuMQam5VuJ6g+xhbHoHZDZuBayX91KV6JkBvw+9m88IR//yhMvv4q6tJNX7j9c6kkV7JTES4oM3oy5M3ltBnDSRWA634BWWgIkRRGHhbI4gjiUpj+riX1uOx92DKHPcLtVrA7RS6i76ZwRxD2jioMKiM0/3vWisx0i6JbvQ6hqhliyIPafI2ZKPxzdb7act0HWGpBRd5RWDJdDYOgYYUPCO8BMvxZr4n7ulACqRSzCA2pCO7p1zRGhGL53bci3uohDw/IwRAgEdwNvnTartr6KKgdXPuvw6XU0TnOde9a1Sv95YXObxsvoeuMXbV1ccfJzUcgDRjFjlKWqYf4Jj+a1eQNs2+d7+pvSOmhlm4npB93ojig38snl4vHhp8IwV3D+yV23YY1JNyjSEJlfdKoDYdcujqaN4txXsMiRntnuCc+yrEcpZG7ey0KxY0hyhXCZfKHdI2I7QjiVOaXOTp3mHVleKi5hxms9UigzvfwWdep31ZXtiZFk9/MtmoM1xPJ8MSHROF98l+u2TaOywDT6vxELlsumaraLJ4t2rEwlpsPsUTDAy/5g1/6g7ORdkUh/OWj9ufpYq3+q5KTK4N4kAXzPro0lsG9G+g1NgsDU3CV+eui17Dv4Uj0TbBLg/A5naTVrpXXKdkZq6O2HQNY15gs5hSlADi61dkXg2QLIExZdB+BkoPnIUvBIOriAve6m1mskClkx/TBPrD5GpvAMn/NnKvvcLpk9UNS0Rc/wclY551PFL4NOvXzWlLttNPDCR85Lgq0zPv9BNVlzIMeXn6PDbGFP6POsF+I4eQvL/OLZI8IpDb9L/8l5/ntjXMjhVAdeqyp0YMWaHC+APtmP12UbHXwjtsbFWoGoBAyQe7whFCGUjNff3OyULg95jE/BoKmF4DDRoW1jbyPwSi7HpxXZntYBlyQDHvka56JW/cLaCKOJ89uiD0EVby7R4A90hGusRf2y6B7IerM5i0YqZXj2cBp6O3UjBE+7CB7D8CA026WVGx0hWMJRzou3K9lu0B9y1GD0bJ5g/NCD9BT6elJAU8GMsvXyPU/ANTvUEqVddCQDV2iX9+OADcrT9t3zcVYMGhnHND3rBnY2CziRo0VkLqETKc0/6TTmjDROo4pxXrGxrJ71wB+astIKWivh6o5/A/WUd2a236FnrqnIPxPlBXG832OmDbf5R0KYEtLSazAGEsnSA7Ot92gvRHCSKOrALUjdABGzJzac/oYWpjSlVxDAczbFpHbamO1lX23AE/TlLOLcI/jemFb1yLYWhFdzlIjuE2ePA17PR+P5mLTCDsySgDJSma0qqxVjyr+SUU5iQaXc0dmyry5vAYPguCRQO8S2bRCvzo9rzJzHxC22NeEUtc=
I suspect that Solve Obligations closes proofs transparently, which should consume much time to compute something irrelevant.

https://coq.inria.fr/refman/addendum/program.html#coq:flag.transparent-obligations
We present here the Program tactic commands, used to build certified Coq programs, elaborating them from their algorithmic skeleton and a rich specification .It can be thought of as a dual of Extraction.The goal of Program is to program as in a regular functional programming language whilst using as rich a specification as desired and proving that the code meets the specification using the ...
coq.inria.fr

> Controls whether all obligations should be declared as transparent (the default), or if the system should infer which obligations can be declared opaque.

Thanks,
Jason Hu
https://hustmphrrr.github.io/
From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Abhishek Anand <abhishek.anand.iitg AT gmail.com>
Sent: September 20, 2019 8:35 PM
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Debugging an apparently diverging Coq program
 
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