diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-08 14:26:00 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-07 02:56:18 +0200 |
| commit | 633e40b6f925556e94347c348a2804cdc1068d88 (patch) | |
| tree | b8063831a6a2ca60cf45d903dedf11f83b308fe5 /Makefile.build | |
| parent | 1d0eb5d4d6fea88abc29798ee2004b2e27e952c6 (diff) | |
[camlpX] Enrico's changes to camlp4 removal.
This removes some remaining support for camlp4 in the infrastructure
and documents the change.
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 44 |
1 files changed, 5 insertions, 39 deletions
diff --git a/Makefile.build b/Makefile.build index eeb648ba1..56f1fb8b4 100644 --- a/Makefile.build +++ b/Makefile.build @@ -146,14 +146,10 @@ $(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) $(LINKMETADATA) -o $@ $(1) $(addsuffix .cm $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ $(1) $(addsuffix .cma,$(2)) $^) endef -# Camlp4 / Camlp5 settings +# Camlp5 settings CAMLP4DEPS:=grammar/compat5.cmo grammar/grammar.cma -ifeq ($(CAMLP4),camlp5) CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) -else -CAMLP4USE=-D$(CAMLVERSION) -endif PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) @@ -162,11 +158,7 @@ SYSCMA:=$(addsuffix .cma,$(SYSMOD)) SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD)) # We do not repeat the dependencies already in SYSMOD here -ifeq ($(CAMLP4),camlp5) P4CMA:=gramlib.cma -else -P4CMA:=camlp4lib.cma -endif ########################################################################### # Infrastructure for the rest of the Makefile @@ -243,26 +235,6 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h $(HIDE)$(OCAMLC) -ccopt "-MM -MQ $@ -MQ $(<:.c=.o) -isystem $(CAMLHLIB)" $< $(TOTARGET) ########################################################################### -### Special rules (Camlp5 / Camlp4) -########################################################################### - -# Special rule for the compatibility-with-camlp5 extension for camlp4 -# -# - grammar/compat5.cmo changes 'GEXTEND' into 'EXTEND'. Safe, always loaded -# - grammar/compat5b.cmo changes 'EXTEND' into 'EXTEND Gram'. Interact badly with -# syntax such that 'VERNAC EXTEND', we only load it in grammar/ - -ifeq ($(CAMLP4),camlp4) -grammar/compat5.cmo: grammar/compat5.mlp - $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -I $(MYCAMLP4LIB) -impl' -impl $< -grammar/compat5b.cmo: grammar/compat5b.mlp - $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -I $(MYCAMLP4LIB) -impl' -impl $< -else -grammar/compat5.cmo: grammar/compat5.ml - $(OCAMLC) -c $< -endif - -########################################################################### # grammar/grammar.cma ########################################################################### @@ -299,15 +271,9 @@ grammar/grammar.cma : $(GRAMCMO) ## Support of Camlp5 and Camlp5 -ifeq ($(CAMLP4),camlp4) - COMPATCMO:=grammar/compat5.cmo grammar/compat5b.cmo - GRAMP4USE:=$(COMPATCMO) -D$(CAMLVERSION) - GRAMPP:=$(CAMLP4O) -I $(MYCAMLP4LIB) $(GRAMP4USE) $(CAMLP4COMPAT) -impl -else - COMPATCMO:= - GRAMP4USE:=$(COMPATCMO) pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) - GRAMPP:=$(CAMLP4O) -I $(MYCAMLP4LIB) $(GRAMP4USE) $(CAMLP4COMPAT) -impl -endif +COMPATCMO:= +GRAMP4USE:=$(COMPATCMO) pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) +GRAMPP:=$(CAMLP4O) -I $(MYCAMLP4LIB) $(GRAMP4USE) $(CAMLP4COMPAT) -impl ## Rules for standard .mlp and .mli files in grammar/ @@ -597,7 +563,7 @@ plugins/%.cmx: plugins/%.ml $(HIDE)$(OCAMLLEX) -o $@ "$*.mll" %.ml: %.ml4 $(CAMLP4DEPS) - $(SHOW)'CAMLP4O $<' + $(SHOW)'CAMLP5O $<' $(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $(PR_O) \ $(CAMLP4DEPS) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@ |