compiling coq with the ocaml mingw32 cross-compiler

[Richard W.M. Jones]

On Fri, Feb 26, 2010 at 08:38:48AM -0600, Romain Beauxis wrote:
> Le vendredi 26 février 2010 08:34:21, Romain Beauxis a écrit :
> > >   echo "print_string Sys.os_type" >> test.ml
> > >   /usr/i586-mingw32msvc/ocamlc -o test test.ml
> > >   ./test    # answers Unix
> > 
> > I believe bytecode compilation is plateform independant. Hence, when you
> >  run  the test with your own ocamlrun, it returns Unix.
> > 
> > This may also be the case with the shipped ocamlrun, but the bytecode
> >  should  still be executable under windows.
> 
> 8:36 toots at leonard /tmp% echo "print_string Sys.os_type" > test.ml
> 8:36 toots at leonard /tmp% /usr/i586-mingw32msvc/bin/ocamlc -o test test.ml
> 8:36 toots at leonard /tmp% /usr/i586-mingw32msvc/bin/ocamlrun ./test
> Unix
> 
> So the behaviour is the same in this case, although I am not sure what is 
> right and what is wrong there...

In general terms, you cannot run generated binaries at ./configure
time.  The reason is that running binaries doesn't work in the
cross-compiler case (consider if your cross-compiler generated ARM
binaries for example).

The best way to solve this is to include some sort of platform-
independent "pkg-config" type of shell script which produces the
information you need, and (because it's a shell script) can be run in
both the normal and cross-compilation cases.

Rich.

-- 
Richard Jones, Virtualization Group, Red Hat http://people.redhat.com/~rjones
virt-top is 'top' for virtual machines.  Tiny program with many
powerful monitoring features, net stats, disk stats, logging, etc.
http://et.redhat.com/~rjones/virt-top