Stream: Coq users

Topic: Stack overflow with coqc but not inside Proof General

Ana de Almeida Borges (Sep 09 2021 at 14:07):

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.

Guillaume Melquiond (Sep 09 2021 at 14:32):

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.

Paolo Giarrusso (Sep 09 2021 at 14:35):

Either that, or ulimit on the stack changes, directly or because of the size of the environment variables (how much does the threshold vary?)

Paolo Giarrusso (Sep 09 2021 at 14:37):

(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)

Ana de Almeida Borges (Sep 09 2021 at 16:21):

Proof General can handle a number about 15000 units larger.

Ana de Almeida Borges (Sep 09 2021 at 16:23):

What is ulimit?

Ana de Almeida Borges (Sep 09 2021 at 16:30):

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?

Emilio Jesús Gallego Arias (Sep 09 2021 at 16:44):

@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