diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /Makefile | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 127 |
1 files changed, 81 insertions, 46 deletions
@@ -1,12 +1,12 @@ ####################################################################### # v # The Coq Proof Assistant / The Coq Development Team # -# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # +# <O___,, # INRIA-Rocquencourt & LRI-CNRS-osay # # \VV/ ############################################################# # // # This file is distributed under the terms of the # # # GNU Lesser General Public License Version 2.1 # ####################################################################### -# $Id: Makefile 13182 2010-06-23 09:18:18Z notin $ +# $Id$ # Makefile for Coq @@ -16,7 +16,7 @@ # 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 -# http://www.pcug.org.au/~millerp/rmch/recu-make-cons-harm.html +# http://miller.emu.id.au/pmiller/books/rmch/ # before complaining. # # When you are working in a subdir, you can compile without moving to the @@ -24,6 +24,50 @@ # by Emacs' next-error. ########################################################################### + +# Specific command-line options to this Makefile +# +# make GOTO_STAGE=N # perform only stage N (with N=1,2) +# 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 + + +# 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* + +# !! Before using FIND_VCS_CLAUSE, please read how you should in the !! +# !! FIND_VCS_CLAUSE section of dev/doc/build-system.dev.txt !! export FIND_VCS_CLAUSE:='(' \ -name '{arch}' -o \ -name '.svn' -o \ @@ -31,9 +75,10 @@ export FIND_VCS_CLAUSE:='(' \ -name '.git' -o \ -name '.bzr' -o \ -name 'debian' -o \ - -name "$${GIT_DIR}" \ -')' -prune -type f -o -export PRUNE_CHECKER := -wholename ./checker/\* -prune -or + -name "$${GIT_DIR}" -o \ + -name '_build' \ +')' -prune -o +export PRUNE_CHECKER := -wholename ./checker/\* -prune -o FIND_PRINTF_P:=-print | sed 's|^\./||' @@ -43,20 +88,24 @@ 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.v +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) \ + 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') +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 + include Makefile.common NOARG: world @@ -82,7 +131,7 @@ define stage-template @echo '****************** Entering stage$(1) ******************' @echo '*****************************************************' @echo '*****************************************************' - +$(MAKE) -f Makefile.stage$(1) "$@" + +$(MAKE) $(MAKEFLGS) -f Makefile.stage$(1) "$@" endef else define stage-template @@ -106,39 +155,24 @@ config/Makefile Makefile.common Makefile.build Makefile: ; $(call stage-template,$(GOTO_STAGE)) else -.PHONY: stage1 stage2 stage3 world revision - -# This is to remove the built-in rule "%: %.o" -# Otherwise, "make foo" recurses into stage1, trying to build foo.o . -%: %.o - -%.o: always - $(call stage-template,1) +.PHONY: stage1 stage2 world revision -#STAGE1_TARGETS includes all object files necessary for $(STAGE1) -stage1 $(STAGE1_TARGETS): always +stage1 $(STAGE1_TARGETS) : always $(call stage-template,1) -CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.dep.ps %.dot -ifdef CM_STAGE1 -$(CAML_OBJECT_PATTERNS): always - $(call stage-template,1) - -%.ml4-preprocessed: stage1 - $(call stage-template,2) -else -$(CAML_OBJECT_PATTERNS) %.ml4-preprocessed: stage1 +stage2 $(STAGE2_TARGETS) : stage1 $(call stage-template,2) -endif -stage2 $(STAGE2_TARGETS): stage1 - $(call stage-template,2) +# 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 -%.vo %.glob states/% install-%: stage2 - $(call stage-template,3) -stage3 $(STAGE3_TARGETS): stage2 - $(call stage-template,3) +# This is to remove the built-in rule "%: %.o" : +%: %.o +# Otherwise, "make foo" recurses into stage1, trying to build foo.o . endif #GOTO_STAGE @@ -159,15 +193,16 @@ cruftclean: ml4clean indepclean: rm -f $(GENFILES) rm -f $(COQTOPBYTE) $(COQMKTOPBYTE) $(COQCBYTE) $(CHICKENBYTE) - rm -f bin/coq-interface$(EXE) bin/coq-parser$(EXE) find . -name '*~' -o -name '*.cm[ioa]' | xargs rm -f - find contrib test-suite -name '*.vo' -o -name '*.glob' | xargs rm -f - rm -f */*.pp[iox] contrib/*/*.pp[iox] + 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 rm -f test-suite/check.log rm -f glob.dump - rm -f revision + rm -f config/revision.ml revision + $(MAKE) -C test-suite clean docclean: rm -f doc/*/*.dvi doc/*/*.aux doc/*/*.log doc/*/*.bbl doc/*/*.blg doc/*/*.toc \ @@ -180,23 +215,22 @@ docclean: doc/stdlib/library.files.ls 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/stdlib/html/*.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/*.eps doc/refman/Reference-Manual.html rm -f doc/coq.tex - rm -f doc/refman/styles.hva doc/refman/cover.html archclean: clean-ide cleantheories - rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN) + rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN) $(COQDEPBOOT) rm -f $(COQTOPOPT) $(COQMKTOPOPT) $(COQCOPT) $(CHICKENOPT) - rm -f bin/coq-parser.opt$(EXE) bin/coq-interface.opt$(EXE) - find . -name '*.cmx' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f + 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 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/utf8_convert.ml @@ -208,12 +242,13 @@ ml4depclean: find . -name '*.ml4.d' | xargs rm -f depclean: - find . $(FIND_VCS_CLAUSE) -name '*.d' | xargs rm -f + find . $(FIND_VCS_CLAUSE) '(' -name '*.d' ')' -print | xargs rm -f cleanconfig: rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli distclean: clean cleanconfig + $(MAKE) -C test-suite distclean cleantheories: rm -f states/*.coq |