diff options
-rw-r--r-- | doc/refman/RefMan-uti.tex | 8 | ||||
-rw-r--r-- | test-suite/coq-makefile/only/_CoqProject | 11 | ||||
-rwxr-xr-x | test-suite/coq-makefile/only/run.sh | 12 | ||||
-rw-r--r-- | tools/CoqMakefile.in | 3 |
4 files changed, 34 insertions, 0 deletions
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 104d7cd9e..08cdbee50 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -132,6 +132,14 @@ as in {\tt make -f Makefile target} from another Makefile. {\tt CoqMakefile.local} \end{itemize} +\paragraph{Note: building a subset of the targets with -j} + +To build, say, two targets \texttt{foo.vo} and \texttt{bar.vo} +in parallel one can use \texttt{make only TGTS="foo.vo bar.vo" -j}. + +Note that \texttt{make foo.vo bar.vo -j} has a different meaning for +the make utility, in particular it may build a shared prerequisite twice. + \section[Modules dependencies]{Modules dependencies\label{Dependencies}\index{Dependencies} \ttindex{coqdep}} diff --git a/test-suite/coq-makefile/only/_CoqProject b/test-suite/coq-makefile/only/_CoqProject new file mode 100644 index 000000000..357384fdd --- /dev/null +++ b/test-suite/coq-makefile/only/_CoqProject @@ -0,0 +1,11 @@ +-R theories/ test +-R src/ test +-I src/ + +./src/test_plugin.mlpack +./src/test.ml4 +./src/test.mli +./src/test_aux.ml +./src/test_aux.mli +./theories/test.v +./theories/sub/testsub.v diff --git a/test-suite/coq-makefile/only/run.sh b/test-suite/coq-makefile/only/run.sh new file mode 100755 index 000000000..4b471bcb8 --- /dev/null +++ b/test-suite/coq-makefile/only/run.sh @@ -0,0 +1,12 @@ +#!/bin/sh + +#set -x +set -e + +. ../template/init.sh + +coq_makefile -f _CoqProject -o Makefile +make only TGTS="src/test.cmi src/test_aux.cmi" -j2 +test -f src/test.cmi +test -f src/test_aux.cmi +! test -f src/test.cmo diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 1de7a5c24..fdcd2ed79 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -278,6 +278,9 @@ validate: $(VOFILES) $(COQCHK) $(COQCHKFLAGS) $(notdir $(^:.vo=)) .PHONY: validate +only: $(TGTS) +.PHONY: only + # Documentation targets ####################################################### html: $(GLOBFILES) $(VFILES) |