From c0511de2634363029307aa35a1f41539bae905d0 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 18 Feb 2010 18:14:50 +0000
Subject: Experimental build of coqtop.exe + plugins via cross-compilation
 linux-->win32

 Ideally, just install the cross-compiler (mingw32-ocaml on debian)
 and launch ./configure -local && ./build win32

 For the moment, this needs some twicking of mingw32-ocaml, plus
 a mingw32-camlp5 which is not yet distributed. If you want to play with
 that, contact me...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12792 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 build           |  3 +++
 myocamlbuild.ml | 34 ++++++++++++++++++++++++++++++----
 2 files changed, 33 insertions(+), 4 deletions(-)

diff --git a/build b/build
index 26237b705b..96f2a07433 100755
--- a/build
+++ b/build
@@ -16,6 +16,9 @@ ocb()
 
 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;;
     clean)  ocb -clean && rm -rf bin/* && rm -f myocamlbuild_config.ml;;
     all)    ocb coq.otarget;;
     *)      ocb $1;;
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 825b8b3b52..ed27dda155 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -58,6 +58,20 @@ let _ = begin
   Options.ocamllex := A Coq_config.ocamllex;
 end
 
+let w32 = (Coq_config.arch = "win32")
+
+let w32pref = "i586-mingw32msvc"
+let w32ocamlc = w32pref^"-ocamlc"
+let w32ocamlopt = w32pref^"-ocamlopt"
+let w32ocamlmklib = w32pref^"-ocamlmklib"
+let w32lib = "/usr/"^w32pref^"/lib/"
+let w32bin = "/usr/"^w32pref^"/bin/"
+
+let _ = if w32 then begin
+  Options.ocamlopt := A w32ocamlopt;
+  Options.ocamlmklib := A w32ocamlmklib;
+end
+
 let ocaml = A Coq_config.ocaml
 let camlp4o = A Coq_config.camlp4o
 let camlp4incl = S[A"-I"; A Coq_config.camlp4lib]
@@ -174,8 +188,8 @@ let best_ext = if opt then ".opt" else ".byte"
 let best_iext = if ide = "opt" then ".opt" else ".byte"
 
 let coqtopbest = coqtop^best_oext
-let coqdepbest = coqdepboot^best_oext
-let coqmktopbest = coqmktop^best_oext
+let coqdepbest = coqdepboot^(if w32 then ".byte" else best_oext)
+let coqmktopbest = coqmktop^(if w32 then ".byte" else best_oext)
 
 let binaries_deps =
   let rec deps = function
@@ -301,6 +315,17 @@ let extra_rules () = begin
   flag ["compile"; "c"] cflags;
   dep ["link"; "ocaml"; "use_libcoqrun"] [libcoqrun];
 
+  (* we need to use a different ocamlc. For now we copy the rule *)
+  if w32 then
+  rule ".c.o"  ~deps:("%.c"::c_headers) ~prod:"%.o" ~insert:`top
+    (fun env _ ->
+       let c = env "%.c" in
+       let o = env "%.o" in
+       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]
@@ -347,10 +372,11 @@ let extra_rules () = begin
     let depsb = "coq_config.cmo" :: core_cma in
     let depideo = if is_ide then [ide_cmxa] else [] in
     let depideb = if is_ide then [ide_cma] else [] in
+    let camlbin = if w32 then S [A"-camlbin";A w32bin] else N in
     if opt then rule fo ~prod:fo ~deps:(depsall@depso@depideo) ~insert:`top
-      (cmd [P coqmktopbest;A"-boot";A"-opt";ideflag;incl fo;A"-o";Px fo]);
+      (cmd [P coqmktopbest;camlbin;A"-boot";A"-opt";ideflag;incl fo;A"-o";Px fo]);
     rule fb ~prod:fb ~deps:(depsall@depsb@depideb) ~insert:`top
-      (cmd [P coqmktopbest;A"-boot";A"-top";ideflag;incl fb;A"-o";Px fb]);
+      (cmd [P coqmktopbest;camlbin;A"-boot";A"-top";ideflag;incl fb;A"-o";Px fb]);
   in
   mktop_rule coqtop false;
   mktop_rule coqide true;
-- 
cgit v1.2.3