The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

For what it's worth, the problem occurs in the printer:

Compute (let x:=computation1 in (fst x) + (snd x) - (snd x))

will compute properly. On the other hand,

Compute (snd computation1).

will fail with a stack overflow (tested in a recent trunk).

I have no idea what the problem is (it's not notation folding as Set Printing All doesn't help).


--
Arnaud Spiwack

On 19 January 2014 08:38, Michael Ganem <michael.ganem AT gmail.com> wrote:

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