From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- Makefile | 90 +++++++++++++++++++++++++++++++++++----------------------------- 1 file changed, 49 insertions(+), 41 deletions(-) (limited to 'Makefile') 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 -- cgit v1.2.3