diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-21 19:34:51 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-21 20:35:36 +0200 |
| commit | 39861a12445742b481496baf2caafeb391773aba (patch) | |
| tree | 8e38399836572cf13947d28c4ebd6eb4e2ca4240 /Makefile.build | |
| parent | a1a86e6572bbae9e515cc72d7072322e5a11b49e (diff) | |
Makefile: compat5* moved in grammar/, less -I given to camlp4o
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 49 |
1 files changed, 23 insertions, 26 deletions
diff --git a/Makefile.build b/Makefile.build index 2a2eb8796..3a24d8dbc 100644 --- a/Makefile.build +++ b/Makefile.build @@ -138,15 +138,13 @@ endef # Camlp4 / Camlp5 settings -CAMLP4DEPS:=tools/compat5.cmo grammar/grammar.cma +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 -CAMLP4FLAGS=-I $(CAMLLIB) -I $(CAMLLIB)/threads -I $(MYCAMLP4LIB) unix.cma threads.cma - PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) # works also with new camlp4 SYSMOD:=str unix dynlink threads @@ -233,6 +231,26 @@ 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 ########################################################################### @@ -270,13 +288,8 @@ grammar/grammar.cma : $(GRAMCMO) ## Support of Camlp5 and Camlp5 -# NB: compatibility modules for camlp4: -# - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded -# - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with -# syntax such that VERNAC EXTEND, we only load it in grammar/ - ifeq ($(CAMLP4),camlp4) - COMPATCMO:=tools/compat5.cmo tools/compat5b.cmo + COMPATCMO:=grammar/compat5.cmo grammar/compat5b.cmo GRAMP4USE:=$(COMPATCMO) -D$(CAMLVERSION) GRAMPP:=$(CAMLP4O) -I $(MYCAMLP4LIB) $(GRAMP4USE) $(CAMLP4COMPAT) -impl else @@ -465,22 +478,6 @@ test-suite: world $(ALLSTDLIB).v $(MAKE) $(MAKE_TSOPTS) report ########################################################################### -### Special rules (Camlp5 / Camlp4) -########################################################################### - -# Special rule for the compatibility-with-camlp5 extension for camlp4 - -ifeq ($(CAMLP4),camlp4) -tools/compat5.cmo: tools/compat5.mlp - $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $< -tools/compat5b.cmo: tools/compat5b.mlp - $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $< -else -tools/compat5.cmo: tools/compat5.ml - $(OCAMLC) -c $< -endif - -########################################################################### # Default rules for compiling ML code ########################################################################### @@ -581,7 +578,7 @@ endif %.ml: %.ml4 | $(CAMLP4DEPS) $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) \ + $(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $(PR_O) \ $(CAMLP4DEPS) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@ |