X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FMakefile;h=e449673058fbdb9d8d9aa028f2e9ff0f2dd6a527;hb=96134b9ec1030ed15cea00d751dd4d744463f62c;hp=8a9c5e535792782c06f68609b80692f447ca2a06;hpb=cedc0cfe0ea81f94ac8b88b71d8f855a33329593;p=helm.git diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 8a9c5e535..e44967305 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -1,28 +1,45 @@ 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)) -all: gTopLevel -opt: gTopLevel.opt +all: styles gTopLevel +opt: styles gTopLevel.opt -DEPOBJS = xml2Gdome.ml proofEngineReduction.ml proofEngine.ml cic2Xml.ml \ - doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \ - cic2acic.mli logicalOperations.ml sequentPp.ml mquery.mli \ - mquery.ml gTopLevel.ml +DEPOBJS = \ + proofEngine.ml proofEngine.mli eta_fixing.ml eta_fixing.mli \ + content2cic.ml content2cic.mli logicalOperations.ml \ + logicalOperations.mli disambiguate.ml disambiguate.mli termEditor.ml \ + termEditor.mli texTermEditor.ml texTermEditor.mli termViewer.ml \ + termViewer.mli invokeTactics.ml invokeTactics.mli hbugs.ml hbugs.mli \ + gTopLevel.ml -TOPLEVELOBJS = xml2Gdome.cmo proofEngineReduction.cmo proofEngine.cmo \ - cic2Xml.cmo doubleTypeInference.cmo cic2acic.cmo \ - logicalOperations.cmo sequentPp.cmo mquery.cmo gTopLevel.cmo +TOPLEVELOBJS = \ + eta_fixing.cmo content2cic.cmo \ + proofEngine.cmo logicalOperations.cmo \ + disambiguate.cmo termEditor.cmo texTermEditor.cmo termViewer.cmo \ + invokeTactics.cmo hbugs.cmo gTopLevel.cmo +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 @@ -33,13 +50,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 @@ -51,4 +71,14 @@ uninstall: .PHONY: install uninstall clean -include .depend +ifneq ($(MAKECMDGOALS), depend) + include .depend +endif + + + + + + + +