compiling coq with the ocaml mingw32 cross-compiler

[Pierre Letouzey]

[[ Hi all. As Stephane mentionned to me, I should have added
   debian-ocaml-maint list to the CC, so let's do that now.
   For completeness sake, I leave the full previous message,
   even if my (short answer) is almost at the end ]]


On Fri, Feb 26, 2010 at 08:34:21AM -0600, Romain Beauxis wrote:
> Le vendredi 26 février 2010 06:57:54, Pierre Letouzey a écrit :
> > On Tue, Feb 23, 2010 at 09:10:27PM +0000, Richard Jones wrote:
> > > 
> > > It would be great if Debian could push changes for cross-compilation
> > > back upstream.  Perhaps this is something we will be able to discuss
> > > at the OCaml Users Conference in April?
> > > 
> > 
> > Yes, that would be nice...
> 
> Agreed. But some of them need to be made more generic before..
> 
> > > 
> > > In Fedora we maintain over 100 mingw32-* packages (not OCaml
> > > specifically, but many C and C++ libraries), and there are often quite
> > > a lot of changes from upstream and from the native package.
> > 
> > Indeed, I should have started looking in this direction. In particular
> > I've now found your mingw32-ocaml-lablgtk.spec, but in fact after
> > having made my own mingw32-lablgtk2*.deb. I should try to factorize
> > the two someday.
> > 
> > > > Yes, this can be an issue. In general, I recommend to set the PATH with
> > > > the  cross-compiler binaries first:
> > > >   export PATH=/usr/i586-mingw32msvc/bin:$PATH
> > >
> > > 
> > > Oooo, I don't like this at all.  This is not necessary for any Fedora
> > > cross-compiled packages, so I'm not clear why it should be needed for
> > > Debian ones.
> > > 
> > 
> > As I said earlier I indeed think this export PATH should (and can) be
> > avoided as much as possible.
> 
> Agreed. The problem comes from some build systems that hardcode ocaml compiler 
> or use `which ocamlc`
> 
> > So anyway, here's the current status of my effort to cross-compile Coq:
> > 
> > - With the help of Stephane Glondu, we now have debian packages for
> >   mingw32-{camlp5,gtk2,lablgtk2}, see http://debian.glondu.net/mingw32
> > 
> > - With these packages, my initial goal is fulfilled: I'm able to
> >   compile the native opt win32 binaries for coq (including gtk gui
> >   coqide) while comfortably seated in front of my linux box. I've even
> >   prepared a windows installer by re-using a nsis script of someone of
> >   our group. I still have to thoroughly test these binaries, but
> >   initial tests look ok :-)
> > 
> > - My mingw32-gtk2 package is a "fake", I was too lazy to properly
> >   adapt gtk2 and its dependencies. I think that even with indications
> >   coming from the fedora mingw32-*.spec, this is a non-trivial task.
> >   Instead, this .deb repacks an official gtk+-bundle-2.8.17*-win32.zip
> >   coming from ftp.gnome.org.
> > 
> > - My mingw32-lablgtk2 is quite stripped-down: only gtk, no extensions
> >   such as glade, sourceview, gnome-ui or whatever. Moreover it only
> >   contains the "opt" files. Concerning byte version, the build fails
> >   on ocamlc (and hence ocamlrun) trying to load a .so while a .dll has
> >   been produced. To reproduce the issue, simply replace "lablgtkopt"
> >   with "all" in debian/rules. Since I'm focused on getting native .exe
> >   binaries, I've gladly ignored this :-) ...
> > 
> > - But I've nonetheless spent some time trying to understand what's
> >   going on. And I got the feeling that current ocamlrun and ocamlc
> >   from mingw32-ocaml aren't really emulating a mingw32 environment.
> >   For instance:
> > 
> >   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.
> 
> >   Similarly:
> >   
> >   /usr/i586-mingw32msvc/ocamlmktop -o mytop
> >   ./mytop
> >   print_string Sys.os_type;;  (* answers Unix *)
> 
> >   [Btw this ocamlmktop isn't working out-of-the-box, since
> >    toplevellib.cma isn't installed by mingw32-ocaml.]
> 
> This is more an issue. Should I patch the package to include toplevellib.cma ?
> Shouldn't the result of mktop be a binary for windows ?
> 

Yep, that would be nice. But as I told you earlier, I'm not that much
interested in bytecode binaries, so I'm not sure it worths spending too
much time on this matter. 


> >   So, are these ocamlrun/ocamlc/ocamlmktop meant to have different
> >   behavior than the /usr/bin/ ones ? If this is not the case, maybe
> >   they could simply be removed from the package...
> 
> I do not want to remove ocamlrun from the package. These binaries are ABI 
> dependant with the version of ocaml. For instance, when I had ocaml 3.11.2 as 
> main ocaml and ocaml 3.11.1 as cross-build ocaml, compilation would fail with 
> the cross-compiler because the ocamlrun used was the one from 3.11.2 and it 
> was not ABI compatible with 3.11.1.
> 
> For this reason, the package now ships its own ocamlrun in order to be 
> independant as much as possible from the "normal" ocaml.
> 

I see your point, and that sounds completely reasonable. Btw, that
reminds me that I should test and fix someday the dependencies of my
mingw32-* temptative packages, since they are currently rather
"bricolage". In particular, dependencies toward the regular ocaml or
gtk packages could certainly be totally removed.


> >   When looking at the build process of ocamlrun, I first noticed that
> >   byterun/libcamlrun.a was not remade after switching to the mingw
> >   config/Makefile. But then I realized that ocamlrun itself was not
> >   a remade one, otherwise we would have had a ocamlrun.exe. Which
> >   by the way would be handy to create -custom win32 byte .exe...
> >   Not that I care much about byte when opt is working, but that
> >   might interest some other persons.
> 
>  I believe there should be more work to do with byterun compilation, indeed..
> 
> 
> Romain

Best regards,

Pierre