diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 45 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 2 |
2 files changed, 27 insertions, 20 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index ca02c983d2..727fd3ec37 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) @@ -169,7 +168,8 @@ endif COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) COQCHKFLAGS?=-silent -o $(COQLIBS) -COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML) +COQDOCFLAGS?=-interpolate -utf8 +COQDOCLIBS?=$(COQLIBS_NOML) # The version of Coq being run and the version of coq_makefile that # generated this makefile @@ -178,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)) @@ -381,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 @@ -390,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) @@ -739,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)' diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 091869407e..1e1862220b 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -124,7 +124,7 @@ let read_whole_file s = close_in ic; Buffer.contents b -let quote s = if String.contains s ' ' then "'" ^ s ^ "'" else s +let quote s = if String.contains s ' ' || CString.is_empty s then "'" ^ s ^ "'" else s let generate_makefile oc conf_file local_file args project = let makefile_template = |