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
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
line 78, character 28-29:
Error: No interpretation for numeral 0.
make: *** [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?