X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FMakefile;h=94ea279bd628bba032e464e5c53f52c2256b933b;hb=8aaf525856e25bcd8f355e505fd00f45c62bc18f;hp=ec24a4f4d6610ae3a9ba43d471b4b06b2bd9c07c;hpb=0d853dfc19b683f5d37741df405a2db721f7221a;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile index ec24a4f4d..94ea279bd 100644 --- a/helm/ocaml/cic_disambiguation/Makefile +++ b/helm/ocaml/cic_disambiguation/Makefile @@ -2,12 +2,13 @@ PACKAGE = cic_textual_parser2 REQUIRES = \ helm-tactics helm-logger helm-cic_unification helm-cic_transformations \ - ulex pxp camlp4.gramlib + helm-utf8_macros \ + ulex NOTATIONS = logic arit tex +# NOTATIONS = logic arit INTERFACE_FILES = \ disambiguateTypes.mli \ disambiguateChoices.mli \ - macro.mli \ cicTextualLexer2.mli \ cicTextualParser2.mli \ disambiguate.mli @@ -15,57 +16,37 @@ IMPLEMENTATION_FILES = \ $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \ $(patsubst %,%_notation.ml,$(NOTATIONS)) -ULEXDIR := $(shell ocamlfind query ulex) - -LEXER_P4_OPTS = -I $(ULEXDIR) pa_ulex.cma -PARSER_P4_OPTS = pa_extend.cmo ./macro.cmo ./pa_unicode_macro.cmo -PA_P4_OPTS = q_MLast.cmo pa_extend.cmo - -all: +all: test_lexer test_parser cicTextualLexer2.cmo: cicTextualLexer2.ml - $(OCAMLC) -pp "camlp4o $(LEXER_P4_OPTS)" -c $< -cicTextualParser2.cmo: cicTextualParser2.ml macro.cmo pa_unicode_macro.cmo - $(OCAMLC) -pp "camlp4o $(PARSER_P4_OPTS)" -c $< + $(OCAMLC_P4) -c $< +cicTextualParser2.cmo: cicTextualParser2.ml + $(OCAMLC_P4) -c $< cicTextualLexer2.cmx: cicTextualLexer2.ml - $(OCAMLOPT) -pp "camlp4o $(LEXER_P4_OPTS)" -c $< -cicTextualParser2.cmx: cicTextualParser2.ml macro.cmo pa_unicode_macro.cmo - $(OCAMLOPT) -pp "camlp4o $(PARSER_P4_OPTS)" -c $< - -%_notation.cmo: %_notation.ml cicTextualParser2.cmo - $(OCAMLC) -pp "camlp4o $(PARSER_P4_OPTS)" -c $< -%_notation.cmx: %_notation.ml cicTextualParser2.cmx - $(OCAMLOPT) -pp "camlp4o $(PARSER_P4_OPTS)" -c $< + $(OCAMLOPT_P4) -c $< +cicTextualParser2.cmx: cicTextualParser2.ml + $(OCAMLOPT_P4) -c $< -pa_unicode_macro.cmo: pa_unicode_macro.ml macro.cmo - $(OCAMLC) -pp "camlp4o $(PA_P4_OPTS)" -c $< -pa_unicode_macro.cmx: pa_unicode_macro.ml macro.cmx - $(OCAMLOPT) -pp "camlp4o $(PA_P4_OPTS)" -c $< +%_notation.cmo: %_notation.ml + $(OCAMLC_P4) -c $< +%_notation.cmx: %_notation.ml + $(OCAMLOPT_P4) -c $< -LOCAL_LINKOPTS = -linkpkg $(PACKAGE).cma +LOCAL_LINKOPTS = -package helm-cic_textual_parser2 -linkpkg test: test_lexer test_parser test_lexer: test_lexer.ml $(PACKAGE).cma $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< test_parser: test_parser.ml $(PACKAGE).cma $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< -make_table: make_table.ml - $(OCAMLC) -linkpkg -o $@ $< - -.PHONY: macro_table.dump -macro_table.dump: make_table - ./make_table $@ clean: extra_clean distclean: extra_clean rm -f macro_table.dump extra_clean: - rm -f test_lexer test_parser make_table + rm -f test_lexer test_parser include ../Makefile.common - -.PHONY: depend -depend: macro.cmi macro.cmo pa_unicode_macro.cmi pa_unicode_macro.cmo - $(OCAMLDEP) -pp "camlp4o $(PARSER_P4_OPTS) $(LEXER_P4_OPTS)" $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend +OCAMLARCHIVEOPTIONS += -linkall disambiguateTypes.cmi: disambiguateTypes.mli $(OCAMLC) -c -rectypes $<