diff options
| -rw-r--r-- | Makefile.build | 49 | ||||
| -rw-r--r-- | Makefile.common | 2 | ||||
| -rw-r--r-- | Makefile.ide | 2 | ||||
| -rw-r--r-- | dev/doc/build-system.txt | 2 | ||||
| -rw-r--r-- | grammar/compat5.ml (renamed from tools/compat5.ml) | 0 | ||||
| -rw-r--r-- | grammar/compat5.mlp (renamed from tools/compat5.mlp) | 0 | ||||
| -rw-r--r-- | grammar/compat5b.mlp (renamed from tools/compat5b.mlp) | 0 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 6 |
8 files changed, 29 insertions, 32 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 $@ diff --git a/Makefile.common b/Makefile.common index e156b101c..310e30a0c 100644 --- a/Makefile.common +++ b/Makefile.common @@ -88,7 +88,7 @@ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma -GRAMMARCMA:=tools/compat5.cmo grammar/grammar.cma +GRAMMARCMA:=grammar/compat5.cmo grammar/grammar.cma # modules known by the toplevel of Coq diff --git a/Makefile.ide b/Makefile.ide index c50e42341..21821bfea 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -96,7 +96,7 @@ $(COQIDEBYTE): $(LINKIDE) ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@ + $(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@ ide/%.cmi: ide/%.mli diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index 4593a6ad5..873adc1b2 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -117,7 +117,7 @@ Targets for cleaning various parts: --------------- There is now two kinds of preprocessed files : - - a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp) + - a .mlp do not need grammar.cma (they are in grammar/) - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo), except coqide_main.ml4 and its specific rule diff --git a/tools/compat5.ml b/grammar/compat5.ml index 33c1cd602..33c1cd602 100644 --- a/tools/compat5.ml +++ b/grammar/compat5.ml diff --git a/tools/compat5.mlp b/grammar/compat5.mlp index 8473a1fb7..8473a1fb7 100644 --- a/tools/compat5.mlp +++ b/grammar/compat5.mlp diff --git a/tools/compat5b.mlp b/grammar/compat5b.mlp index 46802a825..46802a825 100644 --- a/tools/compat5b.mlp +++ b/grammar/compat5b.mlp diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 45e843e60..65b2441f7 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -532,11 +532,11 @@ let variables is_install opt (args,defs) = print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n"; print "GRAMMARS?=grammar.cma\n"; print "ifeq ($(CAMLP4),camlp5) -CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma +CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo else -CAMLP4EXTEND=threads.cma +CAMLP4EXTEND= endif\n"; - print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)/threads/ $(COQSRCLIBS) compat5.cmo \\ + print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\ $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; end; match is_install with |