Need some ocaml help: coq rebuild failing
Richard W.M. Jones
rjones at redhat.com
Fri Jun 22 13:28:09 UTC 2012
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
More information about the devel
mailing list