compiling coq with the ocaml mingw32 cross-compiler

[Romain Beauxis]

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...

I had to do a quick and dirty patch to ocamlc/ocamlopt in order to force them 
to return Win32 when invoking the -config option.

I believe there might be a better way to deal with issue...



Romain