X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FMakefile;h=5f8063939e54cd990cd886dc4702f5ee658726ab;hb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;hp=57811ff601876f97a6131c7df776ebcd2b257fe7;hpb=76cb30ecd0159512548aee0ba7085ab17c6fd5bd;p=helm.git diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 57811ff60..5f8063939 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -1,35 +1,43 @@ BIN_DIR = /usr/local/bin -REQUIRES = lablgtkmathview helm-cic_textual_parser helm-cic_proof_checking \ - helm-xml gdome2-xslt helm-cic_unification helm-mathql \ - helm-mathql_interpreter -PREDICATES = +REQUIRES = lablgtkmathview helm-cic_textual_parser helm-tex_cic_textual_parser \ + helm-cic_proof_checking helm-xml gdome2-xslt helm-cic_unification \ + helm-mathql helm-mathql_interpreter helm-mathql_generator \ + helm-tactics threads hbugs-client mathml-editor \ + helm-cic_transformations +PREDICATES = "gnome,init,glade" OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o -OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) -OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLFIND = ocamlfind +OCAMLC = $(OCAMLFIND) ocamlc -thread $(OCAMLOPTIONS) +OCAMLOPT = $(OCAMLFIND) ocamlopt -thread $(OCAMLOPTIONS) OCAMLDEP = ocamldep -pp camlp4o -LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) -LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) +LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) +LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) -all: gTopLevel -opt: gTopLevel.opt +all: styles gTopLevel +opt: styles gTopLevel.opt -DEPOBJS = xml2Gdome.ml proofEngineTypes.ml proofEngineHelpers.ml \ - proofEngineReduction.ml proofEngineStructuralRules.ml \ - proofEngineStructuralRules.mli \ - primitiveTactics.ml primitiveTactics.mli ring.ml ring.mli \ - proofEngine.ml proofEngine.mli \ - doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \ - cic2Xml.ml cic2acic.mli logicalOperations.ml sequentPp.ml \ - mQueryGenerator.mli mQueryGenerator.ml gTopLevel.ml +INTERFACE_FILES = \ + proofEngine.mli logicalOperations.mli disambiguate.mli \ + termEditor.mli texTermEditor.mli xmlDiff.mli termViewer.mli \ + invokeTactics.mli hbugs.mli -TOPLEVELOBJS = xml2Gdome.cmo proofEngineTypes.cmo proofEngineHelpers.cmo \ - proofEngineReduction.cmo proofEngineStructuralRules.cmo \ - primitiveTactics.cmo ring.cmo proofEngine.cmo \ - doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \ - logicalOperations.cmo sequentPp.cmo mQueryGenerator.cmo \ - gTopLevel.cmo +DEPOBJS = $INTERFACE_FILES $(INTERFACE_FILES:%.mli=%.ml) gTopLevel.ml +TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) gTopLevel.cmo + +$(INTERFACE_FILES:%.mli=%.cmo): $(LIBRARIES) +$(INTERFACE_FILES:%.mli=%.cmx): $(LIBRARIES_OPT) + +styles: + @echo "***********************************************************************" + @if [ -d stylesheets -a -d meta_stylesheets ] ; then echo -e "* stylesheets and metastylesheets found: *\\n* I will create the request hyperlinks in styles *" ; else echo -e "* stylesheets or meta_stylesheets not found: *\\n* you should check-out the two directories from the MoWGLI repository *" ; exit -1 ; fi + @echo "***********************************************************************" + mkdir styles + (cd styles && for i in ../stylesheets/*.xsl ; do ln -s $$i; done) + (cd styles && for i in ../stylesheets/generated/*.xsl ; do ln -s $$i; done) + (cd styles && rm rootcontent.xsl && ln -s ../rootcontent.xsl) + depend: $(OCAMLDEP) $(DEPOBJS) > .depend @@ -40,13 +48,16 @@ gTopLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT) $(OCAMLOPT) -linkpkg -o gTopLevel.opt $(TOPLEVELOBJS:.cmo=.cmx) .SUFFIXES: .ml .mli .cmo .cmi .cmx -.ml.cmo: $(LIBRARIES) +.ml.cmo: $(OCAMLC) -c $< -.mli.cmi: $(LIBRARIES) +.mli.cmi: $(OCAMLC) -c $< -.ml.cmx: $(LIBRARIES_OPT) +.ml.cmx: $(OCAMLOPT) -c $< +$(TOPLEVELOBJS): $(LIBRARIES) +$(TOPLEVELOBJS:.cmo=.cmx)): $(LIBRARIES_OPT) + clean: rm -f *.cm[iox] *.o gTopLevel gTopLevel.opt @@ -58,4 +69,14 @@ uninstall: .PHONY: install uninstall clean -include .depend +ifneq ($(MAKECMDGOALS), depend) + include .depend +endif + + + + + + + +