The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

On Friday 20 March 2009 11:04:45 
hugo.herbelin AT inria.fr
 wrote:
> 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.

I run into stack overflows often when calling vm_compute on goals that 
generate 
large terms e.g. 5000 * 5000. Is there anything that can be done to stop Coq 
from causing a segmentation fault in such cases? I would find a function (in 
OCaml or a Coq tactic) that tries to reduce a term but gives up if it grows 
too big to be useful here.

Regards,

Sean