From d63dee24c817560a6fea49dfe0c851b4df25ecf7 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 16 Mar 2009 13:41:49 +0000
Subject: coqdep_boot: a specialized and dependency-free coqdep for killing one
 of the build stages

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11984 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.build | 23 ++++++++++++++++++-----
 1 file changed, 18 insertions(+), 5 deletions(-)

(limited to 'Makefile.build')

diff --git a/Makefile.build b/Makefile.build
index 364ea3503c..96b72d5c17 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -74,7 +74,6 @@ CAMLP4EXTENDFLAGS=-I . #grammar dependencies are now in camlp4use statements
 CAMLP4DEPS=sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*\*)@\1@p'
 CAMLP4USE=sed -n -e 's/pa_macro.cmo/pa_macro.cmo -D$(CAMLVERSION)/' -e 's@^(\*.*camlp4use: "\(.*\)".*\*)@\1@p'
 
-COQINCLUDES=	# coqtop includes itself the needed paths
 COQ_XML=	# is "-xml" when building XML library
 VM=		# is "-no-vm" to not use the vm"
 UNBOXEDVALUES=	# is "-unboxed-values" to use unboxed values
@@ -555,6 +554,20 @@ printers: $(DEBUGPRINTERS)
 
 tools:: $(TOOLS) $(DEBUGPRINTERS)
 
+# coqdep_boot : a basic version of coqdep, with almost no dependencies
+
+$(COQDEPBOOT): $(COQDEPBOOTML)
+ifeq ($(BEST),opt)
+	$(SHOW)'OCAMLOPT -o $@'
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ -I tools unix.cmxa $^
+	$(STRIP) $@
+else
+	$(SHOW)'OCAMLC -o $@'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ -I tools unix.cma $^
+endif
+
+# the full coqdep
+
 ifeq ($(BEST),opt)
 $(COQDEP): $(COQDEPCMX)
 	$(SHOW)'OCAMLOPT -o $@'
@@ -953,9 +966,9 @@ checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC)
 	$(SHOW)'OCAMLDEP  $<'
 	$(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" | sed '' > "$@"
 
-%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEP)
+%.mllib.d: $(D_DEPEND_BEFORE_SRC) %.mllib $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT)
 	$(SHOW)'COQDEP  $<'
-	$(HIDE)$(COQDEP) -slash -boot -c "$<" > "$@" \
+	$(HIDE)$(COQDEPBOOT) -slash -boot -c "$<" > "$@" \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
 ## Veerry nasty hack to keep ocamldep happy
@@ -964,9 +977,9 @@ checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC)
 	$(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" > $@ \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
-%.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) -glob -slash -boot $(COQINCLUDES) "$<" > "$@" \
+	$(HIDE)$(COQDEPBOOT) $(DEPNATDYN) -slash -boot "$<" > "$@" \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
 %.c.d: $(D_DEPEND_BEFORE_SRC) %.c $(D_DEPEND_AFTER_SRC) $(GENHFILES)
-- 
cgit v1.2.3