Imported Upstream version 8.5~beta1+dfsg

1 files changed, 49 insertions, 41 deletions

diff --git a/Makefile b/Makefile
index bb5ec3bc..c7fb1ff7 100644
--- a/Makefile
+++ b/Makefile
@@ -26,7 +26,6 @@
 #
 # make VERBOSE=1           # restore the raw echoing of commands
 # make NO_RECALC_DEPS=1    # avoid recomputing dependencies
-# make NO_RECOMPILE_LIB=1  # a coqtop rebuild does not trigger a stdlib rebuild
 #
 # Nota: the 1 above can be replaced by any non-empty value
 #
@@ -60,11 +59,20 @@ define find
  $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -print | sed 's|^\./||')
 endef
 
+define findx
+ $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -exec $(2) {} \; | sed 's|^\./||')
+endef
+
+# We now discriminate .ml4 files according to their need of grammar.cma
+# or q_constr.cmo
+USEGRAMMAR := '(\*.*camlp4deps.*grammar'
+
 ## Files in the source tree
 
 YACCFILES:=$(call find, '*.mly')
 LEXFILES := $(call find, '*.mll')
 export MLLIBFILES := $(call find, '*.mllib')
+export ML4BASEFILES := $(call findx, '*.ml4', grep -L -e $(USEGRAMMAR))
 export ML4FILES := $(call find, '*.ml4')
 export CFILES := $(call find, '*.c')
 
@@ -78,13 +86,13 @@ EXISTINGMLI := $(call find, '*.mli')
 ## Files that will be generated
 
 GENML4FILES:= $(ML4FILES:.ml4=.ml)
-GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
-  scripts/tolink.ml kernel/copcodes.ml
 GENMLIFILES:=$(YACCFILES:.mly=.mli)
 GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
+export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
+  tools/tolink.ml kernel/copcodes.ml $(GENPLUGINSMOD)
 export GENHFILES:=kernel/byterun/coq_jumptbl.h
 export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v
-export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) $(GENPLUGINSMOD)
+export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES)
 
 # NB: all files in $(GENFILES) can be created initially, while
 # .ml files in $(GENML4FILES) might need some intermediate building.
@@ -96,8 +104,7 @@ define diff
  $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f)))
 endef
 
-export MLEXTRAFILES := $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD)
-export MLSTATICFILES := $(call diff, $(EXISTINGML), $(MLEXTRAFILES))
+export MLSTATICFILES := $(call diff, $(EXISTINGML), $(GENMLFILES) $(GENML4FILES))
 export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI))
 
 include Makefile.common
@@ -108,7 +115,7 @@ include Makefile.common
 
 NOARG: world
 
-.PHONY: NOARG help always
+.PHONY: NOARG help noconfig submake
 
 help:
 	@echo "Please use either"
@@ -132,17 +139,27 @@ endif
 
 # Apart from clean and tags, everything will be done in a sub-call to make
 # on Makefile.build. This way, we avoid doing here the -include of .d :
-# since they trigger some compilations, we do not want them for a mere clean
+# since they trigger some compilations, we do not want them for a mere clean.
+# Moreover, we regroup this sub-call in a common target named 'submake'.
+# This way, multiple user-given goals (cf the MAKECMDGOALS variable) won't
+# trigger multiple (possibly parallel) make sub-calls
 
 ifdef COQ_CONFIGURED
-%:: always
-	$(MAKE) --warn-undefined-variable --no-builtin-rules -f Makefile.build "$@"
+%:: submake ;
 else
-%:: always
-	@echo "Please run ./configure first" >&2; exit 1
+%:: noconfig ;
 endif
 
-always : ;
+MAKE_OPTS := --warn-undefined-variable --no-builtin-rules
+
+GRAM_TARGETS := grammar/grammar.cma grammar/q_constr.cmo
+
+submake:
+	$(MAKE) $(MAKE_OPTS) -f Makefile.build BUILDGRAMMAR=1 $(GRAM_TARGETS)
+	$(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS)
+
+noconfig:
+	@echo "Please run ./configure first" >&2; exit 1
 
 # To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles
 
@@ -166,8 +183,8 @@ cruftclean: ml4clean
 
 indepclean:
 	rm -f $(GENFILES)
