Using home-made ocamllibdep rather than coqdep_boot.

3 files changed, 11 insertions, 65 deletions

diff --git a/Makefile.build b/Makefile.build
index 572ea497d2..a0f7879d53 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -597,7 +597,7 @@ theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_g
 
 printers: $(DEBUGPRINTERS)
 
-tools: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT)
+tools: $(TOOLS) $(DEBUGPRINTERS) $(OCAMLLIBDEP)
 
 # coqdep_boot : a basic version of coqdep, with almost no dependencies.
 
@@ -605,12 +605,9 @@ tools: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT)
 # to avoid using implicit rules and hence .ml.d files that would need
 # coqdep_boot.
 
-COQDEPBOOTSRC:= \
-  tools/coqdep_lexer.mli tools/coqdep_lexer.ml \
-  tools/coqdep_common.mli tools/coqdep_common.ml \
-  tools/coqdep_boot.ml
+OCAMLLIBDEPSRC:= tools/ocamllibdep.ml
 
-$(COQDEPBOOT): $(COQDEPBOOTSRC)
+$(OCAMLLIBDEP): $(OCAMLLIBDEPSRC)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -I tools, unix)
 
@@ -1074,13 +1071,13 @@ checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(GE
 	$(SHOW)'OCAMLDEP  $<'
 	$(HIDE)$(OCAMLDEP_NG) $(DEPFLAGS) "$<" $(TOTARGET)
 
-checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
-	$(SHOW)'COQDEP  $<'
-	$(HIDE)$(COQDEPBOOT) -I checker -c "$<" $(TOTARGET)
+checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES)
+	$(SHOW)'OCAMLLIBDEP  $<'
+	$(HIDE)$(OCAMLLIBDEP) $(LOCALCHKLIBS) "$<" $(TOTARGET)
 
-%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
-	$(SHOW)'COQDEP  $<'
-	$(HIDE)$(COQDEPBOOT) -I kernel -I tools/coqdoc -c "$<" $(TOTARGET)
+%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLLIBDEP) $(GENFILES)
+	$(SHOW)'OCAMLLIBDEP  $<'
+	$(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET)
 
 %.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEP) $(GENVFILES)
 	$(SHOW)'COQDEP    $<'
diff --git a/Makefile.common b/Makefile.common
index e548619610..7ec7dbe55f 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -87,7 +87,7 @@ CHKSRCDIRS:= checker lib config kernel parsing
 ###########################################################################
 
 COQDEP:=bin/coqdep$(EXE)
-COQDEPBOOT:=bin/coqdep_boot$(EXE)
+OCAMLLIBDEP:=bin/ocamllibdep$(EXE)
 COQMAKEFILE:=bin/coq_makefile$(EXE)
 GALLINA:=bin/gallina$(EXE)
 COQTEX:=bin/coq-tex$(EXE)
@@ -99,7 +99,7 @@ COQWORKMGR:=bin/coqworkmgr$(EXE)
 TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\
 	$(COQWORKMGR)
 
-PRIVATEBINARIES:=$(FAKEIDE) $(COQDEPBOOT)
+PRIVATEBINARIES:=$(FAKEIDE) $(OCAMLLIBDEP)
 
 ###########################################################################
 # Documentation
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
deleted file mode 100644
index bc3435a644..0000000000
--- a/tools/coqdep_boot.ml
+++ /dev/null
@@ -1,51 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Coqdep_common
-
-(** [coqdep_boot] is a stripped-down version of [coqdep], whose
-    behavior is the one of [coqdep -boot]. Its only dependencies
-    are [Coqdep_lexer], [Coqdep_common] and [Unix], and it should stay so.
-    If it needs someday some additional information, pass it via
-    options (see for instance [option_natdynlk] below).
-*)
-
-let rec parse = function
-  | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll
-  | "-c" :: ll -> option_c := true; parse ll
-  | "-boot" :: ll -> parse ll (* We're already in boot mode by default *)
-  | "-mldep" :: ocamldep :: ll ->
-      option_mldep := Some ocamldep; option_c := true; parse ll
-  | "-I" :: r :: ll ->
-       (* To solve conflict (e.g. same filename in kernel and checker)
-          we allow to state an explicit order *)
-       add_caml_dir r;
-       norec_dirs:=r::!norec_dirs;
-       parse ll
-  | f :: ll -> treat_file None f; parse ll
-  | [] -> ()
-
-let coqdep_boot () =
-  let () = option_boot := true in
-  if Array.length Sys.argv < 2 then exit 1;
-  parse (List.tl (Array.to_list Sys.argv));
-  if !option_c then begin
-    add_rec_dir add_known "." [];
-    add_rec_dir (fun _ -> add_caml_known) "." ["Coq"];
-  end
-  else begin
-    add_rec_dir add_known "theories" ["Coq"];
-    add_rec_dir add_known "plugins" ["Coq"];
-    add_caml_dir "tactics";
-    add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"];
-    add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"];
-  end;
-  if !option_c then mL_dependencies ();
-  coq_dependencies ()
-
-let _ = Printexc.catch coqdep_boot ()