From 39861a12445742b481496baf2caafeb391773aba Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 21 Jun 2016 19:34:51 +0200 Subject: Makefile: compat5* moved in grammar/, less -I given to camlp4o --- Makefile.build | 49 +++++++++++++++++++++++------------------------- Makefile.common | 2 +- Makefile.ide | 2 +- dev/doc/build-system.txt | 2 +- grammar/compat5.ml | 13 +++++++++++++ grammar/compat5.mlp | 23 +++++++++++++++++++++++ grammar/compat5b.mlp | 23 +++++++++++++++++++++++ tools/compat5.ml | 13 ------------- tools/compat5.mlp | 23 ----------------------- tools/compat5b.mlp | 23 ----------------------- tools/coq_makefile.ml | 6 +++--- 11 files changed, 88 insertions(+), 91 deletions(-) create mode 100644 grammar/compat5.ml create mode 100644 grammar/compat5.mlp create mode 100644 grammar/compat5b.mlp delete mode 100644 tools/compat5.ml delete mode 100644 tools/compat5.mlp delete mode 100644 tools/compat5b.mlp 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 @@ -232,6 +230,26 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h $(SHOW)'CCDEP $<' $(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 @@ -464,22 +477,6 @@ test-suite: world $(ALLSTDLIB).v $(MAKE) $(MAKE_TSOPTS) all $(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/grammar/compat5.ml b/grammar/compat5.ml new file mode 100644 index 000000000..33c1cd602 --- /dev/null +++ b/grammar/compat5.ml @@ -0,0 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ] -> + [< '(KEYWORD "EXTEND", loc); my_token_filter s >] + | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >] + | [< >] -> [< >] + +let _ = + Token.Filter.define_filter (Gram.get_filter()) + (fun prev strm -> prev (my_token_filter strm)) diff --git a/grammar/compat5b.mlp b/grammar/compat5b.mlp new file mode 100644 index 000000000..46802a825 --- /dev/null +++ b/grammar/compat5b.mlp @@ -0,0 +1,23 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ] -> + [< 't; '(UIDENT "Gram", Loc.ghost); my_token_filter s >] + | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >] + | [< >] -> [< >] + +let _ = + Token.Filter.define_filter (Gram.get_filter()) + (fun prev strm -> prev (my_token_filter strm)) diff --git a/tools/compat5.ml b/tools/compat5.ml deleted file mode 100644 index 33c1cd602..000000000 --- a/tools/compat5.ml +++ /dev/null @@ -1,13 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ] -> - [< '(KEYWORD "EXTEND", loc); my_token_filter s >] - | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >] - | [< >] -> [< >] - -let _ = - Token.Filter.define_filter (Gram.get_filter()) - (fun prev strm -> prev (my_token_filter strm)) diff --git a/tools/compat5b.mlp b/tools/compat5b.mlp deleted file mode 100644 index 46802a825..000000000 --- a/tools/compat5b.mlp +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ] -> - [< 't; '(UIDENT "Gram", Loc.ghost); my_token_filter s >] - | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >] - | [< >] -> [< >] - -let _ = - Token.Filter.define_filter (Gram.get_filter()) - (fun prev strm -> prev (my_token_filter strm)) 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 -- cgit v1.2.3