The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

On Wed, May 25, 2011 at 03:34:25PM +0200, Pierre Corbineau wrote:
> There is no axiom-free term of type CC (just look at the normal form
> it would have).
> 
> You can even prove it:
> 
> Inductive CC : Prop := C1: (exists B : Prop,CC)->CC.
> 
> Lemma U:CC -> False.
> fix 1.
> intros [[ _ H]].
> apply U.
> apply H.
> Qed.
> 
> I would tend to interpret the segfault as a consequence of another
> unbounded recursion (undetected stack overflow).
> 
> Pierre
> 

i would suppose this crash is quite different from the previous testcase.

btw, gdb shows something weird (i don't see much memory used and the stack is 
not typical stack exhaustion IMO.):

$ gdb coqtop
Coq < Load crash.

Program received signal SIGSEGV, Segmentation fault.
0x0000000000a41187 in caml_fl_allocate ()
(gdb) bt
#0  0x0000000000a41187 in caml_fl_allocate ()
#1  0x0000000000a42fe9 in caml_alloc_shr ()
#2  0x0000000000a42208 in caml_oldify_one ()
#3  0x0000000000a3fe73 in caml_oldify_local_roots ()
#4  0x0000000000a42420 in caml_empty_minor_heap ()
#5  0x0000000000a42549 in caml_minor_collection ()
#6  0x0000000000a40a01 in caml_garbage_collection ()
#7  0x0000000000a4fc4e in caml_call_gc ()
#8  0x415c095380000000 in ?? ()
#9  0x4066800000000000 in ?? ()
#10 0x3f4af44580944580 in ?? ()
#11 0x415ba00000000000 in ?? ()
#12 0x0000000000000000 in ?? ()