X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2FMakefile;h=2c7f989c9a3d4a22f2c3036af26b5ad721ece422;hb=aec6af4406694eccfa7bba95a1e775c0a21f4f2c;hp=25f5d38fe4a090a5ab20ef3fab0064474ee88ade;hpb=42680d47c033d751738fd0f84af7b45b2a91a5b8;p=helm.git diff --git a/matitaB/matita/Makefile b/matitaB/matita/Makefile index 25f5d38fe..2c7f989c9 100644 --- a/matitaB/matita/Makefile +++ b/matitaB/matita/Makefile @@ -15,12 +15,14 @@ OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION) OCAMLDEP_FLAGS = -pp $(CAMLP5O) PKGS = -package "$(MATITA_REQUIRES)" CPKGS = -package "$(MATITA_CREQUIRES)" +WPKGS = -package "$(MATITA_WREQUIRES)" OCAML_THREADS_FLAGS = -thread OCAML_DEBUG_FLAGS = -g #OCAML_PROF=p -p a #OCAMLOPT_DEBUG_FLAGS = -p OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) OCAMLC = $(OCAMLFIND) ocamlc$(OCAML_PROF) $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS) $(SYNTAXOPTIONS) +OCAMLTOP = $(OCAMLFIND) ocamlmktop$(OCAML_PROF) $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS) $(SYNTAXOPTIONS) OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) $(OCAMLOPT_DEBUG_FLAGS) OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAMLDEP_FLAGS) INSTALL_PROGRAMS= matita matitac @@ -58,6 +60,16 @@ CMLI = \ matitaExcPp.mli \ matitaInit.mli \ $(NULL) +WMLI = \ + matitaTypes.mli \ + matitaMisc.mli \ + applyTransformation.mli \ + matitaEngine.mli \ + matitaExcPp.mli \ + matitaInit.mli \ + matitaFilesystem.mli \ + matitaAuthentication.mli \ + $(NULL) MAINCMLI = \ matitaclean.mli \ $(NULL) @@ -65,6 +77,7 @@ MAINCMLI = \ ML = buildTimeConf.ml matitaGeneratedGui.ml $(MLI:%.mli=%.ml) # objects for matitac (batch compiler) CML = buildTimeConf.ml $(CMLI:%.mli=%.ml) +WML = buildTimeConf.ml $(WMLI:%.mli=%.ml) MAINCML = $(MAINCMLI:%.mli=%.ml) PROGRAMS_BYTE = \ @@ -80,13 +93,30 @@ all: $(PROGRAMS) $(NOINST_PROGRAMS) UTF8DIR := $(shell $(OCAMLFIND) query helm-syntax_extensions) ULEXDIR := $(shell $(OCAMLFIND) query ulex08) + matitaScriptLexer.cmo: SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" +matitaFilesystem.cmi: matitaFilesystem.mli + $(H)echo " OCAMLC $<" + $(H)$(OCAMLC) $(WPKGS) -c $< +matitaFilesystem.cmo: matitaFilesystem.ml + $(H)echo " OCAMLC $<" + $(H)$(OCAMLC) $(WPKGS) -c $< + +matitaAuthentication.cmi: matitaAuthentication.mli + $(H)echo " OCAMLC $<" + $(H)$(OCAMLC) $(WPKGS) -c $< +matitaAuthentication.cmo: matitaAuthentication.ml + $(H)echo " OCAMLC $<" + $(H)$(OCAMLC) $(WPKGS) -c $< + CMOS = $(ML:%.ml=%.cmo) CCMOS = $(CML:%.ml=%.cmo) +WCMOS = $(WML:%.ml=%.cmo) MAINCMOS = $(MAINCML:%.ml=%.cmo) CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS)) +WCMXS = $(patsubst %.cmo,%.cmx,$(WCMOS)) MAINCMXS = $(patsubst %.cmo,%.cmx,$(MAINCMOS)) $(CMOS) : $(LIB_DEPS) $(CMXOS): $(LIBX_DEPS) @@ -95,6 +125,8 @@ LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_REQUIRES)) CLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_CREQUIRES)) CLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_CREQUIRES)) +WLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_WREQUIRES)) +WLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_WREQUIRES)) opt: $(PROGRAMS_OPT) $(NOINST_PROGRAMS_OPT) upx: $(PROGRAMS_UPX) .PHONY: opt upx @@ -120,7 +152,7 @@ linkonly: $(H)echo " OCAMLC matitac.ml" $(H)$(OCAMLC) $(CPKGS) -linkpkg -o matitac $(CCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitac.ml $(H)echo " OCAMLC matitadaemon.ml" - $(H)$(OCAMLC) $(CPKGS) -linkpkg -o matitadaemon $(CCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitadaemon.ml + $(H)$(OCAMLC) $(WPKGS) -linkpkg -o matitadaemon $(WCMOS) $(MAINCMOS) $(OCAML_DEBUG_FLAGS) matitadaemon.ml .PHONY: linkonly matita: matita.ml $(LIB_DEPS) $(CMOS) @@ -137,12 +169,12 @@ matitac.opt: matitac.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) $(H)echo " OCAMLOPT $<" $(H)$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml -matitadaemon: matitadaemon.ml $(CLIB_DEPS) $(CMOS) $(MAINCMOS) +matitadaemon: matitadaemon.ml $(WLIB_DEPS) $(WCMOS) $(MAINCMOS) $(H)echo " OCAMLC $<" - $(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) $(MAINCMOS) matitadaemon.ml -matitadaemon.opt: matitadaemon.ml $(CLIBX_DEPS) $(CMXS) $(MAINCMXS) + $(H)$(OCAMLC) $(WPKGS) -linkpkg -o $@ $(WCMOS) $(MAINCMOS) matitadaemon.ml +matitadaemon.opt: matitadaemon.ml $(WLIBX_DEPS) $(WCMXS) $(MAINCMXS) $(H)echo " OCAMLOPT $<" - $(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) $(MAINCMXS) matitadaemon.ml + $(H)$(OCAMLOPT) $(WPKGS) -linkpkg -o $@ $(WCMXS) $(MAINCMXS) matitadaemon.ml rottener: rottener.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS) $(H)echo " OCAMLC $<" @@ -356,10 +388,10 @@ TAGS: .PHONY: depend -depend: +depend: SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" $(H)echo " OCAMLDEP" $(H)$(OCAMLDEP) *.ml *.mli > .depend -depend.opt: +depend.opt: SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" $(H)echo " OCAMLDEP -native" $(H)$(OCAMLDEP) -native *.ml *.mli > .depend.opt