From 481bc97bfccd2ebd677da191a1e1e69fd4bbc70c Mon Sep 17 00:00:00 2001 From: lmamane Date: Wed, 18 Jul 2007 00:10:08 +0000 Subject: Makefile: more robustness all around - Make sure make notices when a command fails - don't leave behind half-baked output files of commands that failed git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10016 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.build | 55 +++++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 39 insertions(+), 16 deletions(-) diff --git a/Makefile.build b/Makefile.build index ad14d2098..3e92347e5 100644 --- a/Makefile.build +++ b/Makefile.build @@ -136,13 +136,14 @@ $(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN) kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \ -e '/^}/q' kernel/byterun/coq_instruct.h > \ - kernel/byterun/coq_jumptbl.h - + kernel/byterun/coq_jumptbl.h \ + || ( RV=$$?; rm -f "$@"; exit $${RV} ) kernel/copcodes.ml: kernel/byterun/coq_instruct.h sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' \ kernel/byterun/coq_instruct.h | \ - awk -f kernel/make-opcodes > kernel/copcodes.ml + awk -f kernel/make-opcodes > kernel/copcodes.ml \ + || ( RV=$$?; rm -f "$@"; exit $${RV} ) ########################################################################### @@ -524,7 +525,7 @@ theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_STRICT) | # globalizations (for coqdoc) glob.dump: $(THEORIESVO:.vo=.glob) $(CONTRIBVO:.vo=.glob) - cat $^ > "$@" + cat $^ > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) ########################################################################### # tools @@ -702,11 +703,13 @@ toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml4.ml.d toplevel/mlto ## In other words, the Byte-only code doesn't import a new module. toplevel/mltop.byteml: toplevel/mltop.ml4 # no camlp4deps here $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo -DByte -impl $< > $@ + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo -DByte -impl $< > $@ \ + || ( RV=$$?; rm -f "$@"; exit $${RV} ) toplevel/mltop.optml: toplevel/mltop.ml4 # no camlp4deps here $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo -impl $< > $@ + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo -impl $< > $@ \ + || ( RV=$$?; rm -f "$@"; exit $${RV} ) # files compiled with -rectypes @@ -797,7 +800,8 @@ endif %.ml4.preprocessed: %.ml4 | %.ml4.d $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ \ + || ( RV=$$?; rm -f "$@"; exit $${RV} ) %.vo %.glob: %.v states/initial.coq $(VO_TOOLS_STRICT) | %.v.d $(VO_TOOLS_ORDER_ONLY) $(SHOW)'COQC $<' @@ -812,14 +816,16 @@ endif # NOT to generate object code. %.ml4.d: %.ml4 $(SHOW)'CAMLP4DEPS $<' - $(HIDE)( echo -n '$*.cmo $*.cmx $*.ml4.ml.d: ' && $(CAMLP4DEPS) "$<" ) > "$@" + $(HIDE)( echo -n '$*.cmo $*.cmx $*.ml4.ml.d: ' && $(CAMLP4DEPS) "$<" ) > "$@" \ + || ( RV=$$?; rm -f "$@"; exit $${RV} ) %.ml4.ml.d: %.ml4 | $(GENFILES) $(ML4FILES:.ml4=.ml) %.ml4.d #Critical section: # Nobody (in a make -j) should touch the .ml file here. $(SHOW)'OCAMLDEP4 $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $*.ml - $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $*.ml > "$@" + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4USE) $<` pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $*.ml \ + || ( RV=$$?; rm -f "$*.ml"; exit $${RV} ) + $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $*.ml > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) $(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" > $*.ml #End critical section @@ -834,16 +840,33 @@ endif ## Veerry nasty hack to keep ocamldep happy %.ml: | %.ml4 $(SHOW)'TOUCH $@' - $(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" > $@ - -%.v.d: %.v | $(COQDEP) + $(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" > $@ \ + || ( RV=$$?; rm -f "$@"; exit $${RV} ) + +# Another nasty hack. The making of .v.d files is split in two so that +# make notices if coqdep fails (returns an error exit code). If we +# just make %.v.d directly from %.v with +# $(HIDE)$(COQDEP) -coqlib . -R theories Coq -R contrib Coq $(COQINCLUDES) \ +# "$<" | sed 's/\(.*\)\.vo[[:space:]]*:/\1.vo \1.glob:/' > "$@" +# then the exit code of the whole pipe is the exit code of ... sed, +# that is always 0. And make doesn't notice that coqdep failed and +# merrily accepts that the .v.d file is just empty. +# We could also make a complex shell script with ERR trapping and all +# that, but more complex and fragile than this. +# make will delete .raw files because they are intermediate. +%.v.d.raw: %.v | $(COQDEP) $(SHOW)'COQDEP $<' - $(HIDE)$(COQDEP) -coqlib . -R theories Coq -R contrib Coq $(COQINCLUDES) \ - "$<" | sed 's/\(.*\)\.vo[[:space:]]*:/\1.vo \1.glob:/' > "$@" + $(HIDE)$(COQDEP) -coqlib . -R theories Coq -R contrib Coq $(COQINCLUDES) "$<" > "$@" \ + || ( RV=$$?; rm -f "$@"; exit $${RV} ) + +%.v.d: %.v.d.raw + $(HIDE)sed 's/\(.*\)\.vo[[:space:]]*:/\1.vo \1.glob:/' < "$<" > "$@" \ + || ( RV=$$?; rm -f "$@"; exit $${RV} ) %.c.d: %.c | $(GENHFILES) $(SHOW)'CCDEP $<' - $(HIDE)$(CC) -MM -MQ "$@" -MQ "$(<:.c=.o)" $(CFLAGS) $(CINCLUDES) $< > $@ + $(HIDE)$(CC) -MM -MQ "$@" -MQ "$(<:.c=.o)" $(CFLAGS) $(CINCLUDES) $< > $@ \ + || ( RV=$$?; rm -f "$@"; exit $${RV} ) ## The GENFILES and ML4FILESML files need to be secondary, else they ## get deleted by make after the dependencies get generated. This may -- cgit v1.2.3