diff options
| -rw-r--r-- | Makefile | 88 | ||||
| -rw-r--r-- | Makefile.build | 22 | ||||
| -rw-r--r-- | Makefile.common | 47 | ||||
| -rw-r--r-- | Makefile.doc | 18 | ||||
| -rw-r--r-- | Makefile.stage1 | 2 | ||||
| -rw-r--r-- | Makefile.stage2 | 2 |
6 files changed, 123 insertions, 56 deletions
@@ -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,3) +# 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:='(' \ @@ -59,6 +103,9 @@ export CFILES := $(shell find kernel/byterun $(FIND_VCS_CLAUSE) '(' -name '*.c 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 @@ -84,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 @@ -110,37 +157,26 @@ 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 +stage1 $(STAGE1_TARGETS) : always $(call stage-template,1) -#STAGE1_TARGETS includes all object files necessary for $(STAGE1) -stage1 $(STAGE1_TARGETS): always - $(call stage-template,1) - -CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.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 - $(call stage-template,2) -endif - -stage2 $(STAGE2_TARGETS): stage1 +stage2 $(STAGE2_TARGETS) : stage1 $(call stage-template,2) -%.vo %.glob states/% install-%: stage2 +stage3 $(STAGE3_TARGETS) : stage2 $(call stage-template,3) -stage3 $(STAGE3_TARGETS): stage2 - $(call stage-template,3) +# Nota: +# - world is one of the targets in $(STAGE3_TARGETS), hence launching +# "make" or "make world" leads to recursion into stage{1,2,3} +# - the aim of stage1 is to build grammar.cma and q_constr.cmo +# - the aim of stage2 is to build coqdep +# More details in dev/doc/build-system*.txt + + +# This is to remove the built-in rule "%: %.o" : +%: %.o +# Otherwise, "make foo" recurses into stage1, trying to build foo.o . endif #GOTO_STAGE diff --git a/Makefile.build b/Makefile.build index 5d5ff8533..364ea3503 100644 --- a/Makefile.build +++ b/Makefile.build @@ -34,14 +34,12 @@ endif NOARG: world # build and install the three subsystems: coq, coqide, pcoq -ifeq ($(WITHDOC),all) -world: revision coq coqide pcoq doc - -install: install-coq install-coqide install-pcoq install-doc -else world: revision coq coqide pcoq - install: install-coq install-coqide install-pcoq + +ifeq ($(WITHDOC),all) +world: doc +install: install-doc endif #install-manpages: install-coq-manpages install-pcoq-manpages @@ -54,7 +52,7 @@ endif # or only abbreviated versions. # Quiet mode is ON by default except if VERBOSE=1 option is given to make -ifeq ($(VERBOSE),1) +ifdef VERBOSE SHOW = @true "" HIDE = else @@ -110,7 +108,9 @@ ifdef VALIDATE endif ifdef NO_RECOMPILE_LIB VO_TOOLS_ORDER_ONLY:=$(VO_TOOLS_DEP) + VO_TOOLS_STRICT:= else + VO_TOOLS_ORDER_ONLY:= VO_TOOLS_STRICT:=$(VO_TOOLS_DEP) endif @@ -163,8 +163,6 @@ coqlight: theories-light tools coqbinaries states:: states/initial.coq -plugins: $(PLUGINSOPT) $(PLUGINS) - $(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -o $@ @@ -530,8 +528,7 @@ field: $(FIELDVO) $(FIELDCMA) fourier: $(FOURIERVO) $(FOURIERCMA) funind: $(FUNINDCMA) $(FUNINDVO) cc: $(CCVO) $(CCCMA) -programs: $(PROGRAMSVO) -subtac: $(SUBTACVO) $(SUBTACCMA) +subtac: $(SUBTACCMA) rtauto: $(RTAUTOVO) $(RTAUTOCMA) ########################################################################### @@ -720,8 +717,7 @@ install-latex: source-doc: if !(test -d $(SOURCEDOCDIR)); then mkdir $(SOURCEDOCDIR); fi - $(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) \ - `find . $(FIND_VCS_CLAUSE) '(' -name '*.ml' ')' -print` + $(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) $(MLFILES) ########################################################################### diff --git a/Makefile.common b/Makefile.common index ce1fad6b2..7fd52594c 100644 --- a/Makefile.common +++ b/Makefile.common @@ -33,6 +33,9 @@ CHICKEN:=bin/coqchk$(EXE) ifneq ($(HASNATDYNLINK),false) DYNLINKCMXA:=dynlink.cmxa NATDYNLINKDEF:=-DHasDynlink +else + DYNLINKCMXA:= + NATDYNLINKDEF:= endif INSTALLBIN:=install @@ -120,7 +123,7 @@ REFMANTEXFILES:=$(addprefix doc/refman/, \ REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps -REFMANFILES:=$(REFMANTEXFILES) $(COMMON) $(REFMANEPSFILES) doc/refman/biblio.bib +REFMANFILES:=$(REFMANTEXFILES) $(DOCCOMMON) $(REFMANEPSFILES) doc/refman/biblio.bib REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png) @@ -268,11 +271,15 @@ ifneq ($(HASNATDYNLINK),false) CONTRIBSTATIC:= INITPLUGINS:=$(EXTRACTIONCMA) $(FOCMA) $(CCCMA) $(DPCMA) \ $(XMLCMA) $(FUNINDCMA) $(SUBTACCMA) - PLUGINS:=$(CONTRIBS) INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs) + PLUGINS:=$(CONTRIBS) PLUGINSOPT:=$(PLUGINS:.cma=.cmxs) else CONTRIBSTATIC:=$(CONTRIBS) + INITPLUGINS:= + INITPLUGINSOPT:= + PLUGINS:= + PLUGINSOPT:= endif CMA:=$(CLIBS) $(CAMLP4OBJS) @@ -793,27 +800,49 @@ DATE=$(shell LANG=C date +"%B %Y") SOURCEDOCDIR=dev/source-doc -## Targets forwarded by Makefile to a specific stage +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) \ $(filter-out parsing/q_constr.cmo,$(STAGE1_CMO)) \ $(STAGE1_CMO:.cmo=.cmi) $(STAGE1_CMO:.cmo=.cmx) $(GENFILES) \ source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \ - $(STAGE1_ML4:.ml4=.ml4-preprocessed) + $(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o + +ifdef CM_STAGE1 + STAGE1_TARGETS+=$(CAML_OBJECT_PATTERNS) +endif + +## Enumeration of targets that require being done at stage2 + STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \ interp parsing pretyping highparsing toplevel hightactics \ coqide-binaries coqide-byte coqide-opt $(COQIDEOPT) $(COQIDEBYTE) $(COQIDE) \ pcoq-binaries $(COQINTERFACE) $(CSDPCERT) coqbinaries pcoq $(TOOLS) tools \ - printers debug initplugins plugins + printers debug initplugins plugins %.ml4-preprocessed + +ifndef CM_STAGE1 + STAGE2_TARGETS+=$(CAML_OBJECT_PATTERNS) +endif + +## Enumeration of targets that require being done at stage3 + VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \ fsets allfsets relations wellfounded ints reals allreals \ setoids sorting natural integer rational numbers noreal \ omega micromega ring setoid_ring dp xml extraction field fourier \ - funind cc programs subtac rtauto -DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq rectutorial refman-quick refman-nodep stdlib-nodep + funind cc subtac rtauto + +DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq \ + rectutorial refman-quick refman-nodep stdlib-nodep + STAGE3_TARGETS:=world install coqide coqide-files coq coqlib \ coqlight states pcoq-files check init theories theories-light contrib \ - $(DOC_TARGETS) $(VO_TARGETS) validate - + $(DOC_TARGETS) $(VO_TARGETS) validate \ + %.vo %.glob states/% install-% # For emacs: # Local Variables: diff --git a/Makefile.doc b/Makefile.doc index 2190ebf69..cf849dadf 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -45,11 +45,11 @@ rectutorial: doc/RecTutorial/RecTutorial.html \ ### Implicit rules ###################################################################### -ifeq ($(QUICK),1) +ifdef QUICK %.v.tex: %.tex (cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`) else -%.v.tex: %.tex | $(COQTEX) $(COQTOPEXE) $(CONTRIBVO) $(CONTRIBCMO) $(THEORIESVO) +%.v.tex: %.tex | $(COQTEX) $(COQTOPEXE) $(CONTRIBVO) $(THEORIESVO) (cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`) endif @@ -87,7 +87,7 @@ doc/common/version.tex: config/Makefile # The second LATEX compilation is necessary otherwise the pages of the index # are not correct (don't know why...) - BB -doc/refman/Reference-Manual.dvi: $(DOCCOMMON) $(REFMANFILES) doc/refman/Reference-Manual.tex +doc/refman/Reference-Manual.dvi: $(REFMANFILES) doc/refman/Reference-Manual.tex @(cd doc/refman;\ $(LATEX) -interaction=batchmode Reference-Manual;\ $(BIBTEX) -terse Reference-Manual $(HIDEBIBTEXINFO);\ @@ -102,7 +102,7 @@ doc/refman/Reference-Manual.dvi: $(DOCCOMMON) $(REFMANFILES) doc/refman/Referenc $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ $(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\ $(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\ - ../tools/show_latex_messages -no-overfull Reference-Manual.log) + ../tools/show_latex_messages -no-overfull Reference-Manual.log) doc/refman/Reference-Manual.pdf: $(REFMANFILES) doc/refman/Reference-Manual.tex (cd doc/refman;\ @@ -185,7 +185,7 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html ### Standard library (browsable html format) -ifeq ($(QUICK),1) +ifdef QUICK doc/stdlib/index-body.html: - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html @@ -211,7 +211,7 @@ doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.htm ### Standard library (light version, full version is definitely too big) -ifeq ($(QUICK),1) +ifdef QUICK doc/stdlib/Library.coqdoc.tex: $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ @@ -292,3 +292,9 @@ install-doc-printable: $(INSTALLLIB) doc/tutorial/Tutorial.v.ps $(FULLDOCDIR)/ps/Tutorial.ps $(INSTALLLIB) doc/RecTutorial/RecTutorial.ps $(FULLDOCDIR)/ps/RecTutorial.ps $(INSTALLLIB) doc/faq/FAQ.v.ps $(FULLDOCDIR)/ps/FAQ.ps + + +# For emacs: +# Local Variables: +# mode: makefile +# End: diff --git a/Makefile.stage1 b/Makefile.stage1 index a558e3aa6..a60d388fc 100644 --- a/Makefile.stage1 +++ b/Makefile.stage1 @@ -18,8 +18,6 @@ include Makefile.build .SECONDARY: $(MLFILES:.ml=.ml.d) -include $(MLIFILES:.mli=.mli.d) .SECONDARY: $(MLIFILES:.mli=.mli.d) --include $(MLLIBFILES:.mllib=.mllib.d) -.SECONDARY: $(MLLIBFILES:.mli=.mllib.d) ##Depends upon the fact that all .ml4.d for stage1 files are empty -include $(STAGE1_ML4:.ml4=.ml4.ml.d) .SECONDARY: $(STAGE1_ML4:.ml4=.ml4.ml.d) diff --git a/Makefile.stage2 b/Makefile.stage2 index 6fe020be9..81e192cfc 100644 --- a/Makefile.stage2 +++ b/Makefile.stage2 @@ -8,6 +8,8 @@ include Makefile.stage1 +-include $(MLLIBFILES:.mllib=.mllib.d) +.SECONDARY: $(MLLIBFILES:.mli=.mllib.d) -include $(ML4FILES:.ml4=.ml4.ml.d) .SECONDARY: $(ML4FILES:.ml4=.ml4.ml.d) |