The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.jussieu.fr>]

Hi,
There is a mac format for both 32 and 64 bits but ocamlc doesn't give  
way to use it. Neither directly but nor an easy way to build native  
code for one architecture on an other !
I know that it exists a cross compiler for windows so stuff can be  
done but I don't want to do neither the requested hack nor the build  
system to use it !

More over since ocaml package for mac is 32bits, I'll provide a  
package for "packages users" i e a 32b one ...

Anyway, if you need a independant 64b package right now, there is one  
here : http://www.pps.jussieu.fr/~pboutill/coq-night/coq-trunk-x86_64-2011-06-17.dmg

Pierre
Le 17 juin 11 à 10:35, Jean-Jacques Levy a écrit :

> Hello crowd!
>
> problem with coq-8.3pl2-macosx.dmg with following plugin:
>
> > coqc  -q  -R theories Ssreflect -R src Ssreflect   theories/ssreflect
> > File "/Users/levy/Downloads/ssreflect-1.3pl1/theories/ssreflect.v",  
> > line 5, characters 0-30:
> > Error: error loading shared library: dlopen(/Users/levy/Downloads/ 
> > ssreflect-1.3pl1/src/ssreflect.cmxs, 138): no suitable image  
> > found.  Did find:
> > 	/Users/levy/Downloads/ssreflect-1.3pl1/src/ssreflect.cmxs: mach-o,  
> > but wrong architecture
> > make[1]: *** [theories/ssreflect.vo] Error 1
>
> Disk image compiled with 32-bit option, but Ssreflect plugin is  
> compiled with 64-bit. There is this Mac format for having dual  
> formats 32+64. I think it would be preferable to distribute the dual  
> version. Moreover the standard on Mac will evolve to 64-bit.
>
> Best to all, -JJ-

Pierre Boutillier
pierre.boutillier AT pps.jussieu.fr