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: Oct 13 2024 at 01:02 UTC