From 1532e4d57fce07e8a1cd6838853a4a31ea84e453 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 31 May 2016 23:20:21 +0200
Subject: Makefile: restore the use of coqdep_boot for creating .v.d files

 Coqdep_boot has almost no dependencies, and hence can be compiled
 very early during the build, without relying on .ml.d files.
 Some code of system.ml is now in a separate file minisys.ml,
 which is also included in system.ml for compatibility.
---
 Makefile.build | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

(limited to 'Makefile.build')

diff --git a/Makefile.build b/Makefile.build
index 190a62d000..dbf60afb78 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -611,6 +611,16 @@ tools: $(TOOLS) $(DEBUGPRINTERS) $(OCAMLLIBDEP)
 # to avoid using implicit rules and hence .ml.d files that would need
 # coqdep_boot.
 
+COQDEPBOOTSRC := \
+ lib/minisys.ml \
+ tools/coqdep_lexer.mli tools/coqdep_lexer.ml \
+ tools/coqdep_common.mli tools/coqdep_common.ml \
+ tools/coqdep_boot.ml
+
+$(COQDEPBOOT): $(COQDEPBOOTSRC)
+	$(SHOW)'OCAMLBEST -o $@'
+	$(HIDE)$(call bestocaml, -I tools, unix)
+
 OCAMLLIBDEPSRC:= tools/ocamllibdep.ml
 
 $(OCAMLLIBDEP): $(OCAMLLIBDEPSRC)
@@ -1093,9 +1103,9 @@ dev/%.mllib.d: $(D_DEPEND_BEFORE_SRC) dev/%.mllib $(D_DEPEND_AFTER_SRC) $(OCAMLL
 	$(SHOW)'OCAMLLIBDEP  $<'
 	$(HIDE)$(OCAMLLIBDEP) $(DEPFLAGS) "$<" $(TOTARGET)
 
-%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEP) $(GENVFILES)
+%.v.d: $(D_DEPEND_BEFORE_SRC) %.v $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENVFILES)
 	$(SHOW)'COQDEP    $<'
-	$(HIDE)$(COQDEP) -boot $(DEPNATDYN) "$<" $(TOTARGET)
+	$(HIDE)$(COQDEPBOOT) -boot $(DEPNATDYN) "$<" $(TOTARGET)
 
 %_stubs.c.d: $(D_DEPEND_BEFORE_SRC) %_stubs.c $(D_DEPEND_AFTER_SRC)
 	$(SHOW)'CCDEP	$<'
-- 
cgit v1.2.3