From: Stefano Zacchiroli Date: Mon, 19 Apr 2004 12:12:16 +0000 (+0000) Subject: added Makefile.in X-Git-Tag: dead_dir_walking~29 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c6d966bbc276fb0d3bb36ef2945c7bfa31a5ff1b;p=helm.git added Makefile.in --- diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile deleted file mode 100644 index ebf8eeda5..000000000 --- a/helm/gTopLevel/Makefile +++ /dev/null @@ -1,161 +0,0 @@ -BIN_DIR = /usr/local/bin -TEST_REQUIRES = \ - helm-registry \ - helm-mathql_interpreter \ - helm-mathql_generator \ - helm-tactics \ - helm-cic_transformations \ - helm-cic_textual_parser2 \ - helm-cic_textual_parser \ - helm-tex_cic_textual_parser \ - mathml-editor \ - lablgtkmathview -REQUIRES = \ - $(TEST_REQUIRES) \ - gdome2-xslt \ - hbugs-client -PREDICATES = "gnome,init,glade" -OCAMLOPTIONS = \ - -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o -thread -OCAMLFIND = ocamlfind -OCAMLDEBUGOPTIONS = -g -OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) -OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS) -OCAMLDEP = $(OCAMLFIND) ocamldep -pp camlp4o -OCAMLDEBUG = wowcamldebug - -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)) -TEST_LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(TEST_REQUIRES)) -TEST_LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(TEST_REQUIRES)) - -all: styles gTopLevel -opt: styles gTopLevel.opt - -start: - $(MAKE) -C ../hbugs/ start -stop: - $(MAKE) -C ../hbugs/ stop - -INTERFACE_FILES = \ - proofEngine.mli \ - logicalOperations.mli \ - oldDisambiguate.mli \ - disambiguatingParser.mli \ - termEditor.mli \ - texTermEditor.mli \ - xmlDiff.mli \ - chosenTransformer.mli \ - termViewer.mli \ - invokeTactics.mli \ - hbugs.mli \ - chosenTermEditor.mli \ - helmGtkLogger.mli - -DEPOBJS = \ - $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \ - gTopLevel.ml regtest.ml testlibrary.ml batchParser.ml batchParser.mli - -TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) gTopLevel.cmo -TESTOBJS = \ - oldDisambiguate.cmo \ - disambiguatingParser.cmo \ - batchParser.cmo -REGTESTOBJS = $(TESTOBJS) regtest.cmo -TESTLIBOBJS = $(TESTOBJS) testlibrary.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 - -gTopLevel: $(TOPLEVELOBJS) $(LIBRARIES) - $(OCAMLC) -thread -linkpkg -o $@ $(TOPLEVELOBJS) -gTopLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT) - $(OCAMLOPT) -thread -linkpkg -o $@ $(TOPLEVELOBJS:.cmo=.cmx) - -testlibrary: $(TESTLIBOBJS) $(TEST_LIBRARIES) - $(OCAMLFIND) ocamlc -thread $(OCAMLDEBUGOPTIONS) -linkpkg \ - -package "$(TEST_REQUIRES)" -o $@ $(TESTLIBOBJS) -testlibrary.opt: $(TESTLIBOBJS:.cmo=.cmx) $(TEST_LIBRARIES_OPT) - $(OCAMLFIND) ocamlopt -thread -linkpkg -package "$(TEST_REQUIRES)" -o $@ \ - $(TESTLIBOBJS:.cmo=.cmx) - -regtest: $(REGTESTOBJS) $(TEST_LIBRARIES) - $(OCAMLFIND) ocamlc -thread $(OCAMLDEBUGOPTIONS) -linkpkg \ - -package "$(TEST_REQUIRES)" -o $@ $(REGTESTOBJS) -regtest.opt: $(REGTESTOBJS:.cmo=.cmx) $(TEST_LIBRARIES_OPT) - $(OCAMLFIND) ocamlopt -thread -linkpkg -package "$(TEST_REQUIRES)" -o $@ \ - $(REGTESTOBJS:.cmo=.cmx) - -.SUFFIXES: .ml .mli .cmo .cmi .cmx -.ml.cmo: - $(OCAMLC) -c $< -.mli.cmi: - $(OCAMLC) -c $< -.ml.cmx: - $(OCAMLOPT) -c $< - -$(TOPLEVELOBJS): $(LIBRARIES) -$(TOPLEVELOBJS:.cmo=.cmx)): $(LIBRARIES_OPT) - -clean: - rm -f *.cm[iox] *.o gTopLevel{,.opt} regtest{,.opt} testlibrary{,.opt} -install: - cp gTopLevel gTopLevel.opt $(BIN_DIR) -uninstall: - rm -f $(BIN_DIR)/gTopLevel $(BIN_DIR)/gTopLevel.opt - -.PHONY: install uninstall clean test - -INTESTS := $(wildcard tests/*.cic) -OUTTESTS := $(patsubst %, %.test, $(INTESTS)) -gentest: $(OUTTESTS) -cleantest: - rm -f $(OUTTESTS) -tests/%.cic.test: tests/%.cic regtest - time ./regtest -gen $< -test: regtest - ./regtest $(INTESTS) 2> /dev/null -test.opt: regtest.opt - ./regtest.opt $(INTESTS) 2> /dev/null -envtest: regtest - ./regtest -dump $(INTESTS) 2> /dev/null -envtest.opt: regtest.opt - ./regtest.opt -dump $(INTESTS) 2> /dev/null -librarytest: testlibrary - ./testlibrary -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG -librarytest.opt: testlibrary.opt - ./testlibrary.opt -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG - -MAIN = ./gTopLevel -ARGS = -debug: - echo "load_printer \"threads.cma\"" > .debug_script - $(OCAMLFIND) query -recursive -predicates "mt,byte" -a-format \ - helm-cic_unification | \ - sed 's/\(.*\)/load_printer "\1"/' \ - >> .debug_script - echo "install_printer CicMetaSubst.fppsubst" >> .debug_script - echo "install_printer CicMetaSubst.fppterm" >> .debug_script - echo "install_printer CicMetaSubst.fppmetasenv" >> .debug_script - ledit $(OCAMLDEBUG) \ - -source .debug_script \ - -I +threads \ - $(shell $(OCAMLFIND) query -recursive -i-format $(REQUIRES)) \ - $(MAIN) $(ARGS) - -ifneq ($(MAKECMDGOALS), depend) - include .depend -endif - diff --git a/helm/gTopLevel/Makefile.in b/helm/gTopLevel/Makefile.in new file mode 100644 index 000000000..402813f91 --- /dev/null +++ b/helm/gTopLevel/Makefile.in @@ -0,0 +1,161 @@ +BIN_DIR = /usr/local/bin + +TEST_REQUIRES = \ + helm-registry \ + helm-mathql_interpreter \ + helm-mathql_generator \ + helm-tactics \ + helm-cic_transformations \ + helm-cic_textual_parser2 \ + helm-cic_textual_parser \ + helm-tex_cic_textual_parser \ + mathml-editor \ + lablgtkmathview + +REQUIRES = $(TEST_REQUIRES) gdome2-xslt helm-hbugs + +PREDICATES = "gnome,init,glade" +OCAMLOPTIONS = \ + -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o -thread +OCAMLFIND = ocamlfind +OCAMLDEBUGOPTIONS = -g +OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) +OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS) +OCAMLDEP = $(OCAMLFIND) ocamldep -pp camlp4o +OCAMLDEBUG = wowcamldebug + +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)) +TEST_LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(TEST_REQUIRES)) +TEST_LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(TEST_REQUIRES)) + +all: styles gTopLevel +opt: styles gTopLevel.opt + +start: + $(MAKE) -C ../hbugs/ start +stop: + $(MAKE) -C ../hbugs/ stop + +INTERFACE_FILES = \ + proofEngine.mli \ + logicalOperations.mli \ + oldDisambiguate.mli \ + disambiguatingParser.mli \ + termEditor.mli \ + texTermEditor.mli \ + xmlDiff.mli \ + chosenTransformer.mli \ + termViewer.mli \ + invokeTactics.mli \ + hbugs.mli \ + chosenTermEditor.mli \ + helmGtkLogger.mli + +DEPOBJS = \ + $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \ + gTopLevel.ml regtest.ml testlibrary.ml batchParser.ml batchParser.mli + +TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) gTopLevel.cmo +TESTOBJS = \ + oldDisambiguate.cmo \ + disambiguatingParser.cmo \ + batchParser.cmo +REGTESTOBJS = $(TESTOBJS) regtest.cmo +TESTLIBOBJS = $(TESTOBJS) testlibrary.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 + +gTopLevel: $(TOPLEVELOBJS) $(LIBRARIES) + $(OCAMLC) -thread -linkpkg -o $@ $(TOPLEVELOBJS) +gTopLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT) + $(OCAMLOPT) -thread -linkpkg -o $@ $(TOPLEVELOBJS:.cmo=.cmx) + +testlibrary: $(TESTLIBOBJS) $(TEST_LIBRARIES) + $(OCAMLFIND) ocamlc -thread $(OCAMLDEBUGOPTIONS) -linkpkg \ + -package "$(TEST_REQUIRES)" -o $@ $(TESTLIBOBJS) +testlibrary.opt: $(TESTLIBOBJS:.cmo=.cmx) $(TEST_LIBRARIES_OPT) + $(OCAMLFIND) ocamlopt -thread -linkpkg -package "$(TEST_REQUIRES)" -o $@ \ + $(TESTLIBOBJS:.cmo=.cmx) + +regtest: $(REGTESTOBJS) $(TEST_LIBRARIES) + $(OCAMLFIND) ocamlc -thread $(OCAMLDEBUGOPTIONS) -linkpkg \ + -package "$(TEST_REQUIRES)" -o $@ $(REGTESTOBJS) +regtest.opt: $(REGTESTOBJS:.cmo=.cmx) $(TEST_LIBRARIES_OPT) + $(OCAMLFIND) ocamlopt -thread -linkpkg -package "$(TEST_REQUIRES)" -o $@ \ + $(REGTESTOBJS:.cmo=.cmx) + +.SUFFIXES: .ml .mli .cmo .cmi .cmx +.ml.cmo: + $(OCAMLC) -c $< +.mli.cmi: + $(OCAMLC) -c $< +.ml.cmx: + $(OCAMLOPT) -c $< + +$(TOPLEVELOBJS): $(LIBRARIES) +$(TOPLEVELOBJS:.cmo=.cmx)): $(LIBRARIES_OPT) + +clean: + rm -f *.cm[iox] *.o gTopLevel{,.opt} regtest{,.opt} testlibrary{,.opt} +install: + cp gTopLevel gTopLevel.opt $(BIN_DIR) +uninstall: + rm -f $(BIN_DIR)/gTopLevel $(BIN_DIR)/gTopLevel.opt + +.PHONY: install uninstall clean test + +INTESTS := $(wildcard tests/*.cic) +OUTTESTS := $(patsubst %, %.test, $(INTESTS)) +gentest: $(OUTTESTS) +cleantest: + rm -f $(OUTTESTS) +tests/%.cic.test: tests/%.cic regtest + time ./regtest -gen $< +test: regtest + ./regtest $(INTESTS) 2> /dev/null +test.opt: regtest.opt + ./regtest.opt $(INTESTS) 2> /dev/null +envtest: regtest + ./regtest -dump $(INTESTS) 2> /dev/null +envtest.opt: regtest.opt + ./regtest.opt -dump $(INTESTS) 2> /dev/null +librarytest: testlibrary + ./testlibrary -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG +librarytest.opt: testlibrary.opt + ./testlibrary.opt -vars -varsprefix cic:/Coq index.txt 2>/dev/null >LOG + +MAIN = ./gTopLevel +ARGS = +debug: + echo "load_printer \"threads.cma\"" > .debug_script + $(OCAMLFIND) query -recursive -predicates "mt,byte" -a-format \ + helm-cic_unification | \ + sed 's/\(.*\)/load_printer "\1"/' \ + >> .debug_script + echo "install_printer CicMetaSubst.fppsubst" >> .debug_script + echo "install_printer CicMetaSubst.fppterm" >> .debug_script + echo "install_printer CicMetaSubst.fppmetasenv" >> .debug_script + ledit $(OCAMLDEBUG) \ + -source .debug_script \ + -I +threads \ + $(shell $(OCAMLFIND) query -recursive -i-format $(REQUIRES)) \ + $(MAIN) $(ARGS) + +ifneq ($(MAKECMDGOALS), depend) + include .depend +endif + diff --git a/helm/gTopLevel/configure.ac b/helm/gTopLevel/configure.ac index aaa661e0a..fa5e40341 100644 --- a/helm/gTopLevel/configure.ac +++ b/helm/gTopLevel/configure.ac @@ -46,6 +46,16 @@ else fi fi +if test $TERM_EDITOR = "tex"; then + CHOSEN_TERM_EDITOR="include TexTermEditor" +else + if test $TERM_EDITOR = "textual"; then + CHOSEN_TERM_EDITOR="include TermEditor" + else + AC_MSG_ERROR(unknwon term editor $TERM_EDITOR) + fi +fi + AC_SUBST(CHOSEN_TERM_EDITOR) AC_SUBST(CHOSEN_TERM_PARSER) AC_SUBST(CHOSEN_TRANSFORMER) @@ -54,5 +64,6 @@ AC_OUTPUT([ chosenTransformer.ml chosenTermEditor.ml disambiguatingParser.ml + Makefile ])