Need some ocaml help: coq rebuild failing

[Richard W.M. Jones]

On Thu, Jun 21, 2012 at 03:51:52PM -0600, Jerry James wrote:
> On Sun, Jun 17, 2012 at 3:45 AM, Richard W.M. Jones <rjones at redhat.com> wrote:
> > I would also suspect code generation or GC.  Did you try asking on
> > upstream Coq / OCaml mailing lists?
> 
> No, I haven't.  But see below.
> 
> > Having said that, relatively long-running programs are working OK for
> > me.
> 
> How about on i386?  I haven't had a single problem on x86_64; all of
> the failures I've seen have been on i386.  Yesterday, I tried building
> again to see if anything had changed.  It had.  The plugin
> compilations were failing because, apparently, -fPIC had not been
> passed to the compiler when building the shared objects.  I poked at
> it for a little bit before giving up.  Today I tried building again to
> try to localize that problem ... and now I'm getting this:
> 
> bin/coqtop.opt -boot    -nois -compile theories/Init/Peano
> File "/home/jamesjer/rpmbuild/BUILD/coq-8.3pl4/theories/Init/Peano.v",
> line 78, character 28-29:
> Error: No interpretation for numeral 0.
> make[1]: *** [theories/Init/Peano.vo] Error 1
> 
> This is getting weirder and weirder.  I don't even know where to start
> looking.  I'd believe my i386 VM is damaged somehow, except I'm seeing
> these kinds of problems on koji builds, too.  Have you tried running
> nontrivial OCaml programs on an i386 platform?

No, I gave up on i386 a while back.

It still sounds like a code gen bug though, so I would attempt to make
a minimal program that demonstrates the bug, and/or try and see if
upstream can help, and/or look through existing bugs to see if
anything is suggested: http://caml.inria.fr/mantis/my_view_page.php

Rich.

-- 
Richard Jones, Virtualization Group, Red Hat http://people.redhat.com/~rjones
libguestfs lets you edit virtual machines.  Supports shell scripting,
bindings from many languages.  http://libguestfs.org