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.

What is `ulimit`

?

I'm not sure how `coqtop`

and `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: Jun 14 2024 at 18:01 UTC