From dff6f3dbed334ad1179cc1abf8708365c2309106 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 3 Apr 2009 17:18:11 +0000 Subject: Ocamlbuild: option for (not) building coqide, better log messages git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12048 85f007b7-540e-0410-9357-904b9bb8a0f7 --- config/coq_config.mli | 2 ++ configure | 1 + myocamlbuild.ml | 85 ++++++++++++++++++++++++++++++++------------------- 3 files changed, 56 insertions(+), 32 deletions(-) diff --git a/config/coq_config.mli b/config/coq_config.mli index 3598b938d..85d25ad73 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -59,5 +59,7 @@ val browser : string (** default web browser to use, may be overriden by environment variable COQREMOTEBROWSER *) +val has_coqide : string + val has_natdynlink : bool val natdynlinkflag : string (* special cases of natdynlink (e.g. MacOS 10.5) *) diff --git a/configure b/configure index 894e43d64..88bb0fe52 100755 --- a/configure +++ b/configure @@ -994,6 +994,7 @@ let coqideincl = "$LABLGTKINCLUDES" let cflags = "$cflags" let best = "$best_compiler" let arch = "$ARCH" +let has_coqide = "$COQIDE" let has_natdynlink = $HASNATDYNLINK let natdynlinkflag = "$NATDYNLINKFLAG" let osdeplibs = "$OSDEPLIBS" diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 432e7ee51..961e85058 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -21,6 +21,17 @@ open Scanf *) +(** F.A.Q about ocamlbuild: + +* P / Px ? + + Same, except that the second can be use to signal the main target + of a rule, in order to get a nicer log (otherwise the full command + is used as target name) + +*) + + (** Generic file reader, which produces a list of strings, one per line *) @@ -52,8 +63,7 @@ let camlp4o = A Coq_config.camlp4o let camlp4incl = S[A"-I"; A Coq_config.camlp4lib] let camlp4compat = Sh Coq_config.camlp4compat let opt = (Coq_config.best = "opt") -let best_oext = if opt then ".native" else ".byte" -let best_ext = if opt then ".opt" else ".byte" +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 @@ -134,11 +144,11 @@ let coqmktop = "scripts/coqmktop" (** The list of binaries to build: (name of link in bin/, name in _build, install both or only best) *) -type links = Both | Best | BestInPlace +type links = Both | Best | BestInPlace | Ide let all_binaries = [ "coqtop", coqtop, Both; - "coqide", coqide, Both; + "coqide", coqide, Ide; "coqmktop", coqmktop, Both; "coqc", "scripts/coqc", Both; "coqchk", "checker/main", Both; @@ -152,6 +162,11 @@ let all_binaries = "csdpcert", "plugins/micromega/csdpcert", BestInPlace; ] + +let best_oext = if opt then ".native" else ".byte" +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 @@ -159,9 +174,12 @@ let coqmktopbest = coqmktop^best_oext let binaries_deps = let rec deps = function | [] -> [] - | (_,bin,kind) :: l -> - if opt && kind=Both then (bin^".native") :: (bin^".byte") :: deps l - else (bin^best_oext) :: deps l + | (_,bin,Ide)::l -> + (if ide = "opt" then [bin^".native"] else []) @ + (if ide <> "no" then [bin^".byte"] else []) @ deps l + | (_,bin,Both)::l when opt -> + (bin^".native") :: (bin^".byte") :: deps l + | (_,bin,_)::l -> (bin^best_oext) :: deps l in deps all_binaries let ln_sf toward f = @@ -169,17 +187,21 @@ let ln_sf toward f = let rec make_bin_links = function | [] -> () - | (b,ob,Both) :: l -> - ln_sf ("../"^ !_build^"/"^ob^".byte") ("bin/"^b^".byte"); - if opt then ln_sf ("../"^ !_build^"/"^ob^".native") ("bin/"^b^".opt"); - ln_sf (b^best_ext) ("bin/"^b); - make_bin_links l - | (b,ob,Best) :: l -> - ln_sf ("../"^ !_build^"/"^ob^best_oext) ("bin/"^b); - make_bin_links l - | (b,ob,BestInPlace) :: l -> - ln_sf (b^best_oext) ob; - make_bin_links l + | (b,ob,kind)::l -> + make_bin_links l; + let obd = "../"^ !_build^"/"^ob and bd = "bin/"^b in + match kind with + | Ide when ide <> "no" -> + ln_sf (obd^".byte") (bd^".byte"); + if ide = "opt" then ln_sf (obd^".native") (bd^".opt"); + ln_sf (b^best_iext) bd + | Ide (* when ide = "no" *) -> () + | Both -> + ln_sf (obd^".byte") (bd^".byte"); + if opt then ln_sf (obd^".native") (bd^".opt"); + ln_sf (b^best_ext) bd + | Best -> ln_sf (obd^best_oext) bd + | BestInPlace -> ln_sf (b^best_oext) ob let incl f = Ocaml_utils.ocaml_include_flags f @@ -223,7 +245,7 @@ let extra_rules () = begin let ml4 = env "%.ml4" and ml = env "%.ml" in Cmd (S[camlp4o;T(tags_of_pathname ml4 ++ "p4mod");readable_flag; T(tags_of_pathname ml4 ++ "p4option"); camlp4compat; - A"-o"; P ml; A"-impl"; P ml4])); + A"-o"; Px ml; A"-impl"; P ml4])); flag ["is_ml4"; "p4mod"; "use_macro"] (A"pa_macro.cmo"); flag ["is_ml4"; "p4mod"; "use_extend"] (A"pa_extend.cmo"); @@ -317,9 +339,9 @@ let extra_rules () = begin let depideo = if is_ide then [ide_cmxa] else [] in let depideb = if is_ide then [ide_cma] else [] 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";P fo]); + (cmd [P coqmktopbest;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";P fb]); + (cmd [P coqmktopbest;A"-boot";A"-top";ideflag;incl fb;A"-o";Px fb]); in mktop_rule coqtop false; mktop_rule coqide true; @@ -332,7 +354,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 coqdepbest;dep_dynlink;A"-slash";P v;Sh">";P vd])); + Cmd (S [P coqdepbest;dep_dynlink;A"-slash";P v;Sh">";Px vd])); (** Coq files compilation *) @@ -354,7 +376,7 @@ let extra_rules () = begin (fun env build -> let f = env (d^"%") in coq_build_dep f build; - Cmd (S [P coqtopbest;A"-boot";bootflag;A"-compile";P f])) + Cmd (S [P coqtopbest;A"-boot";bootflag;A"-compile";Px f])) in coq_v_rule "theories/Init/" true; coq_v_rule "" false; @@ -363,7 +385,7 @@ let extra_rules () = begin 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";P initialcoq]); + A"-l";P makeinitial; A"-outputstate";Px initialcoq]); (** Generation of _plugin_mod.ml files *) @@ -380,7 +402,7 @@ let extra_rules () = begin rule ".cmxa.cmxs" ~prod:"%.cmxs" ~dep:"%.cmxa" (fun env _ -> - let cmxs = P (env "%.cmxs") and cmxa = P (env "%.cmxa") in + let cmxs = Px (env "%.cmxs") and cmxa = P (env "%.cmxa") in if os5fix then Cmd (S [A"../dev/ocamlopt_shared_os5fix.sh"; !Options.ocamlopt; cmxs]) else @@ -389,7 +411,7 @@ let extra_rules () = begin (** Generation of NMake.v from NMake_gen.ml *) rule "NMake" ~prod:nmake ~dep:nmakegen - (cmd [ocaml;P nmakegen;Sh ">";P nmake]); + (cmd [ocaml;P nmakegen;Sh ">";Px nmake]); end @@ -402,12 +424,11 @@ end (** TODO / Remarques: - * On repasse tout en revue sans arret, et c'est long, meme cached: - 1 min 25 pour les 2662 targets en cache. - Peut-on mieux faire ? + * Apres un premier build, le second prend du temps, meme cached: + 1 min 25 pour les 2662 targets en cache. Etonnement, refaire + coqtop.byte ne prend que ~4s, au lieu des ~40s pour coqtop.opt. + A comprendre ... - * coqdep a besoin dans _build des fichiers dont on depend, - mais ils n'y sont pas forcement, d'ou un gros cp au debut. - Y-a-t'il mieux à faire ? + * Parallelisation: vraiment pas top *) -- cgit v1.2.3