Need some ocaml help: coq rebuild failing

Jerry James loganjerry at gmail.com
Thu Jun 21 21:51:52 UTC 2012


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?

Thanks,
-- 
Jerry James
http://www.jamezone.org/


More information about the devel mailing list