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(a)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