diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /myocamlbuild.ml | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'myocamlbuild.ml')
-rw-r--r-- | myocamlbuild.ml | 113 |
1 files changed, 35 insertions, 78 deletions
diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 5b873fce..097a1042 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -58,7 +58,7 @@ let _ = begin Options.ocamllex := A Coq_config.ocamllex; end -let w32 = (Coq_config.arch = "win32") +let w32 = Coq_config.arch_is_win32 let w32pref = "i586-mingw32msvc" let w32ocamlc = w32pref^"-ocamlc" @@ -76,21 +76,18 @@ end let use_camlp5 = (Coq_config.camlp4 = "camlp5") -let camlp4lib = if w32 then w32lib^"ocaml/camlp5" else Coq_config.camlp4lib - let camlp4args = if use_camlp5 then [A "pa_extend.cmo";A "q_MLast.cmo";A "pa_macro.cmo"] else [] let ocaml = A Coq_config.ocaml let camlp4o = S ((A Coq_config.camlp4o) :: camlp4args) -let camlp4incl = S[A"-I"; A camlp4lib] +let camlp4incl = S[A"-I"; A Coq_config.camlp4lib] let camlp4compat = Sh Coq_config.camlp4compat let opt = (Coq_config.best = "opt") let ide = Coq_config.has_coqide let hasdynlink = Coq_config.has_natdynlink let os5fix = (Coq_config.natdynlinkflag = "os5fixme") -let flag_dynlink = if hasdynlink then A"-DHasDynlink" else N let dep_dynlink = if hasdynlink then N else Sh"-natdynlink no" let lablgtkincl = Sh Coq_config.coqideincl let local = Coq_config.local @@ -106,15 +103,16 @@ let _build = Options.build_dir (** Abbreviations about files *) let core_libs = - ["lib/lib"; "kernel/kernel"; "library/library"; + ["lib/clib"; "lib/lib"; "kernel/kernel"; "library/library"; "pretyping/pretyping"; "interp/interp"; "proofs/proofs"; - "parsing/parsing"; "tactics/tactics"; "toplevel/toplevel"; - "parsing/highparsing"; "tactics/hightactics"] + "parsing/parsing"; "printing/printing"; "tactics/tactics"; + "stm/stm"; "toplevel/toplevel"; "parsing/highparsing"; + "tactics/hightactics"] let core_cma = List.map (fun s -> s^".cma") core_libs let core_cmxa = List.map (fun s -> s^".cmxa") core_libs let core_mllib = List.map (fun s -> s^".mllib") core_libs -let tolink = "scripts/tolink.ml" +let tolink = "tools/tolink.ml" let c_headers_base = ["coq_fix_code.h";"coq_instruct.h"; "coq_memory.h"; "int64_emul.h"; @@ -128,9 +126,7 @@ let copcodes = "kernel/copcodes.ml" let libcoqrun = "kernel/byterun/libcoqrun.a" -let initialcoq = "states/initial.coq" -let init_vo = ["theories/Init/Prelude.vo";"theories/Init/Logic_Type.vo"] -let makeinitial = "states/MakeInitial.v" +let init_vo = "theories/Init/Prelude.vo" let nmake = "theories/Numbers/Natural/BigN/NMake_gen.v" let nmakegen = "theories/Numbers/Natural/BigN/NMake_gen.ml" @@ -160,7 +156,7 @@ let coqdepdeps = theoriesv @ pluginsv @ pluginsmllib let coqtop = "toplevel/coqtop" let coqide = "ide/coqide" let coqdepboot = "tools/coqdep_boot" -let coqmktop = "scripts/coqmktop" +let coqmktop = "tools/coqmktop" (** The list of binaries to build: (name of link in bin/, name in _build, install both or only best) *) @@ -172,7 +168,7 @@ let all_binaries = [ "coqtop", coqtop, Both; "coqide", "ide/coqide_main", Ide; "coqmktop", coqmktop, Both; - "coqc", "scripts/coqc", Both; + "coqc", "tools/coqc", Both; "coqchk", "checker/main", Both; "coqdep_boot", coqdepboot, Best; "coqdep", "tools/coqdep", Best; @@ -264,9 +260,9 @@ let extra_rules () = begin let lines = List.map (fun s -> s^"\n") lines in let line0 = "\n(* Adapted variables for ocamlbuild *)\n" in (* TODO : line2 isn't completely accurate with respect to ./configure: - the case of -local -coqrunbyteflags foo isn't supported *) + the case of -local -vmbyteflags foo isn't supported *) let line1 = - "let coqrunbyteflags = \"-dllib -lcoqrun\"\n" + "let vmbyteflags = [\"-dllib\";\"-lcoqrun\"]\n" in Echo (lines @ (if local then [line0;line1] else []), "coq_config.ml")); @@ -280,8 +276,8 @@ let extra_rules () = begin T(tags_of_pathname ml4 ++ "p4option"); camlp4compat; A"-o"; Px ml; A"-impl"; P ml4])); - flag_and_dep ["p4mod"; "use_grammar"] (P "parsing/grammar.cma"); - flag_and_dep ["p4mod"; "use_constr"] (P "parsing/q_constr.cmo"); + flag_and_dep ["p4mod"; "use_grammar"] (P "grammar/grammar.cma"); + flag_and_dep ["p4mod"; "use_constr"] (P "grammar/q_constr.cmo"); flag_and_dep ["p4mod"; "use_compat5"] (P "tools/compat5.cmo"); flag_and_dep ["p4mod"; "use_compat5b"] (P "tools/compat5b.cmo"); @@ -303,38 +299,17 @@ let extra_rules () = begin mlp_cmo "tools/compat5b"; end; - ocaml_lib ~extern:true ~dir:camlp4lib ~tag_name:"use_camlpX" - ~byte:true ~native:true (if use_camlp5 then "gramlib" else "camlp4lib"); - -(** Special case of toplevel/mltop.ml4: - - mltop.ml will be the old mltop.optml and be used to obtain mltop.cmx - - we add a special mltop.ml4 --> mltop.cmo rule, before all the others -*) - flag ["is_mltop"; "p4option"] flag_dynlink; - -(*TODO: this is rather ugly for a simple file, we should try to - benefit more from predefined rules *) - let mltop = "toplevel/mltop" in - let ml4 = mltop^".ml4" and mlo = mltop^".cmo" and - ml = mltop^".ml" and mld = mltop^".ml.depends" - in - rule "mltop_byte" ~deps:[ml4;mld] ~prod:mlo ~insert:`top - (fun env build -> - Ocaml_compiler.prepare_compile build ml; - Cmd (S [!Options.ocamlc; A"-c"; A"-pp"; - Quote (S [camlp4o; T(tags_of_pathname ml4 ++ "p4mod"); - A"-DByte";A"-DHasDynlink";camlp4compat;A"-impl"]); - A"-rectypes"; A"-impl"; P ml4])); - -(** All caml files are compiled with -rectypes and +camlp4/5 +(** All caml files are compiled with +camlp4/5 and ide files need +lablgtk2 *) - flag ["compile"; "ocaml"] (S [A"-rectypes"; camlp4incl]); + flag ["compile"; "ocaml"] (S [A"-thread";A"-rectypes"; camlp4incl]); flag ["link"; "ocaml"] (S [A"-rectypes"; camlp4incl]); flag ["ocaml"; "ide"; "compile"] lablgtkincl; flag ["ocaml"; "ide"; "link"] lablgtkincl; - flag ["ocaml"; "ide"; "link"; "byte"] (S [A"lablgtk.cma"; A"gtkThread.cmo"]); - flag ["ocaml"; "ide"; "link"; "native"] (S [A"lablgtk.cmxa"; A"gtkThread.cmx"]); + flag ["ocaml"; "ide"; "link"; "byte"] + (S [A"lablgtk.cma"; A"lablgtksourceview2.cma"]); + flag ["ocaml"; "ide"; "link"; "native"] + (S [A"lablgtk.cmxa"; A"lablgtksourceview2.cmxa"]); (** C code for the VM *) @@ -342,7 +317,7 @@ let extra_rules () = begin flag ["compile"; "c"] cflags; dep ["ocaml"; "use_libcoqrun"; "compile"] [libcoqrun]; dep ["ocaml"; "use_libcoqrun"; "link"; "native"] [libcoqrun]; - flag ["ocaml"; "use_libcoqrun"; "link"; "byte"] (Sh Coq_config.coqrunbyteflags); + flag ["ocaml"; "use_libcoqrun"; "link"; "byte"] (Sh Coq_config.vmbyteflags); (* we need to use a different ocamlc. For now we copy the rule *) if w32 then @@ -383,8 +358,8 @@ let extra_rules () = begin let core_mods = String.concat " " (List.map cat core_mllib) in let core_cmas = String.concat " " core_cma in Echo (["let copts = \"-cclib -lcoqrun\"\n"; - "let core_libs = \"coq_config.cmo "^core_cmas^"\"\n"; - "let core_objs = \"Coq_config "^core_mods^"\"\n"], + "let core_libs = \""^core_cmas^"\"\n"; + "let core_objs = \""^core_mods^"\"\n"], tolink)); (** For windows, building coff object file from a .rc (for the icon) *) @@ -395,41 +370,29 @@ let extra_rules () = begin Cmd (S [P w32res;A "--input-format";A "rc";A "--input";P rc; A "--output-format";A "coff";A "--output"; Px o])); -(** Embed the Coq icon inside the windows version of Coqide *) +(** The windows version of Coqide is now a console-free win32 app, + which moreover contains the Coq icon. If necessary, the mkwinapp + tool can be used later to restore or suppress the console of Coqide. *) if w32 then dep ["link"; "ocaml"; "program"; "ide"] [w32ico]; - if w32 then flag ["link"; "ocaml"; "program"; "ide"] (P w32ico); - -(** Ealier we tried to make Coqide a console-free win32 app, - but that was troublesome (unavailable stdout/stderr, issues - with the stop button,...). If somebody really want to try again, - the extra args to add are : - [A "-ccopt"; A "-link -Wl,-subsystem,windows"] - Other solution: use the mkwinapp tool. *) -(** The mingw32-ocaml cross-compiler currently uses Filename.dir_sep="/". - Let's tweak that... *) - - if w32 then begin - ocaml_lib "tools/win32hack"; - List.iter (fun (_,s,_) -> tag_file (s^".native") ["use_win32hack"]) - all_binaries - end; + if w32 then flag ["link"; "ocaml"; "program"; "ide"] + (S [A "-ccopt"; A "-link -Wl,-subsystem,windows"; P w32ico]); (** Coqtop *) let () = let fo = coqtop^".native" and fb = coqtop^".byte" in let depsall = (if w32 then [w32ico] else [])@[coqmktop_boot;libcoqrun] in - let depso = "coq_config.cmx" :: core_cmxa in - let depsb = "coq_config.cmo" :: core_cma in + let depso = core_cmxa in + let depsb = core_cma in let w32flag = if not w32 then N else S ([A"-camlbin";A w32bin;A "-ccopt";P w32ico]) in if opt then rule fo ~prod:fo ~deps:(depsall@depso) ~insert:`top - (cmd [P coqmktop_boot;w32flag;A"-boot";A"-opt";incl fo;camlp4incl;A"-o";Px fo]); + (cmd [P coqmktop_boot;w32flag;A"-boot";A"-opt";incl fo;A"-thread";camlp4incl;A"-o";Px fo]); rule fb ~prod:fb ~deps:(depsall@depsb) ~insert:`top - (cmd [P coqmktop_boot;w32flag;A"-boot";A"-top";incl fb;camlp4incl;A"-o";Px fb]); + (cmd [P coqmktop_boot;w32flag;A"-boot";A"-top";incl fb;A"-thread";camlp4incl;A"-o";Px fb]); in (** Coq files dependencies *) @@ -440,7 +403,7 @@ let extra_rules () = begin (fun env _ -> let v = env "%.v" and vd = env "%.v.depends" in (** NB: this relies on all .v files being already in _build. *) - Cmd (S [P coqdep_boot;dep_dynlink;A"-slash";P v;Sh">";Px vd])); + Cmd (S [P coqdep_boot;dep_dynlink;P v;Sh">";Px vd])); (** Coq files compilation *) @@ -461,8 +424,8 @@ let extra_rules () = begin in let coq_v_rule d init = - let bootflag = if init then A"-nois" else N in - let gendep = if init then coqtopbest else initialcoq in + let bootflag = if init then A"-noinit" else N in + let gendep = if init then coqtopbest else init_vo in rule (d^".v.vo") ~prods:[d^"%.vo";d^"%.glob"] ~deps:[gendep;d^"%.v";d^"%.v.depends"] (fun env build -> @@ -473,12 +436,6 @@ let extra_rules () = begin coq_v_rule "theories/Init/" true; coq_v_rule "" false; -(** Initial state *) - - rule "initial.coq" ~prod:initialcoq ~deps:(makeinitial::init_vo) - (cmd [P coqtopbest;A"-boot";A"-batch";A"-nois";A"-notop";A"-silent"; - A"-l";P makeinitial; A"-outputstate";Px initialcoq]); - (** Generation of _plugin_mod.ml files *) rule "_mod.ml" ~prod:"%_plugin_mod.ml" ~dep:"%_plugin.mllib" |