Permalink
Browse files

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

…naries

 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
  • Loading branch information...
1 parent d7534f6 commit 043532049cf272fd870294265707febc68d1e6a5 letouzey committed Feb 24, 2010
Showing with 30 additions and 3 deletions.
  1. +1 −1 build
  2. +2 −0 coq-win32.itarget
  3. +4 −2 myocamlbuild.ml
  4. +23 −0 plugins/pluginsdyn.itarget
View
@@ -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;;
View
@@ -0,0 +1,2 @@
+binariesopt
+plugins/pluginsdyn.otarget
View
@@ -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]
@@ -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

0 comments on commit 0435320

Please sign in to comment.