Need some ocaml help: coq rebuild failing

[Richard W.M. Jones]

On Fri, Jun 15, 2012 at 05:09:17PM -0600, Jerry James wrote:
> On Thu, Jun 14, 2012 at 10:01 PM, Jerry James <loganjerry at gmail.com> wrote:
> > I'm having a problem with building the coq package for the new OCaml
> > 4.00.0, and I'm at my wits' end.  There were some bad interactions
> > between the new OCaml, camlp5, and coq which I think I have
> > successfully worked around.  (It isn't pretty, but it seems to do the
> > job.)  But now, after the tools are built, the documentation building
> > step is failing due to seemingly random segfaults in the coqdoc tool.
> 
> I patched a few more things in the coq build process for OCaml 4 today
> and got builds that went all the way to completion in my 64-bit and
> 32-bit Fedora Rawhide VMs.  I rejoiced and kicked off a koji build,
> which failed with a segfault in coqdoc during the 32-bit build again:
> 
> http://koji.fedoraproject.org/koji/taskinfo?taskID=4168975
> 
> The apparently random pattern of segfaults makes me suspect that the
> garbage collector is involved somehow.  Has anybody had experience
> with a relatively long-running OCaml 4 program (one that would go
> through multiple rounds of collecting garbage)?

I would also suspect code generation or GC.  Did you try asking on
upstream Coq / OCaml mailing lists?

Having said that, relatively long-running programs are working OK for
me.

Rich.

-- 
Richard Jones, Virtualization Group, Red Hat http://people.redhat.com/~rjones
virt-df lists disk usage of guests without needing to install any
software inside the virtual machine.  Supports Linux and Windows.
http://et.redhat.com/~rjones/virt-df/