diff options
| -rw-r--r-- | Makefile | 7 | ||||
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | Makefile.common | 3 | ||||
| -rw-r--r-- | Makefile.stage0 | 21 | ||||
| -rw-r--r-- | Makefile.stage1 | 14 | ||||
| -rw-r--r-- | Makefile.stage2 | 1 | ||||
| -rw-r--r-- | Makefile.stage3 | 1 | ||||
| -rw-r--r-- | dev/doc/build-system.dev.txt | 3 |
8 files changed, 18 insertions, 34 deletions
@@ -57,14 +57,11 @@ define stage-template endef endif -stage0: always - $(call stage-template,0) - -%.o: stage0 +%.o: always $(call stage-template,1) #STAGE1_TARGETS includes all object files necessary for $(STAGE1) -stage1 $(STAGE1_TARGETS): stage0 +stage1 $(STAGE1_TARGETS): always $(call stage-template,1) %.cmo %.cmx %.cmi %.cma %.cmxa %.ml4.preprocessed: stage1 diff --git a/Makefile.build b/Makefile.build index 3887dfdec..38cdd53be 100644 --- a/Makefile.build +++ b/Makefile.build @@ -849,7 +849,7 @@ endif $(SHOW)'CCDEP $<' $(HIDE)$(CC) -MM -MG -MQ "$@" -MQ "$(<:.c=.o)" $(CFLAGS) $(CINCLUDES) $< > $@ -.PRECIOUS: %.ml %.mli %.d %.ml4.d kernel/copcodes.ml +.SECONDARY: $(GENFILES) ########################################################################### # this sets up developper supporting stuff diff --git a/Makefile.common b/Makefile.common index 8c14d2b9e..3bf6ae502 100644 --- a/Makefile.common +++ b/Makefile.common @@ -440,6 +440,7 @@ MLIFILES := $(shell find . '(' -name '*.mli' ')' -printf '%P\n') \ $(GENMLIFILES) ML4FILES := $(shell find . '(' -name '*.ml4' ')' -printf '%P\n') VFILES := $(shell find . '(' -name '*.v' ')' -printf '%P\n') +CFILES := $(shell find kernel/byterun -name '*.c' -printf '%p\n') ML4FILESML:= $(ML4FILES:.ml4=.ml) @@ -786,7 +787,7 @@ 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 \ - $(GRAMMARML4:.ml4=.ml4.preprocessed) + $(STAGE1_ML4:.ml4=.ml4.preprocessed) STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \ interp parsing pretyping highparsing toplevel hightactics \ coqide-binaries coqide-byte coqide-opt $(COQIDEOPT) $(COQIDEBYTE) $(COQIDE) \ diff --git a/Makefile.stage0 b/Makefile.stage0 deleted file mode 100644 index be1354320..000000000 --- a/Makefile.stage0 +++ /dev/null @@ -1,21 +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 - -.PHONY: stage0 -stage0: $(ML4FILES:.ml4=.ml4.d) - -##Somehow, make decides to delete the .ml4.d files if they are -include'd. -##This "stage0" hack to have them include'd, but no spurious error message -##on bootstrap. GNU Make bug suspected. - -# For emacs: -# Local Variables: -# mode: makefile -# End: diff --git a/Makefile.stage1 b/Makefile.stage1 index e08512206..a60d388fc 100644 --- a/Makefile.stage1 +++ b/Makefile.stage1 @@ -8,13 +8,21 @@ include Makefile.build -include $(ML4FILES:.ml4=.ml4.d) +# 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. +-include $(ML4FILES:.ml4=.ml4.d) +.SECONDARY: $(ML4FILES:.ml4=.ml4.d) -include $(MLFILES:.ml=.ml.d) +.SECONDARY: $(MLFILES:.ml=.ml.d) -include $(MLIFILES:.mli=.mli.d) +.SECONDARY: $(MLIFILES:.mli=.mli.d) ##Depends upon the fact that all .ml4.d for stage1 files are empty -include $(STAGE1_ML4:.ml4=.ml4.ml.d) --include parsing/q_constr.ml4.ml.d --include $(shell find kernel/byterun -name '*.c' -printf '%p.d\n') +.SECONDARY: $(STAGE1_ML4:.ml4=.ml4.ml.d) +-include $(CFILES:.c=.c.d) +.SECONDARY: $(CFILES:.c=.c.d) .PHONY: stage1 stage1: $(STAGE1) diff --git a/Makefile.stage2 b/Makefile.stage2 index 97a10118e..6fe020be9 100644 --- a/Makefile.stage2 +++ b/Makefile.stage2 @@ -9,6 +9,7 @@ include Makefile.stage1 -include $(ML4FILES:.ml4=.ml4.ml.d) +.SECONDARY: $(ML4FILES:.ml4=.ml4.ml.d) .PHONY: stage2 stage2: $(COQDEP) diff --git a/Makefile.stage3 b/Makefile.stage3 index f258ab298..1b9d880f0 100644 --- a/Makefile.stage3 +++ b/Makefile.stage3 @@ -9,6 +9,7 @@ include Makefile.stage2 -include $(VFILES:.v=.v.d) +.SECONDARY: $(VFILES:.v=.v.d) .PHONY: stage3 stage3: world diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt index 8fb036fc5..c825f088b 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -37,9 +37,6 @@ Le Makefile a été séparé en plusieurs fichiers : The build needs to be cut in stages because make will not take into account one include when making another include. -Because a weird not completely understood situation, there is actually -a stage0, see the comment in Makefile.stage0. - Parallélisation --------------- |