Stream: Coq users

Topic: Stack overflow with coqc but not inside Proof General


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?)

view this post on Zulip 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)

view this post on Zulip Ana de Almeida Borges (Sep 09 2021 at 16:21):

Proof General can handle a number about 15000 units larger.

view this post on Zulip Ana de Almeida Borges (Sep 09 2021 at 16:23):

What is ulimit?

view this post on Zulip 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?

view this post on Zulip 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: Jan 29 2023 at 01:02 UTC