Win32 cross-compilation from debian: build of coqide.exe and other binaries

 Details will follow. In a word, we use a gtk+ win32 bundle from gtk.org
 to build some (unofficial) mingw32-liblablgtk2 debian packages. Then
  ./configure -local && ./build win32
 is enough to get all native win32 binaries and plugin cmxs from
 a confortable linux box.

 Next step: an auto-installer :-)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12804 85f007b7-540e-0410-9357-904b9bb8a0f7

Author: letouzey

build

@@ -18,7 +18,7 @@ rule() {
   case $1 in
     win32)  check_config
             sed -i 's/let arch = .*$/let arch = "win32"/' config/coq_config.ml && \
-	    $OCAMLBUILD toplevel/coqtop.native plugins/pluginsopt.otarget;;
+	    $OCAMLBUILD coq-win32.otarget;;
     clean)  ocb -clean && rm -rf bin/* && rm -f myocamlbuild_config.ml;;
     all)    ocb coq.otarget;;
     *)      ocb $1;;

coq-win32.itarget

@@ -0,0 +1,2 @@
+binariesopt
+plugins/pluginsdyn.otarget

myocamlbuild.ml

@@ -202,6 +202,9 @@ let binaries_deps =
     | (_,bin,_)::l -> (bin^best_oext) :: deps l
   in deps all_binaries
 
+let binariesopt_deps =
+  List.filter (fun s -> Filename.check_suffix s ".native") binaries_deps
+
 let ln_sf toward f =
   Command.execute ~quiet:true (Cmd (S [A"ln";A"-sf";P toward;P f]))
 
@@ -240,6 +243,7 @@ let extra_rules () = begin
 (** Virtual target for building all binaries *)
 
   rule "binaries" ~stamp:"binaries" ~deps:binaries_deps (fun _ _ -> Nop);
+  rule "binariesopt" ~stamp:"binariesopt" ~deps:binariesopt_deps (fun _ _ -> Nop);
 
 (** We create a special coq_config which mentions _build *)
 
@@ -324,8 +328,6 @@ let extra_rules () = begin
        Seq [Cmd (S [P w32ocamlc;cflags;A"-c";Px c]);
 	    mv  (Filename.basename o) o]);
 
-  if w32 then flag [ "ocamlmklib"; "c" ] (S[A"-ldopt";A ("-I "^w32lib)]);
-
 (** VM: Generation of coq_jumbtbl.h and copcodes.ml from coq_instruct.h *)
 
   rule "coqinstrs" ~dep:coqinstrs ~prods:[coqjumps;copcodes]

plugins/pluginsdyn.itarget

@@ -0,0 +1,23 @@
+field/field_plugin.cmxs
+setoid_ring/newring_plugin.cmxs
+extraction/extraction_plugin.cmxs
+firstorder/ground_plugin.cmxs
+rtauto/rtauto_plugin.cmxs
+fourier/fourier_plugin.cmxs
+romega/romega_plugin.cmxs
+omega/omega_plugin.cmxs
+micromega/micromega_plugin.cmxs
+dp/dp_plugin.cmxs
+xml/xml_plugin.cmxs
+subtac/subtac_plugin.cmxs
+ring/ring_plugin.cmxs
+cc/cc_plugin.cmxs
+groebner/groebner_plugin.cmxs
+funind/recdef_plugin.cmxs
+syntax/ascii_syntax_plugin.cmxs
+syntax/nat_syntax_plugin.cmxs
+syntax/numbers_syntax_plugin.cmxs
+syntax/r_syntax_plugin.cmxs
+syntax/string_syntax_plugin.cmxs
+syntax/z_syntax_plugin.cmxs
+quote/quote_plugin.cmxs