The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

On Fri, Mar 20, 2009 at 01:02:17AM +0000, Ian Lynagh wrote:
> Assertion failure? Luxury! I just get segfaults when coq disagrees with
> me:
> 
> https://logical.saclay.inria.fr/coq-bugs/show_bug.cgi?id=2081
> https://logical.saclay.inria.fr/coq-bugs/show_bug.cgi?id=2064
> 
> I religiously save before running anything in coqide now...

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.

The segmentation fault reported in #2081 is however a true (apparently
C-zar specific) coq bug (maybe some bad use of magic).

More generally, to check if a segmentation fault is indeed caused by a
stack overflow, use coqide.byte (the byte-code version of CoqIde)
which survives stack overflows. If you still get a segmentation fault,
please report it, it is true Coq bug.

To periodically and automatically save your file in CoqIde, go to
Preferences, tab Files, and select "Enable auto-save" (in principle
this option is set by default). The saved files have names #foo.v#.

Note also that a CoqIde lethal problem "double-free or corruption" has
been recently observed with some Linux installations. 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).

Hope it helps.

Hugo Herbelin