diff options
| author | letouzey | 2012-09-20 17:25:20 +0000 |
|---|---|---|
| committer | letouzey | 2012-09-20 17:25:20 +0000 |
| commit | ac98362d168bc96433bf09ced8ee992bce76483e (patch) | |
| tree | 386b04b0310a96bd05488741b7da0b69d1286561 | |
| parent | 5e8ebbc13909125093e2c7aa18e00cf30cad6362 (diff) | |
Remove broken makefile option NO_RECOMPILE_LIB
The idea was to allow rebuilding coqtop without the whole stdlib,
but it's not working anymore since the stdlib also depends on
plugins .cmxs, hence its compilation will be triggered anyway.
Since I've no idea how to restore the old behavior (except via
hacking the output of coqdep with more ORDER_ONLY hack), I simply
declare this option dead, and remove it for improving clarity.
NB: an imperfect workaround is to touch all the .vo after rebuilding
coqtop and the plugins...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15823 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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. |