From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- Makefile | 231 +++++++++++++++++++++++++++------------------------------------ 1 file changed, 99 insertions(+), 132 deletions(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 97afdfd6..876ac583 100644 --- a/Makefile +++ b/Makefile @@ -6,65 +6,38 @@ # # GNU Lesser General Public License Version 2.1 # ####################################################################### -# $Id: Makefile 14090 2011-05-03 13:34:16Z pboutill $ - # Makefile for Coq # -# To be used with GNU Make. +# To be used with GNU Make >= 3.81. # -# This is the only Makefile. You won't find Makefiles in sub-directories -# and this is done on purpose. If you are not yet convinced of the advantages -# of a single Makefile, please read +# This Makefile is now separated into Makefile.{common,build,doc}. +# You won't find Makefiles in sub-directories and this is done on purpose. +# If you are not yet convinced of the advantages of a single Makefile, please +# read # http://miller.emu.id.au/pmiller/books/rmch/ # before complaining. # # When you are working in a subdir, you can compile without moving to the # upper directory using "make -C ..", and the output is still understood # by Emacs' next-error. -########################################################################### - - -# Specific command-line options to this Makefile # -# make GOTO_STAGE=N # perform only stage N (with N=1,2) +# Specific command-line options to this Makefile: +# # 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 -# More details in dev/doc/build-system*.txt +# +# ---------------------------------------------------------------------- +# See dev/doc/build-system*.txt for more details/FAQ about this Makefile +# ---------------------------------------------------------------------- -# FAQ: special features used in this Makefile -# -# * Order-only dependencies: | -# -# Dependencies placed after a bar (|) should be built before -# the current rule, but having one of them is out-of-date do not -# trigger a rebuild of the current rule. -# See http://www.gnu.org/software/make/manual/make.html#Prerequisite-Types -# -# * Annotation before commands: +/-/@ -# -# a command starting by - is always successful (errors are ignored) -# a command starting by + is runned even if option -n is given to make -# a command starting by @ is not echoed before being runned -# -# * Custom functions -# -# Definition via "define foo" followed by commands (arg is $(1) etc) -# Call via "$(call foo,arg1)" -# -# * Useful builtin functions -# -# $(subst ...), $(patsubst ...), $(shell ...), $(foreach ...) -# -# * Behavior of -include -# -# If the file given to -include doesn't exist, make tries to build it, -# but doesn't care if this build fails. This can be quite surprising, -# see in particular the -include in Makefile.stage* +########################################################################### +# File lists +########################################################################### # !! Before using FIND_VCS_CLAUSE, please read how you should in the !! # !! FIND_VCS_CLAUSE section of dev/doc/build-system.dev.txt !! @@ -78,41 +51,63 @@ export FIND_VCS_CLAUSE:='(' \ -name "$${GIT_DIR}" -o \ -name '_build' \ ')' -prune -o -export PRUNE_CHECKER := -wholename ./checker/\* -prune -o -FIND_PRINTF_P:=-print | sed 's|^\./||' +define find + $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -print | sed 's|^\./||') +endef + +## Files in the source tree + +export YACCFILES:=$(call find, '*.mly') +export LEXFILES := $(call find, '*.mll') +export MLLIBFILES := $(call find, '*.mllib') +export ML4FILES := $(call find, '*.ml4') +export CFILES := $(call find, '*.c') + +# NB: The lists of currently existing .ml and .mli files will change +# before and after a build or a make clean. Hence we do not export +# these variables, but cleaned-up versions (see below MLFILES and co) + +EXISTINGML := $(call find, '*.ml') +EXISTINGMLI := $(call find, '*.mli') + +## Files that will be generated -export YACCFILES:=$(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mly' ')' $(FIND_PRINTF_P)) -export LEXFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mll' ')' $(FIND_PRINTF_P)) export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \ scripts/tolink.ml kernel/copcodes.ml export GENMLIFILES:=$(YACCFILES:.mly=.mli) export GENHFILES:=kernel/byterun/coq_jumptbl.h export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v -export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) -export MLFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml' ')' $(FIND_PRINTF_P) | \ - while read f; do if ! [ -e "$${f}4" ]; then echo "$$f"; fi; done) \ - $(GENMLFILES) -export MLIFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mli' ')' $(FIND_PRINTF_P)) \ - $(GENMLIFILES) -export MLLIBFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mllib' ')' $(FIND_PRINTF_P)) -export ML4FILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml4' ')' $(FIND_PRINTF_P)) -#export VFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.v' ')' $(FIND_PRINTF_P)) \ -# $(GENVFILES) -export CFILES := $(shell find kernel/byterun $(FIND_VCS_CLAUSE) '(' -name '*.c' ')' -print) - -export ML4FILESML:= $(ML4FILES:.ml4=.ml) - -# Nota: do not use the name $(MAKEFLAGS), it has a particular behavior -MAKEFLGS:=--warn-undefined-variable --no-builtin-rules +export GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml)) +export GENML4FILES:= $(ML4FILES:.ml4=.ml) +export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES) $(GENPLUGINSMOD) + +# NB: all files in $(GENFILES) can be created initially, while +# .ml files in $(GENML4FILES) might need some intermediate building. +# That's why we keep $(GENML4FILES) out of $(GENFILES) + +## More complex file lists + +define diff + $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f))) +endef + +export MLSTATICFILES := \ + $(call diff, $(EXISTINGML), $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD)) +export MLFILES := \ + $(sort $(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(GENPLUGINSMOD)) +export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI)) +export MLWITHOUTMLI := $(call diff, $(MLFILES), $(MLIFILES:.mli=.ml)) include Makefile.common -NOARG: world +########################################################################### +# Starting rules +########################################################################### -.PHONY: NOARG help always tags otags +NOARG: world -always: ; +.PHONY: NOARG help always help: @echo "Please use either" @@ -124,76 +119,44 @@ help: @echo @echo "For make to be verbose, add VERBOSE=1" -ifdef COQ_CONFIGURED -define stage-template - @echo '*****************************************************' - @echo '*****************************************************' - @echo '****************** Entering stage$(1) ******************' - @echo '*****************************************************' - @echo '*****************************************************' - +$(MAKE) $(MAKEFLGS) -f Makefile.stage$(1) "$@" -endef -else -define stage-template - @echo "Please run ./configure first" >&2; exit 1 -endef -endif - -UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.mli' -o -name '.\#*.ml4') +UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?') ifdef UNSAVED_FILES -$(error You have unsaved changes in your editor (emacs?) [$(UNSAVED_FILES)]; cancel them or save before proceeding. \ -Or your editor crashed. Then, you may want to consider whether you want to restore the autosaves) +$(error You have unsaved changes in your editor (emacs?) [$(UNSAVED_FILES)]; \ +cancel them or save before proceeding. Or your editor crashed. \ +Then, you may want to consider whether you want to restore the autosaves) #If you try to simply remove this explicit test, the compilation may #fail later. In particular, if a .#*.v file exists, coqdep fails to #run. endif -ifdef GOTO_STAGE -config/Makefile Makefile.common Makefile.build Makefile: ; +# 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 -%: always - $(call stage-template,$(GOTO_STAGE)) +ifdef COQ_CONFIGURED +%:: always + $(MAKE) --warn-undefined-variable --no-builtin-rules -f Makefile.build "$@" else - -.PHONY: stage1 stage2 world revision - -stage1 $(STAGE1_TARGETS) : always - $(call stage-template,1) - -ifneq (,$(STAGE1_IMPLICITS)) -$(STAGE1_IMPLICITS) : always - $(call stage-template,1) -endif - -stage2 $(STAGE2_TARGETS) : stage1 - $(call stage-template,2) - -ifneq (,$(STAGE2_IMPLICITS)) -$(STAGE2_IMPLICITS) : stage1 - $(call stage-template,2) +%:: always + @echo "Please run ./configure first" >&2; exit 1 endif -# Nota: -# - world is one of the targets in $(STAGE2_TARGETS), hence launching -# "make" or "make world" leads to recursion into stage1 then stage2 -# - the aim of stage1 is to build grammar.cma and q_constr.cmo -# More details in dev/doc/build-system*.txt - +always : ; -# This is to remove the built-in rule "%: %.o" : -%: %.o -# Otherwise, "make foo" recurses into stage1, trying to build foo.o . +# To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles -endif #GOTO_STAGE +Makefile Makefile.build Makefile.common config/Makefile : ; ########################################################################### # Cleaning ########################################################################### -.PHONY: clean objclean cruftclean indepclean archclean ml4clean clean-ide ml4depclean depclean distclean cleanconfig cleantheories docclean devdocclean +.PHONY: clean cleankeepvo objclean cruftclean indepclean doclean archclean optclean clean-ide ml4clean ml4depclean depclean cleanconfig distclean voclean devdocclean clean: objclean cruftclean depclean docclean devdocclean +cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean devdocclean + objclean: archclean indepclean cruftclean: ml4clean @@ -202,10 +165,8 @@ cruftclean: ml4clean indepclean: rm -f $(GENFILES) - rm -f $(COQTOPBYTE) $(COQMKTOPBYTE) $(COQCBYTE) $(CHICKENBYTE) + rm -f $(COQTOPBYTE) $(COQMKTOPBYTE) $(COQCBYTE) $(CHICKENBYTE) bin/fake_ide find . -name '*~' -o -name '*.cm[ioa]' | xargs rm -f - find . -name '*_mod.ml' | xargs rm -f - find plugins test-suite -name '*.vo' -o -name '*.glob' | xargs rm -f rm -f */*.pp[iox] plugins/*/*.pp[iox] rm -rf $(SOURCEDOCDIR) rm -f toplevel/mltop.byteml toplevel/mltop.optml @@ -221,33 +182,34 @@ docclean: doc/*/*.hatoc doc/*/*.haux doc/*/*.hcomind doc/*/*.herrind doc/*/*.hidx doc/*/*.hind \ doc/*/*.htacind doc/*/*.htoc doc/*/*.v.html rm -f doc/stdlib/index-list.html doc/stdlib/index-body.html \ - doc/stdlib/Library.coqdoc.tex doc/stdlib/library.files \ - doc/stdlib/library.files.ls - rm -f doc/*/*.ps doc/*/*.pdf + doc/stdlib/*Library.coqdoc.tex doc/stdlib/library.files \ + doc/stdlib/library.files.ls doc/stdlib/FullLibrary.tex + rm -f doc/*/*.ps doc/*/*.pdf rm -rf doc/refman/html doc/stdlib/html doc/faq/html doc/tutorial/tutorial.v.html rm -f doc/refman/euclid.ml doc/refman/euclid.mli rm -f doc/refman/heapsort.ml doc/refman/heapsort.mli 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 cleantheories +archclean: clean-ide optclean voclean + rm -rf _build myocamlbuild_config.ml + rm -f $(ALLSTDLIB).* + +optclean: rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN) $(COQDEPBOOT) rm -f $(COQTOPOPT) $(COQMKTOPOPT) $(COQCOPT) $(CHICKENOPT) - find . -name '*.cmx' -o -name '*.cmxs' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f rm -f $(TOOLS) $(CSDPCERT) - rm -rf _build myocamlbuild_config.ml + 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 ide/input_method_lexer.ml - rm -f ide/extract_index.ml ide/find_phrase.ml ide/highlight.ml - rm -f ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml + rm -f ide/highlight.ml ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml rm -f ide/utf8_convert.ml ml4clean: - rm -f $(ML4FILESML) $(ML4FILESML:.ml=.ml4-preprocessed) + rm -f $(GENML4FILES) ml4depclean: find . -name '*.ml4.d' | xargs rm -f @@ -261,19 +223,24 @@ cleanconfig: distclean: clean cleanconfig $(MAKE) -C test-suite distclean -cleantheories: +voclean: rm -f states/*.coq - find theories -name '*.vo' -o -name '*.glob' | xargs rm -f + find theories plugins test-suite -name '*.vo' -o -name '*.glob' | xargs rm -f devdocclean: - find . -name '*.dep.ps' -o -name '*.dot' -exec rm -f {} \; + find . -name '*.dep.ps' -o -name '*.dot' | xargs rm -f + rm -f $(OCAMLDOCDIR)/*.log $(OCAMLDOCDIR)/*.aux $(OCAMLDOCDIR)/*.toc + rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex + rm -f $(OCAMLDOCDIR)/html/*.html ########################################################################### # Emacs tags ########################################################################### +.PHONY: tags otags + tags: - echo $(MLIFILES) $(MLFILES) $(ML4FILES) | sort -r | xargs \ + echo $(MLIFILES) $(MLSTATICFILES) $(ML4FILES) | sort -r | xargs \ etags --language=none\ "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ @@ -288,7 +255,7 @@ tags: otags: - echo $(MLIFILES) $(MLFILES) | sort -r | xargs otags + echo $(MLIFILES) $(MLSTATICFILES) | sort -r | xargs otags echo $(ML4FILES) | sort -r | xargs \ etags --append --language=none\ "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ -- cgit v1.2.3