-	rm -f $(COQTOPBYTE) $(COQMKTOPBYTE) $(COQCBYTE) $(CHICKENBYTE) bin/fake_ide
-	find . -name '*~' -o -name '*.cm[ioa]' | xargs rm -f
+	rm -f $(COQTOPBYTE) $(CHICKENBYTE) $(FAKEIDE)
+	find . \( -name '*~' -o -name '*.cm[ioat]' -o -name '*.cmti' \) -delete
 	rm -f */*.pp[iox] plugins/*/*.pp[iox]
 	rm -rf $(SOURCEDOCDIR)
 	rm -f toplevel/mltop.byteml toplevel/mltop.optml
@@ -192,23 +209,22 @@ docclean:
 	rm -f doc/common/version.tex
 	rm -f doc/refman/styles.hva doc/refman/cover.html doc/refman/Reference-Manual.html
 	rm -f doc/coq.tex
-	rm -f doc/refman/styles.hva doc/refman/cover.html 
 
 archclean: clean-ide optclean voclean
-	rm -rf _build myocamlbuild_config.ml
+	rm -rf _build
 	rm -f $(ALLSTDLIB).*
 
 optclean:
 	rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN) $(COQDEPBOOT)
-	rm -f $(COQTOPOPT) $(COQMKTOPOPT) $(COQCOPT) $(CHICKENOPT)
 	rm -f $(TOOLS) $(CSDPCERT)
 	find . -name '*.cmx' -o -name '*.cmxs' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f
 
 clean-ide:
-	rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE)
+	rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDE)
 	rm -f ide/input_method_lexer.ml
 	rm -f ide/highlight.ml ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml
 	rm -f ide/utf8_convert.ml
+	rm -rf $(COQIDEAPP)
 
 ml4clean:
 	rm -f $(GENML4FILES)
@@ -219,14 +235,16 @@ ml4depclean:
 depclean:
 	find . $(FIND_VCS_CLAUSE) '(' -name '*.d' ')' -print | xargs rm -f
 
+cacheclean:
+	find theories plugins test-suite -name '.*.aux' -delete
+
 cleanconfig:
-	rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli
+	rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-v7 config/Info-*.plist
 
-distclean: clean cleanconfig
+distclean: clean cleanconfig cacheclean
 
 voclean:
-	rm -f states/*.coq
-	find theories plugins test-suite -name '*.vo' -o -name '*.glob' | xargs rm -f
+	find theories plugins test-suite \( -name '*.vo' -o -name '*.glob' -o -name "*.cmxs" -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -delete
 
 devdocclean:
 	find . -name '*.dep.ps' -o -name '*.dot' | xargs rm -f
@@ -238,10 +256,10 @@ devdocclean:
 # Emacs tags
 ###########################################################################
 
-.PHONY: tags otags
+.PHONY: tags printenv
 
 tags:
-	echo $(MLIFILES) $(MLSTATICFILES) $(ML4FILES) | sort -r | xargs \
+	echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(ML4FILES) | sort -r | xargs \
 	etags --language=none\
 	      "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
@@ -254,11 +272,9 @@ tags:
 	etags --append --language=none\
 	      "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/"
 
-
-otags: 
-	echo $(MLIFILES) $(MLSTATICFILES) | sort -r | xargs otags
-	echo $(ML4FILES) | sort -r | xargs \
-	etags --append --language=none\
+checker-tags:
+	echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(ML4FILES) | sort -r | xargs \
+	etags --language=none\
 	      "--regex=/let[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/and[ \t]+\([^ \t]+\)/\1/" \
@@ -266,17 +282,9 @@ otags:
               "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"
-
-
-%.elc: %.el
-ifdef COQ_CONFIGURED
-	echo "(setq load-path (cons \".\" load-path))" > $*.compile
-	echo "(byte-compile-file \"$<\")" >> $*.compile
-	- $(EMACS) -batch -l $*.compile
-	rm -f $*.compile
-else
-	@echo "Please run ./configure first" >&2; exit 1
-endif
+	echo $(ML4FILES) | sort -r | xargs \
+	etags --append --language=none\
+	      "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/"
 
 # Useful to check that the exported variables are within the win32 limits