diff options
| -rw-r--r-- | Makefile | 68 | ||||
| -rw-r--r-- | Makefile.build | 50 | ||||
| -rw-r--r-- | Makefile.common | 60 | ||||
| -rw-r--r-- | Makefile.stage1 | 32 | ||||
| -rw-r--r-- | Makefile.stage2 | 23 |
5 files changed, 54 insertions, 179 deletions
@@ -27,7 +27,6 @@ # 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 @@ -58,7 +57,7 @@ # # * Useful builtin functions # -# $(subst ...), $(patsubst ...), $(shell ...), $(foreach ...) +# $(subst ...), $(patsubst ...), $(shell ...), $(foreach ...), $(if ...) # # * Behavior of -include # @@ -138,9 +137,7 @@ include Makefile.common NOARG: world -.PHONY: NOARG help always tags otags - -always: ; +.PHONY: NOARG help always help: @echo "Please use either" @@ -152,60 +149,33 @@ help: @echo @echo "For make to be verbose, add VERBOSE=1" -# Nota: do not use the name $(MAKEFLAGS), it has a particular behavior -MAKEFLGS:=--warn-undefined-variable --no-builtin-rules - -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 +%:: always + @echo "Please run ./configure first" >&2; exit 1 +endif -.PHONY: stage1 stage2 world revision - -stage1 $(STAGE1_TARGETS) : always - $(call stage-template,1) - -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 - +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 @@ -292,6 +262,8 @@ devdocclean: # Emacs tags ########################################################################### +.PHONY: tags otags + tags: echo $(MLIFILES) $(MLSTATICFILES) $(ML4FILES) | sort -r | xargs \ etags --language=none\ diff --git a/Makefile.build b/Makefile.build index eb1ab45bed..e06c80596b 100644 --- a/Makefile.build +++ b/Makefile.build @@ -24,25 +24,45 @@ # by Emacs' next-error. ########################################################################### -include Makefile.common -ifndef COQ_CONFIGURED - $(error Please run ./configure first) -endif - -.PHONY: NOARG - -NOARG: world +########################################################################### +# Starting rule +########################################################################### # build and install the three subsystems: coq, coqide world: revision coq coqide install: install-coq install-coqide +.PHONY: world install + +########################################################################### +# Includes +########################################################################### + +include Makefile.common +include Makefile.doc + ifeq ($(WITHDOC),all) world: doc install: install-doc endif -#install-manpages: install-coq-manpages +# All dependency includes must be declared secondary, otherwise make will +# delete them if it decided to build them by dependency instead of because +# of include, and they will then be automatically deleted, leading to an +# infinite loop. + +ALLDEPS=$(addsuffix .d, \ + $(ML4FILES) $(MLFILES) $(MLIFILES) $(CFILES) $(MLLIBFILES) $(VFILES)) + +.SECONDARY: $(ALLDEPS) $(GENFILES) $(GENML4FILES) + +# NOTA: the -include below will lauch the build of all .d. Some of them +# will _fail_ at first, this is to be expected (no grammar.cma initially). +# These errors (see below "not ready yet, will try again later") do not +# discourage make to try again and finally succeed. + +-include $(ALLDEPS) + ########################################################################### # Compilation options @@ -662,7 +682,7 @@ parsing/grammar.cma: | parsing/grammar.mllib.d ## of the ml4 toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml.d toplevel/mltop.ml4.d - $(SHOW)'OCAMLOPT $<' + $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $< -o $@ toplevel/mltop.ml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here @@ -764,7 +784,7 @@ $(MLWITHOUTMLI:.ml=.cmi): %.cmi: %.cmo %.cmx: %.ml | %.ml.d $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) -c -o $*.tmp.cmx $< && \ - rm -f $*.tmp.cmi && mv -f $*.tmp.o $*.o && mv -f $*.tmp.cmx $*.cmx + rm -f $*.tmp.cmi && mv -f $*.tmp.o $*.o && mv -f $*.tmp.cmx $*.cmx %.cmxs: %.cmxa $(SHOW)'OCAMLOPT -shared -o $@' @@ -791,11 +811,11 @@ plugins/%_mod.ml: plugins/%.mllib $(HIDE)sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@ $(HIDE)echo "let _=Mltop.add_known_module\"$(notdir $*)\"" >> $@ -.SECONDARY: $(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml)) - %.ml: %.ml4 | %.ml4.d $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(PR_O) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< $(TOTARGET) + $(HIDE)if ls `$(CAMLP4DEPS) $<` > /dev/null 2>&1; then \ + $(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(PR_O) `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< $(TOTARGET); \ + else echo Dependencies `$(CAMLP4DEPS) $<` not ready yet, will try again later; false; fi %.vo %.glob: %.v states/initial.coq $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | %.v.d $(VO_TOOLS_ORDER_ONLY) $(SHOW)'COQC $<' @@ -860,8 +880,6 @@ checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC) $(SHOW)'CCDEP $<' $(HIDE)$(CC) -MM -MQ "$@" -MQ "$(<:.c=.o)" $(CFLAGS) -isystem $(CAMLHLIB) $< $(TOTARGET) -.SECONDARY: $(GENFILES) $(GENML4FILES) - ########################################################################### # this sets up developper supporting stuff ########################################################################### diff --git a/Makefile.common b/Makefile.common index 8a29988d52..62a22d8b9b 100644 --- a/Makefile.common +++ b/Makefile.common @@ -261,20 +261,6 @@ COQDOCCMO:=$(CONFIG) $(addprefix tools/coqdoc/, \ cdglobals.cmo alpha.cmo index.cmo output.cmo cpretty.cmo main.cmo ) COQDOCCMX:=$(COQDOCCMO:.cmo=.cmx) -# grammar modules with camlp4 - -GRAMMARCMA:=parsing/grammar.cma - -GRAMMARML4:=lib/compat.ml4 lib/pp.ml4 parsing/q_util.ml4 parsing/pcoq.ml4 \ - parsing/argextend.ml4 parsing/tacextend.ml4 parsing/vernacextend.ml4 \ - parsing/g_prim.ml4 parsing/g_tactic.ml4 \ - parsing/g_ltac.ml4 parsing/g_constr.ml4 \ - parsing/lexer.ml4 parsing/q_coqast.ml4 - -STAGE1_ML4:=$(GRAMMARML4) parsing/q_constr.ml4 -STAGE1:=parsing/grammar.cma parsing/q_constr.cmo - - ########################################################################### # vo files ########################################################################### @@ -364,52 +350,6 @@ DATE=$(shell LANG=C date +"%B %Y") SOURCEDOCDIR=dev/source-doc -CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot - -### Targets forwarded by Makefile to a specific stage: - -## Enumeration of targets that require being done at stage1 - -STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \ - $(GENFILES) \ - source-doc revision toplevel/mltop.ml toplevel/mltop.optml \ - $(STAGE1_ML4:.ml4=.ml) %.o - -ifdef CM_STAGE1 - STAGE1_TARGETS+=$(CAML_OBJECT_PATTERNS) -endif - -## Enumeration of targets that require being done at stage2 - -VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \ - fsets relations wellfounded ints reals \ - setoids sorting natural integer rational numbers noreal \ - omega micromega ring setoid_ring dp xml extraction field fourier \ - funind cc subtac rtauto - -DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq \ - rectutorial refman-quick refman-nodep stdlib-nodep \ - install-doc install-doc-meta install-doc-html install-doc-printable install-doc-index-url \ - ide/index_urls.txt - -DOC_TARGET_PATTERNS:=%.dvi %.ps %.eps %.pdf %.html %.v.tex %.hva - -STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \ - interp parsing pretyping highparsing toplevel hightactics \ - coqide-binaries coqide-byte coqide-opt $(COQIDEOPT) $(COQIDEBYTE) $(COQIDE) \ - $(CSDPCERT) coqbinaries $(TOOLS) tools \ - printers debug initplugins plugins \ - world install coqide coqide-files coq coqlib \ - coqlight states check init theories theories-light \ - $(DOC_TARGETS) $(VO_TARGETS) validate \ - %.vo %.glob states/% install-% \ - $(DOC_TARGET_PATTERNS) - -ifndef CM_STAGE1 - STAGE2_TARGETS+=$(CAML_OBJECT_PATTERNS) -endif - - # For emacs: # Local Variables: # mode: makefile diff --git a/Makefile.stage1 b/Makefile.stage1 deleted file mode 100644 index 93d54eef91..0000000000 --- a/Makefile.stage1 +++ /dev/null @@ -1,32 +0,0 @@ -####################################################################### -# v # The Coq Proof Assistant / The Coq Development Team # -# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # -# \VV/ ############################################################# -# // # This file is distributed under the terms of the # -# # GNU Lesser General Public License Version 2.1 # -####################################################################### - -include Makefile.build - -# All includes must be declared secondary, otherwise make will delete -# them if it decided to build them by dependency instead of because of -# include, and they will then be automatically deleted, leading to an -# infinite loop. - -STAGE1_DEPS := $(addsuffix .d, \ - $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES) $(MLIFILES) $(CFILES) \ - $(MLLIBFILES) $(STAGE1_ML4:.ml4=.ml)) - -# NB: this depends upon the fact that .ml4.d for $(STAGE1_ML4) are empty, -# hence .ml and .ml.d for these .ml4 can be generated initially. - -.SECONDARY: $(STAGE1_DEPS) --include $(STAGE1_DEPS) - -.PHONY: stage1 -stage1: $(STAGE1) - -# For emacs: -# Local Variables: -# mode: makefile -# End: diff --git a/Makefile.stage2 b/Makefile.stage2 deleted file mode 100644 index e6a61b8e44..0000000000 --- a/Makefile.stage2 +++ /dev/null @@ -1,23 +0,0 @@ -####################################################################### -# v # The Coq Proof Assistant / The Coq Development Team # -# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # -# \VV/ ############################################################# -# // # This file is distributed under the terms of the # -# # GNU Lesser General Public License Version 2.1 # -####################################################################### - -include Makefile.stage1 -include Makefile.doc - -STAGE2_DEPS := $(addsuffix .d, $(GENPLUGINSMOD) $(GENML4FILES) $(VFILES)) - -.SECONDARY: $(STAGE2_DEPS) --include $(STAGE2_DEPS) - -# NB: all $(STAGE1_DEPS) are already included thanks to the inclusion of -# Makefile.stage1 - -# For emacs: -# Local Variables: -# mode: makefile -# End: |