The Coq mailing list

[Michael Ganem <michael.ganem AT gmail.com>]

Hi,

I try to run the following:

Definition computation1 :=
  (fun f h p => f (f (f h)) p)
    (fun g p => g (g p))
    (fun p => match p with (x, y) => (x+1, (x+1) * y) end)
    (0, 1).

Compute computation1.

on a Ubuntu machine. In this machine, Coq is compiled in byte code.

And I got "Stack overflow."

I try:

1. This calculation on another machine where Coq is compiled in native and it is ok.
2. In the same machine than 1, I compile Coq in byte code and got also "Stack overflow." on the  calculation.
   
3. In the original machine, I try to increase the stack limit using : ulimit -s 32000 and still the same problem.

The original machine is a ubuntu/ARM and the second machine is ubuntu/x86.
I did not manage to compile in native mode Coq on my original machine that s why I compiled it in byte code.

The problem seems to be linked to byte code compilation.

Has anyone a tip for this?

thanks,
Michael