The Coq mailing list

[Santiago Zanella <Santiago.Zanella AT sophia.inria.fr>]

It seems that you're trying to compile Coq on an Intel Mac using a
PowerPC version of OCaml, since the generated instructions li and blr
are part of the PowerPC instruction set.

Regards

On Sun, 2007-09-30 at 15:24 +0200, "Vladimir Komendantsky" wrote: 
> Hi,
> Is there an svn version of coq that would compile successfully on i386 mac
> os x?
> 
> I've tried some versions between 10100 (28/08/2007) and 10150 (the last
> available). There, the error message looks like that:
> 
> OCAMLC4   parsing/g_tactic.ml4
> OCAMLC4   parsing/g_ltac.ml4
> OCAMLC4   parsing/g_constr.ml4
> Testing parsing/grammar.cma
> /tmp/camlasm11546e.s:16:no such instruction: `li r3,1'
> /tmp/camlasm11546e.s:17:no such instruction: `blr'
> Assembler error, input left in file /tmp/camlasm11546e.s
> make[1]: *** [parsing/grammar.cma] Error 2
> 
> I've also tried some earlier versions choosing at random and ending up
> with different errors.
> 
> Thanks and regards,
> 
> Vladimir
> 
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club