diff options
| author | letouzey | 2010-02-24 19:30:09 +0000 |
|---|---|---|
| committer | letouzey | 2010-02-24 19:30:09 +0000 |
| commit | 043532049cf272fd870294265707febc68d1e6a5 (patch) | |
| tree | 5f99e3c01aa0d8b982361146ca2cd04c9c5ea963 | |
| parent | d7534f6f3c52eb2c1fdb91bbfa49a818f771fbb8 (diff) | |
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
| -rwxr-xr-x | build | 2 | ||||
| -rw-r--r-- | coq-win32.itarget | 2 | ||||
| -rw-r--r-- | myocamlbuild.ml | 6 | ||||
| -rw-r--r-- | plugins/pluginsdyn.itarget | 23 |
4 files changed, 30 insertions, 3 deletions
@@ -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;; diff --git a/coq-win32.itarget b/coq-win32.itarget new file mode 100644 index 0000000000..9e2c7a2b6b --- /dev/null +++ b/coq-win32.itarget @@ -0,0 +1,2 @@ +binariesopt +plugins/pluginsdyn.otarget diff --git a/myocamlbuild.ml b/myocamlbuild.ml index ed27dda155..cdf46542c7 100644 --- a/myocamlbuild.ml +++ b/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] diff --git a/plugins/pluginsdyn.itarget b/plugins/pluginsdyn.itarget new file mode 100644 index 0000000000..f44121ee4a --- /dev/null +++ b/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 |