The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

On Fri, Mar 20, 2009 at 12:04:45PM +0100, 
hugo.herbelin AT inria.fr
 wrote:
> 
> Most causes of segmentation fault in Coq are due to stack overflows
> that are most often fatal in native Objective Caml code (even with
> recent versions of O'Caml) and against which we don't know any kind of
> reasonable protection. This is especially the case of the bug reports
> #2064 and #1809.
>
> More generally, to check if a segmentation fault is indeed caused by a
> stack overflow, use coqide.byte (the byte-code version of CoqIde)

Aha, thanks for the info!

> Note also that a CoqIde lethal problem "double-free or corruption" has
> been recently observed with some Linux installations.

I don't know if this is useful, but with the bug 2064 example if I (in
coqide.byte):
    "Go to end"
    "Backward one command"
    "Forward one command"
then I get such an abort:
    *** glibc detected *** /usr/bin/ocamlrun: double free or corruption 
(!prev): 0x00000000009398a0 ***
    [...]

> A known
> workaround is to set the global variable MALLOC_CHECK_ to 0 ("export
> MALLOC_CHECK_=0" on bash-style shells or "setenv MALLOC_CHECK_ 0" on
> csh-style shells).

This does indeed work around it.


Thanks
Ian