The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

The problem is not bytecode, but the computation with unary numbers. The 
output of your expression should be (8, 40320): this second number in unary 
is... big. The computations to produce it will blow out the stack. Try using 
BinNat for more compact representation.
-Ian
----- Original Message -----
From: "Michael Ganem" 
<michael.ganem AT gmail.com>
To: 
coq-club AT inria.fr
Sent: Sunday, January 19, 2014 2:38:57 AM GMT -05:00 US/Canada Eastern
Subject: [Coq-Club] Stack overflow with byte code compilation

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