diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-15 10:38:11 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-15 10:38:11 +0100 |
| commit | 8dd6d091ffbfa237f7266eeca60187263a9b521f (patch) | |
| tree | 7b0c9acf940698b7e04eaebbc640c346dab24649 /tools | |
| parent | a87fc2f9c400919cf37e4e74eb79ce65739eaa9c (diff) | |
| parent | 999a7059840bdfbdc46ce198e1a16b8621f93588 (diff) | |
Merge PR #1073: new quick2vo target: like vio2vo, but smarter
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 173eaae89..23212ef84 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -382,7 +382,7 @@ bytefiles: $(CMOFILES) $(CMAFILES) optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) .PHONY: optfiles -# FIXME, see Ralph's bugreport +# FIXME, see Ralf's bugreport quick: $(VOFILES:.vo=.vio) .PHONY: quick @@ -391,6 +391,18 @@ vio2vo: -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) .PHONY: vio2vo +quick2vo: + $(HIDE)make -j $(J) quick + $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ + viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ + if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ + done); \ + echo "VIO2VO: $$VIOFILES"; \ + if [ -n "$$VIOFILES" ]; then \ + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; \ + fi +.PHONY: quick2vo + checkproofs: $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \ -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) |