ocamlbuild improvements + minor makefile fix

 * a small shell script ./build to drive ocamlbuild
 * rules for all the binaries (apart from coqide and coqchk)
 * use of ocamlbuild's Echo instead of using shell + sed + awk
   for generated files
 * Makefile: remove unused STAGE1_CMO and add bin/coqdep_boot to the
   list of things to "clean"

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

6 files changed, 227 insertions, 110 deletions

diff --git a/Makefile.common b/Makefile.common
index 8a258fb8c..e61a4e28a 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -87,7 +87,7 @@ COQTEX:=bin/coq-tex$(EXE)
 COQWC:=bin/coqwc$(EXE)
 COQDOC:=bin/coqdoc$(EXE)
 
-TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC)
+TOOLS:=$(COQDEP) $(COQDEPBOOT) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC)
 
 ###########################################################################
 # Documentation
@@ -619,7 +619,6 @@ CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
 ## Enumeration of targets that require being done at stage1
 
 STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \
-  $(filter-out parsing/q_constr.cmo,$(STAGE1_CMO)) \
   $(GENFILES) \
   source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \
   $(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o
diff --git a/_tags b/_tags
index 7e8db8dd6..76a7da8a0 100644
--- a/_tags
+++ b/_tags
@@ -2,6 +2,12 @@
 ## tags for binaries
 
 <scripts/coqmktop.{native,byte}> : use_str, use_unix, use_gramlib
+<scripts/coqc.{native,byte}> : use_unix, use_gramlib
+<tools/coqdep_boot.{native,byte}> : use_unix
+<tools/coqdep.{native,byte}> : use_unix, use_gramlib
+<tools/coq_tex.{native,byte}> : use_str
+<tools/coq_makefile.{native,byte}> : use_str
+<tools/coqdoc/main.{native,byte}> : use_str
 
 ## tags for camlp4 files 
 
@@ -55,5 +61,6 @@
 "tactics": include
 "theories": include
 "tools": include
+"tools/coqdoc": include
 "toplevel": include
 
diff --git a/build b/build
new file mode 100755
index 000000000..4552d5a43
--- /dev/null
+++ b/build
@@ -0,0 +1,26 @@
+#!/bin/sh
+
+FLAGS=
+OCAMLBUILD=ocamlbuild
+
+ocb()
+{
+  $OCAMLBUILD $FLAGS $*
+}
+
+rule() {
+  case $1 in
+    clean)  ocb -clean && rm -rf bin/*;;
+    all)    ocb coq.otarget;;
+    *)      ocb $1;;
+  esac;
+}
+
+if [ $# -eq 0 ]; then
+  rule all
+else
+  while [ $# -gt 0 ]; do
+    rule $1;
+    shift
+  done
+fi
diff --git a/coq.itarget b/coq.itarget
index 4845e1cdc..421082a3a 100644
--- a/coq.itarget
+++ b/coq.itarget
@@ -1,5 +1,11 @@
-bin/.foo
-scripts/coqmktop.byte
-scripts/coqmktop.native
-bin/coqtop.opt
-bin/coqtop.byte
\ No newline at end of file
+bin/coqmktop
+bin/coqtop
+bin/coqc
+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
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
index 8a45e9739..e224a1080 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -11,6 +11,10 @@
 #ifndef _COQ_INSTRUCT_
 #define _COQ_INSTRUCT_
 
+/* Nota: this list of instructions is parsed to produce derived files */
+/* coq_jumptbl.h and copcodes.ml. Instructions should be uppercase    */
+/* and alone on lines starting by two spaces.                         */
+
 enum instructions {
   ACC0, ACC1, ACC2, ACC3, ACC4, ACC5, ACC6, ACC7, ACC,
   PUSH, 
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index b518c50d0..17dfcdff1 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -3,6 +3,7 @@
 open Ocamlbuild_plugin
 open Ocamlbuild_pack
 open Printf
+open Scanf
 
 (** WARNING !! this is preliminary stuff, able only to build
     coqtop.opt and coqtop.byte, and only in a precise environment
@@ -11,48 +12,50 @@ open Printf
     Support for other rules and other configurations will be
     added later...
 
-    Usage: 
-
-    ocamlbuild coq.otarget
+    Usage: ./build   (which launches ocamlbuild coq.itarget)
 
     Then you can (hopefully) launch coq (with no input state) via:
     
-    _build/bin/coqtop.opt -nois -coqlib .
+    bin/coqtop.opt -nois -coqlib .
 
     or
 
-    CAML_LD_LIBRARY_PATH=_build/kernel/byterun _build/bin/coqtop.byte -nois -coqlib .
+    export CAML_LD_LIBRARY_PATH=_build/kernel/byterun 
+    bin/coqtop.byte -nois -coqlib .
+
+    Apart from binaries in bin/, every created files are in _build.
+    A "./build clean" should give you back a clean source tree
  
     TODO: understand how to create the right symlinks towards _build ...
 
 *)
 
+(** Generic file reader, which produces a list of strings, one per line *)
 
+let read_file f =
+  let ic = open_in f in
+  let lines = ref [] in
+  begin try
+    while true do lines := (input_line ic)::!lines done
+  with End_of_file -> () end;
+  close_in ic;
+  List.rev !lines
 
-(** Parse a config file such as config/Makefile: 
-    valid lines are NAME=value, comments start by # *)
+(** Parse a config file such as config/Makefile. Valid lines are VAR=def.
+    If def is double-quoted we remove the "..." (first sscanf attempt with %S).
+    Otherwise, def is as long as possible (%s@\n prevents stopping at ' ').
+*)
 
 let read_env f =
-  let ic = open_in f in
-  let vars = ref [] in
-  begin try while true do
-    let l = input_line ic in
-    if l <> "" && l.[0] <> '#' && l.[0] <> ' ' then
-      try
-	let i = String.index l '=' in
-	let var = String.sub l 0 i
-	and def = if i+1 >= String.length l then "" else
-	  String.sub l (i+1) (String.length l - i - 1)
-	in
-	let def = if String.length def >= 2 &&
-	  def.[0]='\"' && def.[String.length def - 1] = '\"'
-	then String.sub def 1 (String.length def - 2) else def
-	in
-	vars:=(var,def)::!vars
-      with Not_found -> ()
-  done with End_of_file -> () end;
-  close_in ic;
-  !vars
+  let lines = read_file f in
+  let add, get = let l = ref [] in (fun x -> l:= x::!l), (fun () -> !l) in
+  let get_var_def s =
+    try sscanf s "%[A-Z0-9_]=%S" (fun v d -> add (v,d))
+    with _ ->
+      try sscanf s "%[A-Z0-9_]=%s@\n" (fun v d -> add (v,d))
+      with _ -> ()
+  in
+  List.iter get_var_def lines; get ()
 
 let env_vars =
   let f = "config/Makefile" in
@@ -63,20 +66,28 @@ let get_env s =
   with Not_found -> (eprintf "Unknown environment variable %s\n" s; exit 1)
 
 
+
 (** Configuration *)
 
 let _ = Options.ocamlc := A(get_env "OCAMLC")
 
-let camlp4o = get_env "CAMLP4O"
-let camlp4lib = get_env "MYCAMLP4LIB"
-let camlp4compat = get_env "CAMLP4COMPAT"
+let camlp4o = A(get_env "CAMLP4O")
+let camlp4lib = 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 "-DHasDynLink" else ""
+let flag_dynlink = if hasdynlink then A"-DHasDynLink" else N
 
 (** Do we want to inspect .ml generated from .ml4 ? *)
 let readable_genml = false
 let readable_flag = if readable_genml then A"pr_o.cmo" else N
 
+
+
+(** Abbreviations about files *)
+
 let core_libs =
   ["lib/lib"; "kernel/kernel"; "library/library";
    "pretyping/pretyping"; "interp/interp";  "proofs/proofs";
@@ -86,31 +97,88 @@ 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_mllib = "ide/ide.mllib"
+
+let tolink = "scripts/tolink.ml"
+let coqconfig = "config/coq_config"
+
+let c_headers_base =
+  ["coq_fix_code.h";"coq_instruct.h"; "coq_memory.h"; "int64_emul.h";
+   "coq_gc.h"; "coq_interp.h"; "coq_values.h"; "int64_native.h";
+   "coq_jumptbl.h"]
+let c_headers = List.map ((^) "kernel/byterun/") c_headers_base
+
+let coqinstrs = "kernel/byterun/coq_instruct.h"
+let coqjumps = "kernel/byterun/coq_jumptbl.h"
+let copcodes = "kernel/copcodes.ml"
+
+let libcoqrun = "kernel/byterun/libcoqrun.a"
+
+let grammar = "parsing/grammar.cma"
+let qconstr = "parsing/q_constr.cmo"
+
+let coqtop = "bin/coqtop"
+let coqmktop = "bin/coqmktop"
+let coqdep_boot = "bin/coqdep_boot"
+let coqdep = "bin/coqdep"
+let coqdoc = "bin/coqdoc"
+let coqwc = "bin/coqwc"
+let coqtex = "bin/coq-tex"
+let coqmakefile = "bin/coq_makefile"
+let gallina = "bin/gallina"
+
+
+
+(** 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
+  copy_rule (src^".byte") (dst^".byte");
+  if opt then copy_rule (src^".native") (dst^".opt")
+
+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)
+
+
+
+(** The real game ... *)
 
 let _ = dispatch begin function
  | After_rules ->  (* Add our rules after the standard ones. *)
 
+(** The _build/bin directory isn't done by default *)
+
+     if not (Sys.file_exists "_build/bin") then
+       Command.execute ~quiet:true (ln_s "../bin" "_build");
+
 (** Camlp4 extensions *)
 
      rule "ml4ml" ~dep:"%.ml4" ~prod:"%.ml"
        (fun env _ ->
 	  let ml4 = env "%.ml4" and ml = env "%.ml" in
-	  Cmd (S[A camlp4o;T(tags_of_pathname ml4 ++ "p4mod");readable_flag;
-		 T(tags_of_pathname ml4 ++ "p4option");
-		 Sh camlp4compat; A"-o"; P ml; A"-impl"; P ml4]));
+	  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]));
 
      flag ["is_ml4"; "p4mod"; "use_macro"] (A"pa_macro.cmo");
      flag ["is_ml4"; "p4mod"; "use_extend"] (A"pa_extend.cmo");
      flag ["is_ml4"; "p4mod"; "use_MLast"] (A"q_MLast.cmo");
 
-     flag_and_dep ["is_ml4"; "p4mod"; "use_grammar"] (P"parsing/grammar.cma");
-     flag_and_dep ["is_ml4"; "p4mod"; "use_constr"] (P"parsing/q_constr.cmo");
+     flag_and_dep ["is_ml4"; "p4mod"; "use_grammar"] (P grammar);
+     flag_and_dep ["is_ml4"; "p4mod"; "use_constr"] (P qconstr);
 
 (** 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"] (A flag_dynlink);
+     flag ["is_mltop"; "p4option"] flag_dynlink;
 
 (*TODO: this is rather ugly for a simple file, we should try to
         benefit more from predefined rules *)
@@ -121,19 +189,17 @@ let _ = dispatch begin function
      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"-rectypes"; A"-I"; A camlp4lib;
-		  A"-pp";
-		  Quote (S [A camlp4o; T(tags_of_pathname ml4 ++ "p4mod");
-			    A"-DByte"; A"-DHasDynLink"; Sh camlp4compat;
+	  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"-I"; A camlp4lib;
-		  Ocaml_utils.ocaml_include_flags ml4;
+		  A"-rectypes"; camlp4lib; Ocaml_utils.ocaml_include_flags ml4;
 		  A"-impl"; P ml4]));
 
-(** All caml files are compiled with -rectypes and +camlp5 *)
+(** All caml files are compiled with -rectypes and +camlp4/5 *)
 
-     flag ["compile"; "ocaml"] (S [A"-rectypes"; A"-I"; A camlp4lib]);
-     flag ["link"; "ocaml"] (S [A"-rectypes"; A"-I"; A camlp4lib]);
+     flag ["compile"; "ocaml"] (S [A"-rectypes"; camlp4lib]);
+     flag ["link"; "ocaml"] (S [A"-rectypes"; camlp4lib]);
 
 (** Extra libraries *)
 
@@ -141,76 +207,85 @@ let _ = dispatch begin function
 
 (** C code for the VM *)
 
-     let headers = List.map (fun s -> "kernel/byterun/"^s)
-       ["coq_fix_code.h";"coq_instruct.h"; "coq_memory.h"; "int64_emul.h";
-	"coq_gc.h"; "coq_interp.h"; "coq_values.h"; "int64_native.h";
-	"coq_jumptbl.h"]
-     in
-     dep ["compile"; "c"] headers;
+     dep ["compile"; "c"] c_headers;
      flag ["compile"; "c"] (S[A"-ccopt";A"-fno-defer-pop -Wall -Wno-unused"]);
-     dep ["link"; "ocaml"; "use_libcoqrun"] ["kernel/byterun/libcoqrun.a"];
-
-(** Generation of coq_jumbtbl.h for the VM *)
+     dep ["link"; "ocaml"; "use_libcoqrun"] [libcoqrun];
 
-     let coqjump = "kernel/byterun/coq_jumptbl.h"
-     and coqinstr = "kernel/byterun/coq_instruct.h" in
-     let cmd = Printf.sprintf
-       "sed -n -e '/^  /s/ \\([A-Z]\\)/ \\&\\&coq_lbl_\\1/gp' -e '/^}/q' %s > %s"
-       coqinstr coqjump
-     in
-     rule "coqjump" ~deps:[coqinstr] ~prod:coqjump
-       (fun _ _ -> Cmd (Sh cmd));
+(** VM: Generation of coq_jumbtbl.h and copcodes.ml from coq_instruct.h *)
 
-(** Generation of opcodes for the VM *)
-
-     let copcodes = "kernel/copcodes.ml"
-     and coqinstr = "kernel/byterun/coq_instruct.h"
-     and script = "kernel/make-opcodes" in
-     let cmd = Printf.sprintf
-       "sed -n -e '/^enum/p' -e 's/,//g' -e '/^  /p' %s | awk -f %s > %s"
-       coqinstr script copcodes
-     in
-     rule "copcodes" ~deps:[coqinstr;script] ~prod:copcodes
-       (fun _ _ -> Cmd (Sh cmd));
+     rule "coqinstrs" ~dep:coqinstrs ~prods:[coqjumps;copcodes]
+       (fun _ _ ->
+	  let jmps = ref [] and ops = ref [] and i = ref 0 in
+	  let add_instr instr comma =
+	    if instr = "" then failwith "Empty" else begin
+	      jmps:=sprintf "&&coq_lbl_%s%s \n" instr comma :: !jmps;
+	      ops:=sprintf "let op%s = %d\n" instr !i :: !ops;
+	      incr i
+	    end
+	  in
+	  (** we recognize comma-separated uppercase instruction names *)
+	  let parse_line s =
+	    let b = Scanning.from_string s in
+	    try while true do bscanf b " %[A-Z0-9_]%[,]" add_instr done
+	    with _ -> ()
+	  in
+	  List.iter parse_line (read_file coqinstrs);
+	  Seq [Echo (List.rev !jmps, coqjumps);
+	       Echo (List.rev !ops, copcodes)]);
 
 (** Generation of tolink.ml *)
 
-     let tolink = "scripts/tolink.ml" in
-     let core_cma_s = String.concat " " core_cma in
-     let core_mllib_s = String.concat " " core_mllib in
-     let cmd =
-       "(echo \'let copts = \"-cclib -lcoqrun\"\'; "^
-       "echo \'let core_libs = \"config/coq_config.cmo "^core_cma_s^"\"\'; "^
-       "echo \'let core_objs = \"Coq_config `cat "^core_mllib_s^"`\"\'; "^
-       "echo \'let ide = \"`cat ide/ide.mllib`\"\' " ^
-       ") > " ^ tolink
-     in
-     rule "tolink.ml" ~deps:core_mllib ~prod:tolink
-       (fun _ _ -> Cmd (Sh cmd));
+     rule "tolink.ml" ~deps:(ide_mllib::core_mllib) ~prod:tolink
+       (fun _ _ ->
+	  let cat s = String.concat " " (read_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
+	  Echo (["let copts = \"-cclib -lcoqrun\"\n";
+		 "let core_libs = \""^coqconfig^".cmo "^core_cmas^"\"\n";
+		 "let core_objs = \"Coq_config "^core_mods^"\"\n";
+		 "let ide = \""^ide_mods^"\"\n"],
+		tolink));
 
 (** Coqtop *)
 
-     let coqtopopt = "bin/coqtop.opt"
-     and coqtopbyte = "bin/coqtop.byte" in
-     let deps = ["scripts/coqmktop.native";"kernel/byterun/libcoqrun.a"] in
-     let depsopt = [ "config/coq_config.cmx"] @ deps @ core_cmxa
-     and depsbyte = [ "config/coq_config.cmo"] @ deps @ core_cma
-     in begin
-     rule "coqtop.opt" ~deps:depsopt ~prod:coqtopopt
+     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
+     in
+     if opt then rule coqtopo ~prod:coqtopo ~deps:depso
        (fun _ _ ->
-	  Cmd (S [P "scripts/coqmktop.native";A"-boot";A"-opt";
-		  Ocaml_utils.ocaml_include_flags coqtopopt;
-		  A"-o";P coqtopopt]));
-     rule "coqtop.byte" ~deps:depsbyte ~prod:coqtopbyte
+	  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 "scripts/coqmktop.native";A"-boot";A"-top";
-		  Ocaml_utils.ocaml_include_flags coqtopbyte;
-		  A"-o";P coqtopbyte]));
-     end;
+	  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);
+
+(** Coqmktop *)
+
+     copy_bin_alias "scripts/" "coqmktop";
+
+(** Coqc *)
+
+     copy_bin_alias "scripts/" "coqc";
+
+(** Coqdep *)
+
+     copy_rule ("tools/coqdep_boot"^best_oext) coqdep_boot;
+     copy_rule ("tools/coqdep"^best_oext) coqdep;
+
+(** Misc binaries *)
 
-(** bin : directory bin doesn't get made by default ??!! *)
+     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 "bin dir" ~prod:"bin/.foo" (fun _ _ -> Cmd (Sh "mkdir -p bin && touch bin/.foo"));
+(* TODO: coqide, coqchk *)
 
  | _ -> ()