coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Stack Overflow when running tail-recursive function on large input

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Stack Overflow when running tail-recursive function on large input
Date: Fri, 19 Jun 2020 22:27:44 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f45.google.com
Ironport-phdr: 9a23:MoFfcxXtU+QvKD+wj/9OmgPwTIbV8LGtZVwlr6E/grcLSJyIuqrYbBGCt8tkgFKBZ4jH8fUM07OQ7/m9HzVfvt3Q6jgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrrQjdrNQajIlgJ6o+zhbFvGZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhNwzY7bYoGbOvR9cK3AY90VWXFMUdxNWyFbGI6wc5cDAugHMO1Fr4f9vVwOrR6mCASwH+zvyj5IhmT23aIk0OQqDB3L3Ao6ENIIrXvfsdL4O70JXuC1zanI1jXDYO1V2Tvn8ofIdAouofeRUr5qcMrRyFUvFwzeg1WfrIzqJTKV1uAXv2eH6OpgUPuihmg6oA5+vjah3N0jipXVho0L0FDE8z10zok7K9CmRkB3fcOpHZpOuyybOIZ7Q98vTn1mtSg6xbMLvZG1cSkFxpko2xLTdviKfpWI7x/gSuucIDV1iWxmdb+5mh288lCgx/XiWsWo1FtGtClIn9nWunwQ1hHe69KLR/R980qnxD2BzRrc6vteLkAxjafbK4Auwro3lpcLtETMBC72mEHvgK+XcUUo5/Gk6+rob7jmvJOcOIh0igbxMqQqhMOzG/g3Mg8LX2SD+OS80qPs/VHhTblUkvE7lrPVvZPaKMgBu6K0Ag5Y3pws5hu/Fzum1c4XnXgDLFJLYhKHiI3pNknUL//jDfe/gk+skDd1yPDFJLHuGJPNIWLFkLj8Z7p96k9cyBY8zd1E6JJUD6sOIPP3WkPrqNPYCRo5PxSuw+n7ENV9yp8eWWWXD6CFN6PSqEaE6f4rI+mRf4AYoy39Kvgg5/72l3A1g14dfa+z3ZsWcn+0BPpmI1/KKUbr19wGCCIBuhc0BLjhj0THWjpObV6zWbg973c1EtT1I53EQ9WEiryAxye2HdV/YGlABhjYGH3odp6EVvRKYSSbJMMnkz0YWpCuToYg0VelswqsmOkvFfbd5iBN7cGr79Ny/eCGzUhjpwwxNNyU1iS2d08xm2oJQzEs26Um+B5yz16C1e5zhPkKTIUPtcMMaR8zMNvn98I/E8r7A1uTcdKASVLgSdKjU2loE4ABhuQWakM4IO2MyxDO2y3wXu0Qnr2PQZ0zq+fSgyW3KMF6xHLLkqImigt+Tw==

not sure about Mac, but that anti-functional stack size restriction can be removed for good by "ulimit -s unlimited" in linux

On Fri, Jun 19, 2020, 9:49 PM Hadas Zeilberger <hadas.zeilberger AT consensyshealth.com> wrote:

Hi,
I am writing a simple compiler from one imperative language to another. I have implemented this compiler as a tail-recursive function. Nonetheless, when I try to compute this function on an input over ~300KB, I receive a Stack Overflow error. I am running this on a Mac OSX, where the default stack size is 512KB.

The input is of the following format (CSeq c1 (CSeq c2 ...(CSeq c(n-1) cn))) where c1,..,cn are commands in the source language and CSeq denotes the sequence command of the source language. Stack Overflow occurs when run with compute, vm_compute and native_compute. I'm wondering if there is a more efficient representation for the input data? Any suggestions would be much appreciated.

Thanks,
Hadas

[Coq-Club] Stack Overflow when running tail-recursive function on large input, Hadas Zeilberger, 06/20/2020
- Re: [Coq-Club] Stack Overflow when running tail-recursive function on large input, Abhishek Anand, 06/20/2020
- Re: [Coq-Club] Stack Overflow when running tail-recursive function on large input, Xavier Leroy, 06/20/2020
- Re: [Coq-Club] Stack Overflow when running tail-recursive function on large input, Emilio Jesús Gallego Arias, 06/25/2020