diff options
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | Makefile.build | 12 | ||||
| -rw-r--r-- | dev/doc/build-system.txt | 3 |
3 files changed, 2 insertions, 14 deletions
@@ -26,7 +26,6 @@ # # 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 # diff --git a/Makefile.build b/Makefile.build index 9d9f08ea07..bea461131c 100644 --- a/Makefile.build +++ b/Makefile.build @@ -67,7 +67,6 @@ ALLDEPS:=$(addsuffix .d, \ VERBOSE= NO_RECOMPILE_ML4= -NO_RECOMPILE_LIB= NO_RECALC_DEPS= READABLE_ML4= # non-empty means .ml of .ml4 will be ascii instead of binary VALIDATE= @@ -151,13 +150,6 @@ endif ifdef VALIDATE VO_TOOLS_DEP += $(CHICKEN) 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 ifdef NO_RECALC_DEPS D_DEPEND_BEFORE_SRC:=| @@ -471,7 +463,7 @@ pluginsopt: $(PLUGINSOPT) # rules to make theories and plugins ########################################################################### -theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_STRICT) | theories/Init/%.v.d $(VO_TOOLS_ORDER_ONLY) +theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/%.v.d $(SHOW)'COQC -noinit $<' $(HIDE)rm -f theories/Init/$*.glob $(HIDE)$(BOOTCOQC) theories/Init/$* -noinit @@ -894,7 +886,7 @@ plugins/%_mod.ml: plugins/%.mllib $(CAMLP4O) $(PR_O) -I $(CAMLLIB) tools/compat5.cmo $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@; \ else echo $< : Dependency $${DEPS} not ready yet; false; fi -%.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_STRICT) | %.v.d $(VO_TOOLS_ORDER_ONLY) +%.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d $(SHOW)'COQC $<' $(HIDE)rm -f $*.glob $(HIDE)$(BOOTCOQC) $* diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index b243ebe2ed..d7cf396ff5 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -108,9 +108,6 @@ save precious time: like that. This will avoid entering the stage 3, and cut build system overhead by 50% (1.2s instead of 2.4 on writer's machine). - - You can turn off rebuilding of the standard library each time - bin/coqtop is rebuilt with NO_RECOMPILE_LIB=1. - - If you want to avoid all .ml4 files being recompiled only because grammar.cma was rebuilt, do "make ml4depclean" once and then use NO_RECOMPILE_ML4=1. |