The following code stack overflows when it is compiled with
coqc and when I feed it into
coqtop through the terminal. However, it works fine from inside Proof General. How can this be?
From Coq Require Import ZArith. From mathcomp Require Import all_ssreflect all_algebra. From Coq Require Import Sint63. Definition nat_of_sint (n : int) : nat := match Sint63.to_Z n with | Zpos p => nat_of_pos p | _ => 0 end. Lemma problem a b : (a * Posz (nat_of_sint 86000) + b)%R = (a * 86000 + b)%R. Proof. congr (_ + _)%R. Qed.
My initial guess would be that, for some reason, the
coqtop executable as configured in Proof General is not the one you get on the command line.
Either that, or
ulimit on the stack changes, directly or because of the size of the environment variables (how much does the threshold vary?)
(Off-topic: you probably know but I'd just not convert 86000 to an unlocked unary
nat — you want the binary
N if computation is not blocked)
Proof General can handle a number about 15000 units larger.
I'm not sure how
Proof General!coqtop could be different. I'm pretty sure they are running the same version of Coq, though I guess it could be that some flags are different? How to debug that, though?
@Ana de Almeida Borges
ulimit is a Unix tool that set process limits, for example, you can increase stack size with it, so stack overflows do happen less often
Last updated: Oct 04 2023 at 23:01 UTC