diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | Makefile.build | 25 | ||||
| -rw-r--r-- | Makefile.dev | 2 | ||||
| -rw-r--r-- | Makefile.doc | 2 | ||||
| -rw-r--r-- | Makefile.ide | 2 | ||||
| -rw-r--r-- | Makefile.vofiles | 27 |
6 files changed, 45 insertions, 15 deletions
@@ -268,7 +268,7 @@ cleanconfig: distclean: clean cleanconfig cacheclean timingclean voclean: - find theories plugins test-suite \( -name '*.vo' -o -name '*.glob' -o -name "*.cmxs" \ + find theories plugins test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.glob' -o -name "*.cmxs" \ -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -exec rm -f {} + find theories plugins test-suite -name .coq-native -empty -exec rm -rf {} + diff --git a/Makefile.build b/Makefile.build index 34d7ce42f7..b4be233faf 100644 --- a/Makefile.build +++ b/Makefile.build @@ -57,6 +57,9 @@ TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line BEFORE ?= AFTER ?= +# Number of parallel jobs for -schedule-vio2vo +NJOBS ?= 2 + ########################################################################### # Default starting rule ########################################################################### @@ -543,7 +546,7 @@ $(CSDPCERTBYTE): $(CSDPCERTCMO) VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m -validate: $(CHICKEN) | $(ALLVO) +validate: $(CHICKEN) | $(ALLVO:.$(VO)=.vo) $(SHOW)'COQCHK <theories & plugins>' $(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS) @@ -779,13 +782,21 @@ $(PLUGMLLIBDFILE).d: $(D_DEPEND_BEFORE_SRC) $(filter plugins/%, $(MLLIBFILES) $( # since they are all mentioned in at least one Declare ML Module in some .v coqlib: theories plugins +ifdef QUICK + $(SHOW)'COQC -schedule-vio2vo $(NJOBS) theories/**.vio plugins/**.vio' + $(HIDE)$(BOOTCOQC:-compile=-schedule-vio2vo) $(NJOBS) \ + $(THEORIESVO) $(PLUGINSVO) + @# this should be done by -schedule-vio2vo, see #9334 + $(HIDE)touch $(THEORIESVO:.$(VO)=.vo) $(PLUGINSVO:.$(VO)=.vo) +endif + coqlib.timing.diff: theories.timing.diff plugins.timing.diff theories: $(THEORIESVO) plugins: $(PLUGINSVO) -theories.timing.diff: $(THEORIESVO:.vo=.v.timing.diff) -plugins.timing.diff: $(PLUGINSVO:.vo=.v.timing.diff) +theories.timing.diff: $(THEORIESVO:.$(VO)=.v.timing.diff) +plugins.timing.diff: $(PLUGINSVO:.$(VO)=.v.timing.diff) .PHONY: coqlib theories plugins coqlib.timing.diff theories.timing.diff plugins.timing.diff @@ -802,6 +813,10 @@ theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) $(HIDE)rm -f theories/Init/$*.glob $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq $(TIMING_ARG) $(TIMING_EXTRA) +theories/Init/%.vio: theories/Init/%.v $(VO_TOOLS_DEP) + $(SHOW)'COQC -quick -noinit $<' + $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq -quick -noglob + # The general rule for building .vo files : %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) @@ -814,6 +829,10 @@ ifdef VALIDATE || ( RV=$$?; rm -f "$@"; exit $${RV} ) endif +%.vio: %.v theories/Init/Prelude.vio $(VO_TOOLS_DEP) + $(SHOW)'COQC -quick $<' + $(HIDE)$(BOOTCOQC) $< -quick -noglob + %.v.timing.diff: %.v.before-timing %.v.after-timing $(SHOW)PYTHON TIMING-DIFF $< $(HIDE)$(MAKE) --no-print-directory print-pretty-single-time-diff BEFORE=$*.v.before-timing AFTER=$*.v.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" diff --git a/Makefile.dev b/Makefile.dev index 9659f602d7..13b85dfad4 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -63,7 +63,7 @@ revision: coqlight: theories-light tools coqbinaries -states: theories/Init/Prelude.vo +states: theories/Init/Prelude.$(VO) miniopt: $(COQTOPEXE) pluginsopt minibyte: $(COQTOPBYTE) pluginsbyte diff --git a/Makefile.doc b/Makefile.doc index 9e6ec4955a..db60189870 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -137,7 +137,7 @@ else doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO) endif $(COQDOC) -q -boot --gallina --body-only --latex --stdout \ - -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@ + -R theories Coq $(THEORIESLIGHTVO:.$(VO)=.v) >> $@ doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex (cd doc/stdlib;\ diff --git a/Makefile.ide b/Makefile.ide index cae77ee348..23ce83d263 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -70,7 +70,7 @@ SOURCEVIEWSHARE=$(shell pkg-config --variable=prefix gtksourceview-2.0)/share .PHONY: ide-toploop ide-byteloop ide-optloop # target to build CoqIde (native version) and the stuff needed to lauch it -coqide: coqide-files coqide-opt theories/Init/Prelude.vo +coqide: coqide-files coqide-opt theories/Init/Prelude.$(VO) # target to build CoqIde (in native and byte versions), and no more # NB: this target is used in the opam package coq-coqide diff --git a/Makefile.vofiles b/Makefile.vofiles index d0ae317335..d5217ef4b7 100644 --- a/Makefile.vofiles +++ b/Makefile.vofiles @@ -2,14 +2,20 @@ # This file calls [find] and as such is not suitable for inclusion in # the test suite Makefile, unlike Makefile.common. +ifdef QUICK +VO=vio +else +VO=vo +endif + ########################################################################### # vo files ########################################################################### -THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v")) -PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v")) +THEORIESVO := $(patsubst %.v,%.$(VO),$(shell find theories -type f -name "*.v")) +PLUGINSVO := $(patsubst %.v,%.$(VO),$(shell find plugins -type f -name "*.v")) ALLVO := $(THEORIESVO) $(PLUGINSVO) -VFILES := $(ALLVO:.vo=.v) +VFILES := $(ALLVO:.$(VO)=.v) ## More specific targets @@ -20,22 +26,27 @@ THEORIESLIGHTVO:= \ # remove .vo, replace theories and plugins by Coq, and replace slashes by dots vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=)))) -ALLMODS:=$(call vo_to_mod,$(ALLVO)) +ALLMODS:=$(call vo_to_mod,$(ALLVO:.$(VO)=.vo)) # Converting a stdlib filename into native compiler filenames # Used for install targets -vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*))))) +vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.cm*))))) -vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o))))) +vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.o))))) + +ifdef QUICK +GLOBFILES:= +else +GLOBFILES:=$(ALLVO:.$(VO)=.glob) +endif -GLOBFILES:=$(ALLVO:.vo=.glob) ifdef NATIVECOMPUTE NATIVEFILES := $(call vo_to_cm,$(ALLVO)) $(call vo_to_obj,$(ALLVO)) else NATIVEFILES := endif -LIBFILES:=$(ALLVO) $(NATIVEFILES) $(VFILES) $(GLOBFILES) +LIBFILES:=$(ALLVO:.$(VO)=.vo) $(NATIVEFILES) $(VFILES) $(GLOBFILES) # For emacs: # Local Variables: |