diff options
| -rw-r--r-- | _tags | 9 | ||||
| -rw-r--r-- | coq.itarget | 5 | ||||
| -rw-r--r-- | myocamlbuild.ml | 177 | ||||
| -rw-r--r-- | plugins/_tags | 4 |
4 files changed, 141 insertions, 54 deletions
@@ -8,6 +8,11 @@ <tools/coq_tex.{native,byte}> : use_str <tools/coq_makefile.{native,byte}> : use_str <tools/coqdoc/main.{native,byte}> : use_str +<checker/main.{native,byte}> : use_str, use_unix, use_gramlib + +## tags for ide + +<ide/**/*.{ml,mli}>: thread, ide ## tags for camlp4 files @@ -44,9 +49,12 @@ ## sub-directory inclusion +# Note: "checker" is deliberately not included + "config": include "parsing": include "ide": include +"ide/utils": include "interp": include "kernel": include "kernel/byterun": include @@ -63,4 +71,3 @@ "tools": include "tools/coqdoc": include "toplevel": include - diff --git a/coq.itarget b/coq.itarget index 421082a3a..ea48c3339 100644 --- a/coq.itarget +++ b/coq.itarget @@ -1,11 +1,12 @@ bin/coqmktop bin/coqtop +bin/coqide bin/coqc +bin/coqchk bin/coqdep bin/coqwc bin/coq-tex bin/coq_makefile bin/gallina bin/coqdoc -# for the moment: -bin/coqdep_boot
\ No newline at end of file +states/initial.coq diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 17dfcdff1..ecc60c24b 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -70,15 +70,24 @@ let get_env s = (** Configuration *) let _ = Options.ocamlc := A(get_env "OCAMLC") +let _ = Options.ocamlopt := A(get_env "OCAMLOPT") +let _ = Options.ocamlmklib := A(get_env "OCAMLMKLIB") +let _ = Options.ocamldep := A(get_env "OCAMLDEP") +let _ = Options.ocamldoc := A(get_env "OCAMLDOC") +let _ = Options.ocamlopt := A(get_env "OCAMLOPT") +let _ = Options.ocamlyacc := A(get_env "OCAMLYACC") +let _ = Options.ocamllex := A(get_env "OCAMLLEX") let camlp4o = A(get_env "CAMLP4O") -let camlp4lib = S[A"-I"; A(get_env "MYCAMLP4LIB")] +let camlp4incl = S[A"-I"; A(get_env "MYCAMLP4LIB")] let camlp4compat = Sh(get_env "CAMLP4COMPAT") let opt = (get_env "BEST" = "opt") let best_oext = if opt then ".native" else ".byte" let best_ext = if opt then ".opt" else ".byte" let hasdynlink = (get_env "HASNATDYNLINK" = "true") -let flag_dynlink = if hasdynlink then A"-DHasDynLink" else N +let flag_dynlink = if hasdynlink then A"-DHasDynlink" else N +let dep_dynlink = if hasdynlink then N else Sh"-natdynlink no" +let lablgtkincl = Sh(get_env "COQIDEINCLUDES") (** Do we want to inspect .ml generated from .ml4 ? *) let readable_genml = false @@ -97,6 +106,8 @@ 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 ide_cma = "ide/ide.cma" +let ide_cmxa = "ide/ide.cmxa" let ide_mllib = "ide/ide.mllib" let tolink = "scripts/tolink.ml" @@ -118,7 +129,10 @@ let grammar = "parsing/grammar.cma" let qconstr = "parsing/q_constr.cmo" let coqtop = "bin/coqtop" +let coqide = "bin/coqide" let coqmktop = "bin/coqmktop" +let coqc = "bin/coqc" +let coqchk = "bin/coqchk" let coqdep_boot = "bin/coqdep_boot" let coqdep = "bin/coqdep" let coqdoc = "bin/coqdoc" @@ -127,6 +141,9 @@ let coqtex = "bin/coq-tex" let coqmakefile = "bin/coq_makefile" let gallina = "bin/gallina" +let initialcoq = "states/initial.coq" +let init_vo = ["theories/Init/Prelude.vo";"theories/Init/Logic_Type.vo"] +let makeinitial = "states/MakeInitial.v" (** A few common rules *) @@ -134,17 +151,16 @@ let gallina = "bin/gallina" let copy_rule src dst = rule (src^"_"^dst) ~dep:src ~prod:dst (fun _ _ -> cp src dst) -let copy_bin srcd radix = - let src = srcd^radix and dst = "bin/"^radix in +let copy_bin_alias src dst = + let dsto = dst^".opt" and dstb = dst^".byte" in copy_rule (src^".byte") (dst^".byte"); - if opt then copy_rule (src^".native") (dst^".opt") + if opt then copy_rule (src^".native") (dst^".opt"); + rule dst ~prod:dst ~deps:(if opt then [dsto;dstb] else [dstb]) + (fun _ _ -> ln_s ((Filename.basename dst)^best_ext) dst) -let copy_bin_alias srcd radix = - let f = "bin/"^radix in - let fo = f^".opt" and fb = f^".byte" in - let deps = if opt then [fb;fo] else [fb] in - copy_bin srcd radix; - rule f ~deps:deps ~prod:f (fun _ _ -> ln_s (radix^best_ext) f) +let copy_bin_best src dst = copy_rule (src^best_oext) dst + +let incl f = Ocaml_utils.ocaml_include_flags f @@ -160,7 +176,7 @@ let _ = dispatch begin function (** Camlp4 extensions *) - rule "ml4ml" ~dep:"%.ml4" ~prod:"%.ml" + rule ".ml4.ml" ~dep:"%.ml4" ~prod:"%.ml" (fun env _ -> let ml4 = env "%.ml4" and ml = env "%.ml" in Cmd (S[camlp4o;T(tags_of_pathname ml4 ++ "p4mod");readable_flag; @@ -191,15 +207,16 @@ let _ = dispatch begin function 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"; camlp4lib; Ocaml_utils.ocaml_include_flags ml4; - A"-impl"; P ml4])); + A"-DByte";A"-DHasDynlink";camlp4compat;A"-impl"]); + A"-rectypes"; camlp4incl; incl ml4; A"-impl"; P ml4])); -(** All caml files are compiled with -rectypes and +camlp4/5 *) +(** All caml files are compiled with -rectypes and +camlp4/5 + and ide files need +lablgtk2 *) - flag ["compile"; "ocaml"] (S [A"-rectypes"; camlp4lib]); - flag ["link"; "ocaml"] (S [A"-rectypes"; camlp4lib]); + flag ["compile"; "ocaml"] (S [A"-rectypes"; camlp4incl]); + flag ["link"; "ocaml"] (S [A"-rectypes"; camlp4incl]); + flag ["compile"; "ocaml"; "ide"] lablgtkincl; + flag ["link"; "ocaml"; "ide"] lablgtkincl; (** Extra libraries *) @@ -237,7 +254,7 @@ let _ = dispatch begin function rule "tolink.ml" ~deps:(ide_mllib::core_mllib) ~prod:tolink (fun _ _ -> - let cat s = String.concat " " (read_file s) in + let cat s = String.concat " " (string_list_of_file s) in let core_mods = String.concat " " (List.map cat core_mllib) in let ide_mods = cat ide_mllib in let core_cmas = String.concat " " core_cma in @@ -247,46 +264,108 @@ let _ = dispatch begin function "let ide = \""^ide_mods^"\"\n"], tolink)); -(** Coqtop *) - - let coqtopo = coqtop^".opt" and coqtopb = coqtop^".byte" in - let depso = [coqmktop;libcoqrun;coqconfig^".cmx"] @ core_cmxa - and depsb = [coqmktop;libcoqrun;coqconfig^".cmo"] @ core_cma +(** Coqtop and coqide *) + + let rules f is_ide = + let fo = f^".opt" and fb = f^".byte" in + let ideflag = if is_ide then A"-ide" else N in + let depsall = [coqmktop;libcoqrun] in + let depso = (coqconfig^".cmx") :: core_cmxa in + let depsb = (coqconfig^".cmo") :: core_cma in + 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) + (fun _ _ -> Cmd (S [P coqmktop;A"-boot";A"-opt";ideflag; + incl fo;A"-o";P fo])); + rule fb ~prod:fb ~deps:(depsall@depsb@depideb) + (fun _ _ -> Cmd (S [P coqmktop;A"-boot";A"-top";ideflag; + incl fb;A"-o";P fb])); + rule f ~prod:f ~deps:(if opt then [fb;fo] else [fb]) + (fun _ _ -> ln_s ((Filename.basename f)^best_ext) f) in - if opt then rule coqtopo ~prod:coqtopo ~deps:depso - (fun _ _ -> - Cmd (S [P coqmktop;A"-boot";A"-opt"; - Ocaml_utils.ocaml_include_flags coqtopo; A"-o";P coqtopo])); - rule coqtopb ~prod:coqtopb ~deps:depsb - (fun _ _ -> - Cmd (S [P coqmktop;A"-boot";A"-top"; - Ocaml_utils.ocaml_include_flags coqtopb; A"-o";P coqtopb])); - rule coqtop ~prod:coqtop ~deps:(coqtopb :: if opt then [coqtopo] else []) - (fun _ _ -> ln_s ("coqtop"^best_ext) coqtop); + rules coqtop false; + rules coqide true; -(** Coqmktop *) +(** Other binaries *) - copy_bin_alias "scripts/" "coqmktop"; + copy_bin_alias "scripts/coqmktop" coqmktop; + copy_bin_alias "scripts/coqc" coqc; + copy_bin_alias "checker/main" coqchk; + copy_bin_best "tools/coqdep_boot" coqdep_boot; + copy_bin_best "tools/coqdep" coqdep; + copy_bin_best "tools/coqdoc/main" coqdoc; + copy_bin_best "tools/coqwc" coqwc; + copy_bin_best "tools/coq_makefile" coqmakefile; + copy_bin_best "tools/coq_tex" coqtex; + copy_bin_best "tools/gallina" gallina; -(** Coqc *) +(** Coq files dependencies *) + + rule ".v.depends" ~prod:"%.v.depends" ~deps:["%.v";coqdep_boot] + (fun env _ -> + let v = env "%.v" and vd = env "%.v.depends" in + (** All .v files are not necessarily present yet in _build + (could we do something cleaner ?) *) + Cmd (S [Sh "cd .. && "; + P coqdep_boot;dep_dynlink;A"-slash";P v;Sh">"; + P ("_build/"^vd)])); + +(** Coq files compilation *) + + let check_dep_coq vd v vo vg build = + (** NB: this rely on coqdep producing a single Makefile rule + for one .v file *) + match string_list_of_file vd with + | vo'::vg'::v'::deps when vo'=vo && vg'=vg^":" && v'=v -> + let d = List.map (fun a -> [a]) deps in + List.iter Outcome.ignore_good (build d) + | _ -> failwith ("Something wrong with dependencies of "^v) + in - copy_bin_alias "scripts/" "coqc"; + let coq_v_rule d boot = + rule (d^"/.v.vo") ~prods:[d^"%.vo";d^"%.glob"] + ~deps:([d^"%.v";d^"%.v.depends"]@(if boot then [] else [initialcoq])) + (fun env build -> + let v = env (d^"%") and vd = env (d^"%.v.depends") and + vo = env (d^"%.vo") and vg = env (d^"%.glob") in + check_dep_coq vd (v^".v") vo vg build; + let bootflag = if boot then S [A"-boot";A"-nois"] else N in + Cmd (S [P coqtop;Sh "-coqlib .";bootflag; A"-compile";P v])) + in + coq_v_rule "theories/Init/" true; + coq_v_rule "" false; -(** Coqdep *) + rule "initial.coq" ~prod:initialcoq ~deps:(makeinitial :: init_vo) + (fun _ _ -> + Cmd (S [P coqtop;Sh "-coqlib ."; + A"-batch";A"-nois";A"-notop";A"-silent"; + A"-l";P makeinitial; A"-outputstate";P initialcoq])); - copy_rule ("tools/coqdep_boot"^best_oext) coqdep_boot; - copy_rule ("tools/coqdep"^best_oext) coqdep; +(** Generation of _plugin_mod.ml files *) -(** Misc binaries *) + rule "_mod.ml" ~prod:"%_plugin_mod.ml" ~dep:"%_plugin.mllib" + (fun env _ -> + let mods = string_list_of_file (env "%_plugin.mllib") in + let line s = "let _ = Mltop.add_known_module \""^s^"\"\n" in + Echo (List.map line mods, env "%_plugin_mod.ml")); - copy_rule ("tools/coqdoc/main"^best_oext) coqdoc; - copy_rule ("tools/coqwc"^best_oext) coqwc; - copy_rule ("tools/coq_makefile"^best_oext) coqmakefile; - copy_rule ("tools/coq_tex"^best_oext) coqtex; - copy_rule ("tools/gallina"^best_oext) gallina; +(** Rule for native dynlinkable plugins *) -(* TODO: coqide, coqchk *) + rule ".cmxa.cmxs" ~prod:"%.cmxs" ~dep:"%.cmxa" + (fun env _ -> + (* TODO: reuse the fix for MacOS *) + Cmd (S [!Options.ocamlopt;A"-linkall";A"-shared"; + A"-o";P (env "%.cmxs"); P (env "%.cmxa")])); | _ -> () end + +(** TODO: + * pourquoi certains binaires de bin/ se retrouvent parfois + avec une taille a zero ? + * les binaires n'ont pas l'air d'etre refait si on touche un fichier + (p.ex. coqdep_boot.ml) + * on repasse tout en revue sans arret, et c'est long (meme cached)... + +*) diff --git a/plugins/_tags b/plugins/_tags index a8291f6c8..968b25bd2 100644 --- a/plugins/_tags +++ b/plugins/_tags @@ -6,9 +6,9 @@ "interface/centaur.ml4": use_grammar "interface/debug_tac.ml4": use_grammar "quote/g_quote.ml4": use_grammar -"subtac/equations.ml4": use_grammar +"subtac/equations.ml4": use_grammar, use_extend "subtac/g_eterm.ml4": use_grammar -"subtac/g_subtac.ml4": use_grammar +"subtac/g_subtac.ml4": use_grammar, use_extend "rtauto/g_rtauto.ml4": use_grammar "xml/xmlentries.ml4": use_grammar "xml/dumptree.ml4": use_grammar |