ocamlbuild: many improvements (macos 10.5 fix, correct dllpath, etc)

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

6 files changed, 249 insertions, 232 deletions

diff --git a/Makefile.build b/Makefile.build
index 16e7cdaa43..36fdbfdb0f 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -836,24 +836,10 @@ endif
 
 %.cmxs: %.cmxa
 	$(SHOW)'OCAMLOPT -shared -o $@'
-ifneq ($(HASNATDYNLINK),os5fixme)
-	$(HIDE)$(OCAMLOPT) -linkall -shared -o $@ $<
+ifeq ($(HASNATDYNLINK),os5fixme)
+	$(HIDE)dev/ocamlopt_shared_os5fix.sh $(OCAMLOPT) $@ $<
 else
-	$(HIDE)$(OCAMLOPT) -dstartup -linkall -shared -o $@ $<
-#	Fix1: add a dummy instruction before the caml generic functions
-#	Fix2: make all caml generic functions private
-	$(HIDE)rm -f $@ $@.startup.fixed.s
-	$(HIDE)cat $@.startup.s | sed \
-	  -e "s/_caml_shared_startup__code_begin:/_caml_shared_startup__code_begin:	ret/" \
-	  -e "s/.globl	_caml_curry/.private_extern	_caml_curry/" \
-	  -e "s/.globl	_caml_apply/.private_extern	_caml_apply/" \
-	  -e "s/.globl	_caml_tuplify/.private_extern	_caml_tuplify/" \
-	  > $@.startup.fixed.s
-#	Recompile fixed startup code
-	$(HIDE)as -o $@.startup.o $@.startup.fixed.s
-#	Build fixed .cmxs (assume plugins are on directory base and include all files)
-	$(HIDE)ld -bundle -flat_namespace -undefined warning -read_only_relocs suppress -o $@ `dirname $@`/*.o
-	$(HIDE)rm $@.startup.o $@.startup.s $@.startup.fixed.s
+	$(HIDE)$(OCAMLOPT) -linkall -shared -o $@ $<
 endif
 
 %.cmxs: %.cmx
diff --git a/_tags b/_tags
index 78380f18c5..df9ad10fc6 100644
--- a/_tags
+++ b/_tags
@@ -50,8 +50,8 @@
 ## sub-directory inclusion
 
 # Note: "checker" is deliberately not included
+# Note: same for "config" (we create a special coq_config.ml)
 
-"config": include
 "parsing": include
 "ide": include
 "ide/utils": include
diff --git a/bin.itarget b/bin.itarget
deleted file mode 100644
index a4110bc958..0000000000
--- a/bin.itarget
+++ /dev/null
@@ -1,11 +0,0 @@
-bin/coqmktop
-bin/coqtop
-bin/coqide
-bin/coqc
-bin/coqchk
-bin/coqdep
-bin/coqwc
-bin/coq-tex
-bin/coq_makefile
-bin/gallina
-bin/coqdoc
diff --git a/coq.itarget b/coq.itarget
index 6ab8e46700..72684c23b3 100644
--- a/coq.itarget
+++ b/coq.itarget
@@ -1,2 +1,2 @@
-bin.otarget
+binaries
 vo.otarget
diff --git a/dev/ocamlopt_shared_os5fix.sh b/dev/ocamlopt_shared_os5fix.sh
new file mode 100755
index 0000000000..db4cb159c4
--- /dev/null
+++ b/dev/ocamlopt_shared_os5fix.sh
@@ -0,0 +1,23 @@
+#/bin/sh
+
+### Temporary fix for production of .cmxs on MacOS 10.5
+
+OCAMLOPT=$1
+CMXS=$2
+CMXA=$3
+
+$OCAMLOPT -dstartup -linkall -shared -o $CMXS $CMXA
+# Fix1: add a dummy instruction before the caml generic functions
+# Fix2: make all caml generic functions private
+rm -f $CMXS $CMXS.startup.fixed.s
+cat $CMXS.startup.s | sed \
+ -e "s/_caml_shared_startup__code_begin:/_caml_shared_startup__code_begin:	ret/" \
+ -e "s/.globl	_caml_curry/.private_extern	_caml_curry/" \
+ -e "s/.globl	_caml_apply/.private_extern	_caml_apply/" \
+ -e "s/.globl	_caml_tuplify/.private_extern	_caml_tuplify/" \
+ > $CMXS.startup.fixed.s
+# Recompile fixed startup code
+as -o $CMXS.startup.o $CMXS.startup.fixed.s
+# Build fixed .cmxs (assume plugins are on directory base and include all files)
+ld -bundle -flat_namespace -undefined warning -read_only_relocs suppress -o $CMXS `dirname $CMXS`/*.o
+rm $CMXS.startup.o $CMXS.startup.s $CMXS.startup.fixed.s
\ No newline at end of file
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 3ad543302f..b38c175bbf 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -9,23 +9,14 @@ open Scanf
     build coq and its libraries if everything goes right.
     Support for all the build rules and configuration options
     is progressively added. Tested only on linux + ocaml 3.11 +
-    natdynlink for now.
+    local + natdynlink for now.
 
     Usage: 
      ./configure -local -opt
-     manual addition of /_build to coqlib and coqsrc in config/coq_config.ml
      ./build   (which launches ocamlbuild coq.otarget)
 
-    Then you can (hopefully) launch coq via:
-    
-    _build/bin/coqtop.opt
-
-    or
-
-    export CAML_LD_LIBRARY_PATH=_build/kernel/byterun 
-    _build/bin/coqtop.byte -nois
-
-    Every created files are in _build.
+    Then you can (hopefully) launch bin/coqtop, bin/coqide and so on.
+    Apart from the links in bin, every created files are in _build.
     A "./build clean" should give you back a clean source tree
 
 *)
@@ -85,10 +76,13 @@ 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 hasdynlink = (get_env "HASNATDYNLINK" <> "false")
+let os5fix = (get_env "HASNATDYNLINK" = "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(get_env "COQIDEINCLUDES")
+let local = (get_env "LOCAL" = "true")
+let coqsrc = get_env "COQSRC"
 
 (** Do we want to inspect .ml generated from .ml4 ? *)
 let readable_genml = false
@@ -113,7 +107,6 @@ let ide_cmxa = "ide/ide.cmxa"
 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";
@@ -130,19 +123,6 @@ let libcoqrun = "kernel/byterun/libcoqrun.a"
 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"
-let coqwc = "bin/coqwc"
-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"
@@ -152,241 +132,280 @@ let nmakegen = "theories/Numbers/Natural/BigN/NMake_gen.ml"
 
 let genvfiles = [nmake]
 
-(** A few common functions *)
-
-let copy_rule src dst =
-  rule (src^"_"^dst) ~dep:src ~prod:dst (fun _ _ -> cp src dst)
-
-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");
-  rule dst ~prod:dst ~deps:(if opt then [dsto;dstb] else [dstb])
-    (fun _ _ -> ln_s ((Filename.basename dst)^best_ext) dst)
-
-let copy_bin_best src dst = copy_rule (src^best_oext) dst
+let coqtop = "toplevel/coqtop"
+let coqide = "ide/coqide"
+let coqdepboot = "tools/coqdep_boot"
+let coqmktop = "scripts/coqmktop"
+
+(** The list of binaries to build:
+    (name of link in bin/, name in _build, install both or only best) *)
+
+let all_binaries =
+ [ "coqtop", coqtop, true;
+   "coqide", coqide, true;
+   "coqmktop", coqmktop, true;
+   "coqc", "scripts/coqc", true;
+   "coqchk", "checker/main", true;
+   "coqdep_boot", coqdepboot, false;
+   "coqdep", "tools/coqdep", false;
+   "coqdoc", "tools/coqdoc/main", false;
+   "coqwc", "tools/coqwc", false;
+   "coq_makefile", "tools/coq_makefile", false;
+   "coq-tex", "tools/coq_tex", false;
+   "gallina", "tools/gallina", false;
+ ]
+
+let coqtopbest = coqtop^best_oext
+let coqdepbest = coqdepboot^best_oext
+let coqmktopbest = coqmktop^best_oext
+
+let binaries_deps =
+  let rec deps = function
+    | [] -> []
+    | (_,bin,both) :: l ->
+	if opt && both then (bin^".native") :: (bin^".byte") :: deps l
+	else (bin^best_oext) :: deps l
+  in deps all_binaries
+
+let ln_sf toward f =
+  Command.execute ~quiet:true (Cmd (S [A"ln";A"-sf";P toward;P f]))
+
+let rec make_bin_links = function
+  | [] -> ()
+  | (b,ob,true) :: 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,false) :: l ->
+      ln_sf ("../"^ !_build^"/"^ob^best_oext) ("bin/"^b);
+      make_bin_links l
 
 let incl f = Ocaml_utils.ocaml_include_flags f
 
-(** The real game ... *)
-
-let _ = dispatch begin function
- | After_rules ->  (* Add our rules after the standard ones. *)
+let cmd cl = (fun _ _ -> (Cmd (S cl)))
+
+let initial_actions () = begin
+  make_bin_links all_binaries;
+  (** We "pre-create" a few subdirs in _build to please coqtop *)
+  Shell.mkdir_p (!_build^"/dev");
+  (** Moreover, we "pre-import" in _build the sources file that will be needed
+      by coqdep_boot *)
+  (*TODO: do something nicer than this call to find (maybe with Slurp) *)
+  let exclude = "-name _\\$* -or -name .\\* -prune -or" in
+  Command.execute ~quiet:true (Cmd (Sh
+   ("for i in `find theories plugins "^exclude^" -print`; do "^
+    "[ -f $i -a ! -f _build/$i ] && mkdir -p _build/`dirname $i` && cp $i _build/$i; "^
+    "done; true")))
+end
 
-(** We "pre-create" a few subdirs in _build to please coqtop *)
+let extra_rules () = begin
 
-     Shell.mkdir_p (!_build^"/bin");
-     Shell.mkdir_p (!_build^"/dev");
+(** Virtual target for building all binaries *)
 
-(** Moreover, we "pre-import" in _build the sources file that will be needed
-    by coqdep_boot *)
+  rule "binaries" ~stamp:"binaries" ~deps:binaries_deps (fun _ _ -> Nop);
 
-     (*TODO: do something nicer than this call to find (maybe with Slurp) *)
+(** We create a special coq_config which mentions _build *)
 
-     let exclude = "-name _\\$* -or -name .\\* -prune -or" in
-     Command.execute ~quiet:true (Cmd (Sh
-       ("for i in `find theories plugins "^exclude^" -print`; do "^
-	"[ -f $i -a ! -f _build/$i ] && mkdir -p _build/`dirname $i` && cp $i _build/$i; "^
-	"done; true")));
+  rule "coq_config.ml" ~prod:"coq_config.ml" ~dep:"config/coq_config.ml"
+    (fun _ _ ->
+       let lines = read_file "config/coq_config.ml" in
+       let lines = List.map (fun s -> s^"\n") lines in
+       let srcbuild = Filename.concat coqsrc !_build in
+       let line0 = "\n(* Adapted variables for ocamlbuild *)\n" in
+       let line1 = "let coqsrc = \""^srcbuild^"\"\n" in
+       let line2 = "let coqlib = \""^srcbuild^"\"\n" in
+       (* TODO : line3 isn't completely accurate with respect to ./configure:
+	  the case of -local -coqrunbyteflags foo isn't supported *)
+       let line3 =
+	 "let coqrunbyteflags = \"-dllib -lcoqrun -dllpath '"
+	 ^srcbuild^"/kernel/byterun'\"\n"
+       in
+       Echo (lines @ [line0;line1] @ (if local then [line2;line3] else []),
+	     "coq_config.ml"));
 
 (** Camlp4 extensions *)
 
-     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;
-		 T(tags_of_pathname ml4 ++ "p4option"); camlp4compat;
-		 A"-o"; P ml; A"-impl"; P ml4]));
+  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;
+	      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 ["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 grammar);
-     flag_and_dep ["is_ml4"; "p4mod"; "use_constr"] (P qconstr);
+  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"] 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 *)
-     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"; camlp4incl; incl ml4; A"-impl"; P ml4]));
+  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"; camlp4incl; incl ml4; A"-impl"; P ml4]));
 
 (** All caml files are compiled with -rectypes and +camlp4/5 
     and ide files need +lablgtk2 *)
 
-     flag ["compile"; "ocaml"] (S [A"-rectypes"; camlp4incl]);
-     flag ["link"; "ocaml"] (S [A"-rectypes"; camlp4incl]);
-     flag ["compile"; "ocaml"; "ide"] lablgtkincl;
-     flag ["link"; "ocaml"; "ide"] lablgtkincl;
+  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 *)
 
-     ocaml_lib ~extern:true "gramlib";
+  ocaml_lib ~extern:true "gramlib";
 
 (** C code for the VM *)
 
-     dep ["compile"; "c"] c_headers;
-     flag ["compile"; "c"] (S[A"-ccopt";A"-fno-defer-pop -Wall -Wno-unused"]);
-     dep ["link"; "ocaml"; "use_libcoqrun"] [libcoqrun];
+  dep ["compile"; "c"] c_headers;
+  flag ["compile"; "c"] (S[A"-ccopt";A"-fno-defer-pop -Wall -Wno-unused"]);
+  dep ["link"; "ocaml"; "use_libcoqrun"] [libcoqrun];
 
 (** VM: Generation of coq_jumbtbl.h and copcodes.ml from coq_instruct.h *)
 
-     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)]);
+  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 *)
 
-     rule "tolink.ml" ~deps:(ide_mllib::core_mllib) ~prod:tolink
-       (fun _ _ ->
-	  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
-	  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));
+  rule tolink ~deps:(ide_mllib::core_mllib) ~prod:tolink
+    (fun _ _ ->
+       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
+       Echo (["let copts = \"-cclib -lcoqrun\"\n";
+	      "let core_libs = \"coq_config.cmo "^core_cmas^"\"\n";
+	      "let core_objs = \"Coq_config "^core_mods^"\"\n";
+	      "let ide = \""^ide_mods^"\"\n"],
+	     tolink));
 
 (** 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
-     rules coqtop false;
-     rules coqide true;
-
-(** Other binaries *)
-
-     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;
+  let mktop_rule f is_ide =
+    let fo = f^".native" and fb = f^".byte" in
+    let ideflag = if is_ide then A"-ide" else N in
+    let depsall = [coqmktopbest;libcoqrun] in
+    let depso = "coq_config.cmx" :: core_cmxa in
+    let depsb = "coq_config.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) ~insert:`top
+      (cmd [P coqmktopbest;A"-boot";A"-opt";ideflag;incl fo;A"-o";P 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]);
+  in
+  mktop_rule coqtop false;
+  mktop_rule coqide true;
 
 (** Coq files dependencies *)
 
-     rule ".v.d" ~prod:"%.v.depends" ~deps:(["%.v";coqdep_boot]@genvfiles)
-       (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">";P vd]));
+  rule ".v.d" ~prod:"%.v.depends" ~deps:(["%.v";coqdepbest]@genvfiles)
+    (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]));
 
 (** Coq files compilation *)
 
-     let coq_build_dep f build =
-       (** NB: this relies on coqdep producing a single Makefile line
-	   for one .v file, with some specific shape : *)
-       match string_list_of_file (f^".v.depends") with
-	 | vo::vg::v::deps when vo=f^".vo" && vg=f^".glob:" && v=f^".v" ->
-	     let d = List.map (fun x -> [x]) deps in
-	     List.iter Outcome.ignore_good (build d)
-	 | _ -> failwith ("Something wrong with dependencies of "^f^".v")
-     in
-
-     let coq_v_rule d init =
-       let bootflag = if init then A"-nois" else N in
-       let gendeps = if init then [coqtop] else [coqtop;initialcoq] in
-       rule (d^".v.vo")
-	 ~prods:[d^"%.vo";d^"%.glob"] ~deps:([d^"%.v";d^"%.v.depends"]@gendeps)
-	 (fun env build ->
-	    let f = env (d^"%") in
-	    coq_build_dep f build;
-	    Cmd (S [P coqtop;A"-boot";bootflag;A"-compile";P f]))
-     in
-     coq_v_rule "theories/Init/" true;
-     coq_v_rule "" false;
-
-     rule "initial.coq" ~prod:initialcoq ~deps:(makeinitial :: init_vo)
-       (fun _ _ ->
-	  Cmd (S [P coqtop;A"-boot";A"-batch";A"-nois";A"-notop";A"-silent";
-		  A"-l";P makeinitial; A"-outputstate";P initialcoq]));
+  let coq_build_dep f build =
+    (** NB: this relies on coqdep producing a single Makefile line
+	for one .v file, with some specific shape : *)
+    match string_list_of_file (f^".v.depends") with
+      | vo::vg::v::deps when vo=f^".vo" && vg=f^".glob:" && v=f^".v" ->
+	  let d = List.map (fun x -> [x]) deps in
+	  List.iter Outcome.ignore_good (build d)
+      | _ -> failwith ("Something wrong with dependencies of "^f^".v")
+  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
+    rule (d^".v.vo")
+      ~prods:[d^"%.vo";d^"%.glob"] ~deps:[gendep;d^"%.v";d^"%.v.depends"]
+      (fun env build ->
+	 let f = env (d^"%") in
+	 coq_build_dep f build;
+	 Cmd (S [P coqtopbest;A"-boot";bootflag;A"-compile";P f]))
+  in
+  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";P initialcoq]);
 
 (** Generation of _plugin_mod.ml files *)
 
-     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"));
+  rule "_mod.ml" ~prod:"%_plugin_mod.ml" ~dep:"%_plugin.mllib"
+    (fun env _ ->
+       let line s = "let _ = Mltop.add_known_module \""^s^"\"\n" in
+       let mods =
+	 string_list_of_file (env "%_plugin.mllib") @
+	   [Filename.basename (env "%_plugin")]
+       in
+       Echo (List.map line mods, env "%_plugin_mod.ml"));
 
 (** Rule for native dynlinkable plugins *)
 
-     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")]));
+  rule ".cmxa.cmxs" ~prod:"%.cmxs" ~dep:"%.cmxa"
+    (fun env _ ->
+       let prog = if os5fix then
+	 [A"../dev/ocamlopt_shared_os5fix.sh"; !Options.ocamlopt]
+       else [!Options.ocamlopt;A"-linkall";A"-shared";A"-o"]
+       in Cmd (S (prog@[P (env "%.cmxs"); P (env "%.cmxa")])));
 
 (** Generation of NMake.v from NMake_gen.ml *)
 
-     rule "NMake" ~prod:nmake ~dep:nmakegen
-       (fun _ _ -> Cmd (S [ocaml;P nmakegen;Sh ">";P nmake]));
-
- | _ -> ()
+  rule "NMake" ~prod:nmake ~dep:nmakegen
+    (cmd [ocaml;P nmakegen;Sh ">";P nmake]);
 
 end
 
-(** TODO / Remarques:
+(** Registration of our rules (after the standard ones) *)
 
-    * L'idée initiale de partager bin/ et _build/bin/ a coup de symlink
-      etait une anerie : ocamlbuild prenait bin/foo comme _source_
-      et le copiait dans _build/bin/ (par dessus foo), ce qui donnait un
-      foo vide.
+let _ = dispatch begin function
+  | After_rules -> initial_actions (); extra_rules ()
+  | _ -> ()
+end
 
-    ==> Pour l'instant, les binaires sont dans _build/bin uniquement.
-    Une solution serait d'avoir deux repertoires de noms differents:
-    bin/ et _build/binaries/ par exemple.
+(** TODO / Remarques:
 
     * On repasse tout en revue sans arret, et c'est long, meme cached:
       1 min 25 pour les 2662 targets en cache.