The Coq mailing list

[Xavier Leroy <xavier.leroy AT college-de-france.fr>]

On Sat, Jun 20, 2020 at 6:49 AM 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.

It is possible (even likely) that the stack overflow occurs while Coq typechecks and translates the huge input, even before your functions are evaluated on this input.

It's impossible to be more precise without a repro case.

 

I'm wondering if there is a more efficient representation for the input data? Any  suggestions would be much appreciated. 

Extract your compiler to OCaml or Haskell, add a parser for your input language, and read your source from files.

Coq's built-in execution facilities are pretty good but lack efficient ways of inputting large data (as far as I know).  That's one of the cases where extraction is pretty much a necessity.

Hope this helps,

- Xavier Leroy

Thanks,

Hadas