diff options
Diffstat (limited to 'tools/CoqMakefile.in')
| -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 ca02c983d..a426c3cb2 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -381,7 +381,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 @@ -390,6 +390,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) |