diff options
Diffstat (limited to 'tools/CoqMakefile.in')
| -rw-r--r-- | tools/CoqMakefile.in | 42 |
1 files changed, 24 insertions, 18 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 173eaae89..727fd3ec3 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -34,11 +34,10 @@ LOCAL := $(COQMF_LOCAL) COQLIB := $(COQMF_COQLIB) DOCDIR := $(COQMF_DOCDIR) OCAMLFIND := $(COQMF_OCAMLFIND) -CAMLP4 := $(COQMF_CAMLP4) -CAMLP4O := $(COQMF_CAMLP4O) -CAMLP4BIN := $(COQMF_CAMLP4BIN) -CAMLP4LIB := $(COQMF_CAMLP4LIB) -CAMLP4OPTIONS := $(COQMF_CAMLP4OPTIONS) +CAMLP5O := $(COQMF_CAMLP5O) +CAMLP5BIN := $(COQMF_CAMLP5BIN) +CAMLP5LIB := $(COQMF_CAMLP5LIB) +CAMLP5OPTIONS := $(COQMF_CAMLP5OPTIONS) CAMLFLAGS := $(COQMF_CAMLFLAGS) HASNATDYNLINK := $(COQMF_HASNATDYNLINK) @@ -179,24 +178,20 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") -CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP5LIB) # ocamldoc fails with unknown argument otherwise CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) # FIXME This should be generated by Coq GRAMMARS:=grammar.cma -ifeq ($(CAMLP4),camlp5) -CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo -else -CAMLP4EXTEND= -endif +CAMLP5EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null) ifeq (,$(CAMLLIB)) PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.") else -PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' +PP:=-pp '$(CAMLP5O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP5EXTEND) $(GRAMMARS) $(CAMLP5OPTIONS) -impl' endif ifneq (,$(TIMING)) @@ -382,7 +377,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 +386,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) @@ -740,11 +747,10 @@ printenv:: @echo 'COQLIB = $(COQLIB)' @echo 'DOCDIR = $(DOCDIR)' @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'CAMLP4 = $(CAMLP4)' - @echo 'CAMLP4O = $(CAMLP4O)' - @echo 'CAMLP4BIN = $(CAMLP4BIN)' - @echo 'CAMLP4LIB = $(CAMLP4LIB)' - @echo 'CAMLP4OPTIONS = $(CAMLP4OPTIONS)' + @echo 'CAMLP5O = $(CAMLP5O)' + @echo 'CAMLP5BIN = $(CAMLP5BIN)' + @echo 'CAMLP5LIB = $(CAMLP5LIB)' + @echo 'CAMLP5OPTIONS = $(CAMLP5OPTIONS)' @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' |