ocamlbuild: coqide, coqchk, a bit of .vo

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12019 85f007b7-540e-0410-9357-904b9bb8a0f7

_tags

@@ -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
-

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
+states/initial.coq

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,24 +141,26 @@ 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 *)
 
 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)...
+
+*)

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