diff options
| author |  Ralf Jung <post@ralfj.de> | 2017-09-20 12:59:38 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-15 10:37:19 +0100 |
| commit | 8dc97f734f90f50980b636e2c0c8de34d20a5843 (patch) | |
| tree | 7b62c26a8c3ac202601f54e4d6aaf34a72169043 /tools | |
| parent | 47e43e229ab02a4dedc2405fed3960a4bf476b58 (diff) | |
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 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) |