From d4c6f8464dc183326b7f7b4dc6171e69b482a26b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Mar 2006 15:51:25 +0000 Subject: [PATCH] more work for the release --- Makefile | 19 ++- components/Makefile | 86 ++++++---- components/Makefile.common | 12 +- .../{metadata => binaries}/dump_db/dump.sh | 0 .../{metadata => binaries}/extractor/.depend | 0 .../{metadata => binaries}/extractor/Makefile | 28 ++-- .../extractor/extractor.conf.xml | 0 .../extractor/extractor.ml | 0 .../extractor/extractor_manager.ml | 0 components/binaries/table_creator/.depend | 0 .../table_creator/Makefile | 34 ++-- .../table_creator/sync_db.sh | 0 .../table_creator/table_creator.ml | 0 .../utilities/Makefile | 20 ++- .../utilities/create_environment.ml | 0 .../utilities/list_uris.ml | 0 .../utilities/parse_library.ml | 0 components/cic_proof_checking/Makefile | 12 -- components/content_pres/Makefile | 1 + components/grafite_parser/Makefile | 1 + components/library/libraryClean.ml | 5 +- components/metadata/Makefile | 24 --- components/metadata/table_creator/.depend | 4 - matita/.depend | 22 ++- matita/Makefile | 153 +++++++++--------- matita/help/C/sec_install.xml | 11 +- matita/matita.conf.xml.in | 4 +- matita/matita.glade | 31 ++-- matita/matitaInit.ml | 4 +- matita/matitaMisc.ml | 6 + matita/matitaMisc.mli | 3 + matita/matitacLib.ml | 18 ++- matita/matitaclean.ml | 1 + matita/matitamakeLib.ml | 6 +- 34 files changed, 286 insertions(+), 219 deletions(-) rename components/{metadata => binaries}/dump_db/dump.sh (100%) rename components/{metadata => binaries}/extractor/.depend (100%) rename components/{metadata => binaries}/extractor/Makefile (61%) rename components/{metadata => binaries}/extractor/extractor.conf.xml (100%) rename components/{metadata => binaries}/extractor/extractor.ml (100%) rename components/{metadata => binaries}/extractor/extractor_manager.ml (100%) create mode 100644 components/binaries/table_creator/.depend rename components/{metadata => binaries}/table_creator/Makefile (51%) rename components/{metadata => binaries}/table_creator/sync_db.sh (100%) rename components/{metadata => binaries}/table_creator/table_creator.ml (100%) rename components/{cic_proof_checking => binaries}/utilities/Makefile (56%) rename components/{cic_proof_checking => binaries}/utilities/create_environment.ml (100%) rename components/{cic_proof_checking => binaries}/utilities/list_uris.ml (100%) rename components/{cic_proof_checking => binaries}/utilities/parse_library.ml (100%) delete mode 100644 components/metadata/table_creator/.depend diff --git a/Makefile b/Makefile index 5b069ddf8..f92c8da64 100644 --- a/Makefile +++ b/Makefile @@ -1,3 +1,4 @@ +H=@ include Makefile.defs @@ -5,10 +6,23 @@ SUBDIRS = components matita all: $(foreach d,$(SUBDIRS),rec@all@$(d)) opt: $(foreach d,$(SUBDIRS),rec@opt@$(d)) -world: $(foreach d,$(SUBDIRS),rec@world@$(d)) +world: depend $(foreach d,$(SUBDIRS),rec@world@$(d)) +depend: depend-stamp +depend-stamp: +ifeq ($(HAVE_OCAMLOPT),yes) + ifeq ($(DISTRIBUTED),yes) + $(MAKE) $(foreach d,$(SUBDIRS),rec@depend.opt@$(d)) + else + $(MAKE) $(foreach d,$(SUBDIRS),rec@depend@$(d)) + endif +else + $(MAKE) $(foreach d,$(SUBDIRS),rec@depend@$(d)) +endif + $(H)touch depend-stamp + clean: $(foreach d,$(SUBDIRS),rec@clean@$(d)) distclean: $(foreach d,$(SUBDIRS),rec@distclean@$(d)) - rm -rf .matita library-stamp + $(H)rm -rf .matita library-stamp depend-stamp install: $(foreach d,$(SUBDIRS),rec@install@$(d)) uninstall: $(foreach d,$(SUBDIRS),rec@uninstall@$(d)) @@ -57,6 +71,7 @@ dist_export: dist/configure mkdir $(DISTDIR) svn export components $(DISTDIR)/components svn export matita $(DISTDIR)/matita + (cd $(DISTDIR) && find . -name .depend -exec rm \{\} \;) (cd $(DISTDIR) && rm -f $(CLEAN_ON_DIST)) cp $< $(DISTDIR)/configure cp -r $(EXTRA_DIST) $(DISTDIR) diff --git a/components/Makefile b/components/Makefile index 686fa74d7..6b5e68325 100644 --- a/components/Makefile +++ b/components/Makefile @@ -1,4 +1,4 @@ - +H=@ export SHELL=/bin/bash include ../Makefile.defs @@ -32,31 +32,37 @@ MODULES = \ lexicon \ grafite_engine \ grafite_parser \ - tactics/paramodulation \ $(NULL) -METAS = $(filter-out %/paramodulation,$(MODULES:%=METAS/META.helm-%)) +METAS = $(MODULES:%=METAS/META.helm-%) + +ifeq ($(DISTRIBUTED),no) + MODULES+=binaries +endif all: metas $(MODULES:%=rec@all@%) opt: metas $(MODULES:%=rec@opt@%) + ifeq ($(HAVE_OCAMLOPT),yes) -world: all opt +world: opt else world: all endif -depend: $(MODULES:%=rec@depend@%) +syntax-extensions: + $(H)$(MAKE) -C utf8_macros depend + $(H)$(MAKE) -C utf8_macros pa_unicode_macro.cma +depend: syntax-extensions $(MODULES:%=rec@depend@%) +depend.opt: syntax-extensions $(MODULES:%=rec@depend.opt@%) install: $(MODULES:%=rec@install@%) uninstall: $(MODULES:%=rec@uninstall@%) clean: $(MODULES:%=rec@clean@%) clean_metas .stats: $(MODULES:%=rec@.stats@%) - (for m in $(MODULES); do echo -n "$$m:"; cat $$m/.stats; done) \ + $(H)(for m in $(MODULES); do echo -n "$$m:"; cat $$m/.stats; done) \ | sort -t : -k 2 -n -r > .stats -rec@%@tactics/paramodulation: - $(MAKE) -C tactics/paramodulation $* rec@%: - $(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*)) + $(H)$(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*)) EXTRA_DIST_CLEAN = \ libraries-clusters.ps \ @@ -69,54 +75,70 @@ EXTRA_DIST_CLEAN = \ $(NULL) distclean: clean clean_metas - rm -f $(METAS) - rm -f configure config.log config.cache config.status - rm -f $(EXTRA_DIST_CLEAN) + $(H)rm -f $(METAS) + $(H)rm -f configure config.log config.cache config.status + $(H)rm -f $(EXTRA_DIST_CLEAN) .PHONY: all opt world metas depend install uninstall clean clean_metas distclean METAS/META.helm-%: METAS/meta.helm-%.src - cp $< $@ && echo "directory=\"$(shell pwd)/$*\"" >> $@ + $(H)cp $< $@ && echo "directory=\"$(shell pwd)/$*\"" >> $@ SIMPLIFYDEPS = ../daemons/graphs/tools/simplify_deps/simplify_deps $(SIMPLIFYDEPS): - $(MAKE) -C $(dir $(SIMPLIFYDEPS)) + $(H)$(MAKE) -C $(dir $(SIMPLIFYDEPS)) .PHONY: .dep.dot .dep.dot: $(SIMPLIFYDEPS) - echo "digraph G {" > $@ - echo " rankdir = TB ;" >> $@ - for i in $(MODULES); do $(OCAMLFIND) query helm-$$i -recursive -p-format | grep helm | sed "s/^helm-/ \"$$i\" -> \"/g" | sed "s/$$/\";/g" >> $@ ; done - mv $@ $@.old ; $(SIMPLIFYDEPS) < $@.old > $@ ; rm $@.old - echo "}" >> $@ + $(H)echo "digraph G {" > $@ + $(H)echo " rankdir = TB ;" >> $@ + $(H)for i in $(MODULES); do \ + $(OCAMLFIND) query helm-$$i -recursive -p-format | \ + grep helm | \ + sed "s/^helm-/ \"$$i\" -> \"/g" | \ + sed "s/$$/\";/g" >> $@ ; \ + done + $(H)mv $@ $@.old ; $(SIMPLIFYDEPS) < $@.old > $@ ; rm $@.old + $(H)echo "}" >> $@ .PHONY: .alldep.dot .alldep.dot: - echo "digraph G {" > $@ - echo " rankdir = TB ;" >> $@ - for i in $(MODULES); do $(OCAMLFIND) query helm-$$i -recursive -p-format | grep -v "pxp-" | sed "s/^pxp/pxp[-*]/g" | sed "s/^/ \"helm-$$i\" -> \"/g" | sed "s/$$/\";/g" >> $@ ; done - mv $@ $@.old ; ./simplify_deps/simplify_deps.opt < $@.old > $@ ; rm $@.old - for i in $(MODULES); do echo "\"helm-$$i\" [shape=box,style=filled,fillcolor=yellow];" >> $@ ; done - echo "}" >> $@ + $(H)echo "digraph G {" > $@ + $(H)echo " rankdir = TB ;" >> $@ + $(H)for i in $(MODULES); do \ + $(OCAMLFIND) query helm-$$i -recursive -p-format | \ + grep -v "pxp-" | \ + sed "s/^pxp/pxp[-*]/g" | \ + sed "s/^/ \"helm-$$i\" -> \"/g" | \ + sed "s/$$/\";/g" >> $@ ; \ + done + $(H)mv $@ $@.old ; \ + ./simplify_deps/simplify_deps.opt < $@.old > $@ ; \ + rm $@.old + $(H)for i in $(MODULES); do \ + echo "\"helm-$$i\" [shape=box,style=filled,fillcolor=yellow];"\ + >> $@ ; \ + done + $(H)echo "}" >> $@ .extdep.dot: .dep.dot - STATS/patch_deps.sh $< $@ + $(H)STATS/patch_deps.sh $< $@ .clustersdep.dot: .dep.dot - USE_CLUSTERS=yes STATS/patch_deps.sh $< $@ + $(H)USE_CLUSTERS=yes STATS/patch_deps.sh $< $@ libraries.ps: .dep.dot - dot -Tps -o $@ $< + $(H)dot -Tps -o $@ $< libraries-ext.ps: .extdep.dot - dot -Tps -o $@ $< + $(H)dot -Tps -o $@ $< libraries-clusters.ps: .clustersdep.dot - dot -Tps -o $@ $< + $(H)dot -Tps -o $@ $< libraries-complete.ps: .alldep.dot - dot -Tps -o $@ $< + $(H)dot -Tps -o $@ $< ps: libraries.ps libraries-ext.ps libraries-clusters.ps tags: TAGS .PHONY: TAGS TAGS: - otags -vi -r . + $(H)otags -vi -r . diff --git a/components/Makefile.common b/components/Makefile.common index 9feae4f86..b6ad6eb96 100644 --- a/components/Makefile.common +++ b/components/Makefile.common @@ -62,7 +62,6 @@ all: prereq $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(ARCHIVE) @echo -n opt: prereq $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(ARCHIVE_OPT) @echo -n -world: all opt test: test.ml $(ARCHIVE) $(OCAMLC) $(ARCHIVE) -linkpkg -o $@ $< test.opt: test.ml $(ARCHIVE_OPT) @@ -70,8 +69,13 @@ test.opt: test.ml $(ARCHIVE_OPT) install: uninstall: -depend: $(DEPEND_FILES) - $(OCAMLDEP) $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend +depend:: $(DEPEND_FILES) + $(H)echo " OCAMLDEP" + $(H)$(OCAMLDEP) $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend +depend.opt:: $(DEPEND_FILES) + $(H)echo " OCAMLDEP -native" + $(H)$(OCAMLDEP) -native \ + $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend $(PACKAGE).ps: .dep.dot dot -Tps -o $@ $< @@ -128,7 +132,9 @@ STATS_FILES = \ .PHONY: all opt world backup depend install uninstall clean ocamlinit ifneq ($(MAKECMDGOALS), depend) + ifneq ($(MAKECMDGOALS), depend.opt) include .depend + endif endif NULL = diff --git a/components/metadata/dump_db/dump.sh b/components/binaries/dump_db/dump.sh similarity index 100% rename from components/metadata/dump_db/dump.sh rename to components/binaries/dump_db/dump.sh diff --git a/components/metadata/extractor/.depend b/components/binaries/extractor/.depend similarity index 100% rename from components/metadata/extractor/.depend rename to components/binaries/extractor/.depend diff --git a/components/metadata/extractor/Makefile b/components/binaries/extractor/Makefile similarity index 61% rename from components/metadata/extractor/Makefile rename to components/binaries/extractor/Makefile index 579a5655f..f7151e3cb 100644 --- a/components/metadata/extractor/Makefile +++ b/components/binaries/extractor/Makefile @@ -1,30 +1,31 @@ +H=@ all: extractor extractor_manager - @echo -n + $(H)echo -n opt: extractor.opt extractor_manager.opt - @echo -n + $(H)echo -n clean: rm -f *.cm[ixo] *.[ao] extractor extractor.opt *.err *.out extractor_manager extractor_manager.opt extractor: extractor.ml - @echo " OCAMLC $<" - @$(OCAMLFIND) ocamlc \ + $(H)echo " OCAMLC $<" + $(H)$(OCAMLFIND) ocamlc \ -thread -package mysql,helm-metadata -linkpkg -o $@ $< extractor.opt: extractor.ml - @echo " OCAMLOPT $<" - @$(OCAMLFIND) ocamlopt \ + $(H)echo " OCAMLOPT $<" + $(H)$(OCAMLFIND) ocamlopt \ -thread -package mysql,helm-metadata -linkpkg -o $@ $< extractor_manager: extractor_manager.ml - @echo " OCAMLC $<" - @$(OCAMLFIND) ocamlc \ + $(H)echo " OCAMLC $<" + $(H)$(OCAMLFIND) ocamlc \ -thread -package mysql,helm-metadata -linkpkg -o $@ $< extractor_manager.opt: extractor_manager.ml - @echo " OCAMLOPT $<" - @$(OCAMLFIND) ocamlopt \ + $(H)echo " OCAMLOPT $<" + $(H)$(OCAMLFIND) ocamlopt \ -thread -package mysql,helm-metadata -linkpkg -o $@ $< export: extractor.opt extractor_manager.opt @@ -32,5 +33,12 @@ export: extractor.opt extractor_manager.opt time \ ./extractor_manager.opt 1>export.out 2>export.err +depend: + $(H)echo " OCAMLDEP" + $(H)ocamldep extractor.ml extractor_manager.ml > .depend +depend.opt: + $(H)echo " OCAMLDEP -native" + $(H)ocamldep -native extractor.ml extractor_manager.ml > .depend + include .depend include ../../../Makefile.defs diff --git a/components/metadata/extractor/extractor.conf.xml b/components/binaries/extractor/extractor.conf.xml similarity index 100% rename from components/metadata/extractor/extractor.conf.xml rename to components/binaries/extractor/extractor.conf.xml diff --git a/components/metadata/extractor/extractor.ml b/components/binaries/extractor/extractor.ml similarity index 100% rename from components/metadata/extractor/extractor.ml rename to components/binaries/extractor/extractor.ml diff --git a/components/metadata/extractor/extractor_manager.ml b/components/binaries/extractor/extractor_manager.ml similarity index 100% rename from components/metadata/extractor/extractor_manager.ml rename to components/binaries/extractor/extractor_manager.ml diff --git a/components/binaries/table_creator/.depend b/components/binaries/table_creator/.depend new file mode 100644 index 000000000..e69de29bb diff --git a/components/metadata/table_creator/Makefile b/components/binaries/table_creator/Makefile similarity index 51% rename from components/metadata/table_creator/Makefile rename to components/binaries/table_creator/Makefile index c54e52d4a..15cf1863a 100644 --- a/components/metadata/table_creator/Makefile +++ b/components/binaries/table_creator/Makefile @@ -1,3 +1,5 @@ +H=@ + REQUIRES = mysql helm-metadata INTERFACE_FILES = @@ -7,29 +9,37 @@ EXTRA_OBJECTS_TO_CLEAN = \ table_creator table_creator.opt table_destructor table_destructor.opt all: table_creator table_destructor - @echo -n + $(H)echo -n opt: table_creator.opt table_destructor.opt - @echo -n + $(H)echo -n -table_creator: table_creator.ml ../metadata.cma - @echo " OCAMLC $<" - @$(OCAMLFIND) ocamlc \ +table_creator: table_creator.ml + $(H)echo " OCAMLC $<" + $(H)$(OCAMLFIND) ocamlc \ -thread -package mysql,helm-metadata -linkpkg -o $@ $< table_destructor: table_creator - @ln -f $< $@ + $(H)ln -f $< $@ -table_creator.opt: table_creator.ml ../metadata.cmxa - @echo " OCAMLOPT $<" - @$(OCAMLFIND) ocamlopt \ +table_creator.opt: table_creator.ml + $(H)echo " OCAMLOPT $<" + $(H)$(OCAMLFIND) ocamlopt \ -thread -package mysql,helm-metadata -linkpkg -o $@ $< table_destructor.opt: table_creator.opt - @ln -f $< $@ + $(H)ln -f $< $@ clean: - rm -f *.cm[iox] *.a *.o - rm -f table_creator table_creator.opt table_destructor table_destructor.opt + $(H)rm -f *.cm[iox] *.a *.o + $(H)rm -f table_creator table_creator.opt \ + table_destructor table_destructor.opt + +depend: + $(H)echo " OCAMLDEP" + $(H)ocamldep table_creator.ml > .depend +depend.opt: + $(H)echo " OCAMLDEP -native" + $(H)ocamldep -native table_creator.ml > .depend include .depend include ../../../Makefile.defs diff --git a/components/metadata/table_creator/sync_db.sh b/components/binaries/table_creator/sync_db.sh similarity index 100% rename from components/metadata/table_creator/sync_db.sh rename to components/binaries/table_creator/sync_db.sh diff --git a/components/metadata/table_creator/table_creator.ml b/components/binaries/table_creator/table_creator.ml similarity index 100% rename from components/metadata/table_creator/table_creator.ml rename to components/binaries/table_creator/table_creator.ml diff --git a/components/cic_proof_checking/utilities/Makefile b/components/binaries/utilities/Makefile similarity index 56% rename from components/cic_proof_checking/utilities/Makefile rename to components/binaries/utilities/Makefile index 383391d70..c22d2a99d 100644 --- a/components/cic_proof_checking/utilities/Makefile +++ b/components/binaries/utilities/Makefile @@ -1,3 +1,5 @@ +H=@ + UTILITIES = create_environment parse_library list_uris UTILITIES_OPT = $(patsubst %,%.opt,$(UTILITIES)) LINKOPTS = -linkpkg -thread @@ -5,17 +7,23 @@ LIBS = helm-cic_proof_checking OCAMLC = $(OCAMLFIND) ocamlc $(LINKOPTS) -package $(LIBS) OCAMLOPT = $(OCAMLFIND) opt $(LINKOPTS) -package $(LIBS) all: $(UTILITIES) - @echo -n + $(H)echo -n opt: $(UTILITIES_OPT) - @echo -n + $(H)echo -n %: %.ml - @echo " OCAMLC $<" - @$(OCAMLC) -o $@ $< + $(H)echo " OCAMLC $<" + $(H)$(OCAMLC) -o $@ $< %.opt: %.ml - @echo " OCAMLOPT $<" - @$(OCAMLOPT) -o $@ $< + $(H)echo " OCAMLOPT $<" + $(H)$(OCAMLOPT) -o $@ $< clean: rm -f $(UTILITIES) $(UTILITIES_OPT) *.cm[iox] *.o +depend: + $(H)echo " OCAMLDEP" + $(H)ocamldep extractor.ml extractor_manager.ml > .depend +depend.opt: + $(H)echo " OCAMLDEP -native" + $(H)ocamldep -native extractor.ml extractor_manager.ml > .depend include ../../../Makefile.defs diff --git a/components/cic_proof_checking/utilities/create_environment.ml b/components/binaries/utilities/create_environment.ml similarity index 100% rename from components/cic_proof_checking/utilities/create_environment.ml rename to components/binaries/utilities/create_environment.ml diff --git a/components/cic_proof_checking/utilities/list_uris.ml b/components/binaries/utilities/list_uris.ml similarity index 100% rename from components/cic_proof_checking/utilities/list_uris.ml rename to components/binaries/utilities/list_uris.ml diff --git a/components/cic_proof_checking/utilities/parse_library.ml b/components/binaries/utilities/parse_library.ml similarity index 100% rename from components/cic_proof_checking/utilities/parse_library.ml rename to components/binaries/utilities/parse_library.ml diff --git a/components/cic_proof_checking/Makefile b/components/cic_proof_checking/Makefile index 8e2f99a15..83b211447 100644 --- a/components/cic_proof_checking/Makefile +++ b/components/cic_proof_checking/Makefile @@ -29,15 +29,3 @@ include ../Makefile.common cicReduction.cmo: OCAMLOPTIONS+=-rectypes cicReduction.cmx: OCAMLOPTIONS+=-rectypes -all: all_utilities -opt: opt_utilities - -all_utilities: - @$(MAKE) -C utilities/ all -opt_utilities: - @$(MAKE) -C utilities/ opt - -clean: clean_utilities -clean_utilities: - @$(MAKE) -C utilities/ clean - diff --git a/components/content_pres/Makefile b/components/content_pres/Makefile index 0cd8b4226..5d43e18ab 100644 --- a/components/content_pres/Makefile +++ b/components/content_pres/Makefile @@ -56,5 +56,6 @@ cicNotationParser.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) cicNotationLexer.ml.annot: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) cicNotationParser.ml.annot: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) depend: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) +depend.opt: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) # diff --git a/components/grafite_parser/Makefile b/components/grafite_parser/Makefile index 434eaceaa..964b0a86a 100644 --- a/components/grafite_parser/Makefile +++ b/components/grafite_parser/Makefile @@ -23,6 +23,7 @@ MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ule grafiteParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) grafiteParser.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) depend: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) +depend.opt: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) # # grafiteParser.cmo: OCAMLC = $(OCAMLC_P4) diff --git a/components/library/libraryClean.ml b/components/library/libraryClean.ml index 8b32e97c4..04333fc9a 100644 --- a/components/library/libraryClean.ml +++ b/components/library/libraryClean.ml @@ -227,7 +227,10 @@ let clean_baseuris ?(verbose=true) buris = let buri = UriManager.buri_of_uri uri in if buri <> !last_baseuri then begin - HLog.message ("Removing: " ^ buri ^ "/*"); + if Helm_registry.get_bool "matita.bench" then + (print_endline ("matitaclean " ^ buri ^ "/");flush stdout) + else + HLog.message ("Removing: " ^ buri ^ "/*"); last_baseuri := buri end; LibrarySync.remove_obj uri diff --git a/components/metadata/Makefile b/components/metadata/Makefile index d02d021a5..6c9aa763c 100644 --- a/components/metadata/Makefile +++ b/components/metadata/Makefile @@ -14,27 +14,3 @@ EXTRA_OBJECTS_TO_CLEAN = include ../../Makefile.defs include ../Makefile.common - -all: all_table_creator all_extractor -opt: opt_table_creator opt_extractor - -all_table_creator: - @make -C table_creator/ all -opt_table_creator: - @make -C table_creator/ opt - -all_extractor: - @make -C extractor/ all -opt_extractor: - @make -C extractor/ opt - -clean: clean_table_creator clean_extractor - -clean_table_creator: - @echo " cleaning: table_creator" - @make -C table_creator/ clean - -clean_extractor: - @echo " cleaning: extractor" - @make -C extractor/ clean - diff --git a/components/metadata/table_creator/.depend b/components/metadata/table_creator/.depend deleted file mode 100644 index 1cf113d91..000000000 --- a/components/metadata/table_creator/.depend +++ /dev/null @@ -1,4 +0,0 @@ -sql.cmo: sql.cmi -sql.cmx: sql.cmi -table_creator.cmo: sql.cmi -table_creator.cmx: sql.cmx diff --git a/matita/.depend b/matita/.depend index 300db49f5..e90c087c7 100644 --- a/matita/.depend +++ b/matita/.depend @@ -6,12 +6,12 @@ dump_moo.cmo: buildTimeConf.cmi dump_moo.cmx: buildTimeConf.cmx gragrep.cmo: matitaInit.cmi buildTimeConf.cmi gragrep.cmi gragrep.cmx: matitaInit.cmx buildTimeConf.cmx gragrep.cmi -matitaclean.cmo: matitaInit.cmi matitaclean.cmi -matitaclean.cmx: matitaInit.cmx matitaclean.cmi -matitacLib.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ - buildTimeConf.cmi matitacLib.cmi -matitacLib.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ - buildTimeConf.cmx matitacLib.cmi +matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi +matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi +matitacLib.cmo: matitamakeLib.cmi matitaMisc.cmi matitaInit.cmi \ + matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmi matitacLib.cmi +matitacLib.cmx: matitamakeLib.cmx matitaMisc.cmx matitaInit.cmx \ + matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi matitac.cmo: matitamake.cmi matitadep.cmi matitaclean.cmi matitacLib.cmi \ gragrep.cmi matitac.cmx: matitamake.cmx matitadep.cmx matitaclean.cmx matitacLib.cmx \ @@ -22,13 +22,11 @@ matitaEngine.cmo: matitaEngine.cmi matitaEngine.cmx: matitaEngine.cmi matitaExcPp.cmo: matitaExcPp.cmi matitaExcPp.cmx: matitaExcPp.cmi -matitaGeneratedGui.cmo: matitaGeneratedGui.cmi -matitaGeneratedGui.cmx: matitaGeneratedGui.cmi -matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmi matitaGtkMisc.cmi +matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmo matitaGtkMisc.cmi matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmi matitaGui.cmo: matitamakeLib.cmi matitaTypes.cmi matitaScript.cmi \ matitaMisc.cmi matitaMathView.cmi matitaGtkMisc.cmi \ - matitaGeneratedGui.cmi matitaExcPp.cmi buildTimeConf.cmi matitaGui.cmi + matitaGeneratedGui.cmo matitaExcPp.cmi buildTimeConf.cmi matitaGui.cmi matitaGui.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx \ matitaMisc.cmx matitaMathView.cmx matitaGtkMisc.cmx \ matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi @@ -56,8 +54,8 @@ matitaScript.cmx: matitamakeLib.cmx matitaTypes.cmx matitaMisc.cmx \ matitaEngine.cmx buildTimeConf.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi -matitaGtkMisc.cmi: matitaGeneratedGui.cmi +matitaGtkMisc.cmi: matitaGeneratedGui.cmo matitaGui.cmi: matitaGuiTypes.cmi -matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmi +matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmo matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi matitaScript.cmi: matitaTypes.cmi diff --git a/matita/Makefile b/matita/Makefile index e8dff77e0..7c54333cd 100644 --- a/matita/Makefile +++ b/matita/Makefile @@ -67,7 +67,7 @@ all: $(PROGRAMS) $(NOINST_PROGRAMS) # all: matita.conf.xml $(PROGRAMS) coq.moo # matita.conf.xml: matita.conf.xml.sample -# @if diff matita.conf.xml.sample matita.conf.xml 1>/dev/null 2>/dev/null; then\ +# $(H)if diff matita.conf.xml.sample matita.conf.xml 1>/dev/null 2>/dev/null; then\ # touch matita.conf.xml;\ # else\ # echo;\ @@ -96,68 +96,68 @@ upx: $(PROGRAMS_UPX) .PHONY: opt upx ifeq ($(HAVE_OCAMLOPT),yes) -world: all opt +world: depend.opt opt else -world: all +world: depend all endif matita: matita.ml $(LIB_DEPS) $(CMOS) - @echo " OCAMLC $<" + $(H)echo " OCAMLC $<" $(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) matita.ml matita.opt: matita.ml $(LIBX_DEPS) $(CMXS) - @echo " OCAMLOPT $<" + $(H)echo " OCAMLOPT $<" $(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml dump_moo: dump_moo.ml buildTimeConf.cmo - @echo " OCAMLC $<" + $(H)echo " OCAMLC $<" $(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ buildTimeConf.cmo $< dump_moo.opt: dump_moo.ml buildTimeConf.cmx - @echo "OCAMLOPT $<" + $(H)echo "OCAMLOPT $<" $(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ buildTimeConf.cmx $< matitac: matitac.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS) - @echo " OCAMLC $<" + $(H)echo " OCAMLC $<" $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) $(MAINCMOS) matitac.ml matitac.opt: matitac.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) - @echo " OCAMLOPT $<" + $(H)echo " OCAMLOPT $<" $(H)$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml matitatop: matitatop.ml $(CLIB_DEPS) $(CCMOS) - @echo " OCAMLC $<" + $(H)echo " OCAMLC $<" $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $< matitadep: matitac - @test -f $@ || ln -s $< $@ + $(H)test -f $@ || ln -s $< $@ matitadep.opt: matitac.opt - @test -f $@ || ln -s $< $@ + $(H)test -f $@ || ln -s $< $@ matitaclean: matitac - @test -f $@ || ln -s $< $@ + $(H)test -f $@ || ln -s $< $@ matitaclean.opt: matitac.opt - @test -f $@ || ln -s $< $@ + $(H)test -f $@ || ln -s $< $@ matitamake: matitac - @test -f $@ || ln -s $< $@ + $(H)test -f $@ || ln -s $< $@ matitamake.opt: matitac.opt - @test -f $@ || ln -s $< $@ + $(H)test -f $@ || ln -s $< $@ gragrep: matitac - @test -f $@ || ln -s $< $@ + $(H)test -f $@ || ln -s $< $@ gragrep.opt: matitac.opt - @test -f $@ || ln -s $< $@ + $(H)test -f $@ || ln -s $< $@ cicbrowser: matita - @test -f $@ || ln -s $< $@ + $(H)test -f $@ || ln -s $< $@ cicbrowser.opt: matita.opt - @test -f $@ || ln -s $< $@ + $(H)test -f $@ || ln -s $< $@ matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade - $(LABLGLADECC) -embed $< > matitaGeneratedGui.ml - $(OCAMLC) $(PKGS) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli + $(H)$(LABLGLADECC) -embed $< > matitaGeneratedGui.ml + $(H)#$(OCAMLC) $(PKGS) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli .PHONY: clean clean: - rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \ + $(H)rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \ $(PROGRAMS) $(PROGRAMS_OPT) \ $(NOINST_PROGRAMS) $(NOINST_PROGRAMS_OPT) \ $(PROGRAMS_STATIC) \ @@ -166,12 +166,12 @@ clean: .PHONY: distclean distclean: clean - $(MAKE) -C dist/ clean - rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli - rm -f buildTimeConf.ml - rm -f matita.glade.bak matita.gladep.bak - rm -f matita.conf.xml.sample - rm -rf .matita + $(H)$(MAKE) -C dist/ clean + $(H)rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli + $(H)rm -f buildTimeConf.ml + $(H)rm -f matita.glade.bak matita.gladep.bak + $(H)rm -f matita.conf.xml.sample + $(H)rm -rf .matita TEST_DIRS = \ library \ @@ -198,33 +198,16 @@ cleantests.opt: $(foreach d,$(TEST_DIRS),$(d)-cleantests-opt) # {{{ Distribution stuff -ifeq ($(HAVE_OCAMLOPT),yes) -BEST=opt -BEST_EXT=.opt -else -BEST=all -BEST_EXT= -endif - ifeq ($(DISTRIBUTED),yes) -dist_library: dist_library@library +dist_library: dist_library@standard-library dist_library@%: - @echo "MATITAMAKE init $*" - $(H)MATITA_RT_BASE_DIR=`pwd` \ - MATITA_FLAGS="-conffile `pwd`/matita.conf.xml" \ - ./matitamake$(BEST_EXT) -conffile `pwd`/matita.conf.xml \ - init $* `pwd`/$* - @echo "MATITAMAKE publish $*" - $(H)MATITA_RT_BASE_DIR=`pwd` \ - MATITA_FLAGS="-conffile `pwd`/matita.conf.xml" \ - ./matitamake$(BEST_EXT) -conffile `pwd`/matita.conf.xml \ - publish $* - @echo "MATITAMAKE destroy $*" - $(H)MATITA_RT_BASE_DIR=`pwd` \ - MATITA_FLAGS="-conffile `pwd`/matita.conf.xml" \ - ./matitamake$(BEST_EXT) -conffile `pwd`/matita.conf.xml \ - destroy $* + $(H)echo "MATITAMAKE init $*" + $(H)(cd $(DESTDIR) && ./matitamake init $* $(DESTDIR)/ma/$*) + $(H)echo "MATITAMAKE publish $*" + $(H)(cd $(DESTDIR) && ./matitamake publish $*) + $(H)echo "MATITAMAKE destroy $*" + $(H)(cd $(DESTDIR) && ./matitamake destroy $*) touch $@ endif @@ -245,26 +228,37 @@ INSTALL_STUFF = \ LICENSE \ $(NULL) - +INSTALL_PROGRAMS= matita matitac +INSTALL_PROGRAMS_LINKS_MATITA= cicbrowser +INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitamake matitaclean ifeq ($(HAVE_OCAMLOPT),yes) -INSTALL_STUFF_BIN = $(PROGRAMS_OPT) +INSTALL_STUFF_BIN = $(INSTALL_PROGRAMS:%=%.opt) else -INSTALL_STUFF_BIN = $(PROGRAMS_BYTE) +INSTALL_STUFF_BIN = $(INSTALL_PROGRAMS) endif -install: install_preliminaries - #dist_library +install: install_preliminaries dist_library install_conclusion install_preliminaries: install -d $(DESTDIR)/ma/ cp -a $(INSTALL_STUFF) $(DESTDIR) - install -s $(INSTALL_STUFF_BIN) $(DESTDIR) ifeq ($(HAVE_OCAMLOPT),yes) - for p in $(PROGRAMS_BYTE); do ln -fs $$p.opt $(DESTDIR)/$$p; done + install -s $(INSTALL_STUFF_BIN) $(DESTDIR) + for p in $(INSTALL_PROGRAMS); do ln -fs $$p.opt $(DESTDIR)/$$p; done +else + install $(INSTALL_STUFF_BIN) $(DESTDIR) endif + for p in $(INSTALL_PROGRAMS_LINKS_MATITAC); do \ + ln -fs matitac $(DESTDIR)/$$p;\ + done + for p in $(INSTALL_PROGRAMS_LINKS_MATITA); do \ + ln -fs matita $(DESTDIR)/$$p;\ + done cp -a library/ $(DESTDIR)/ma/standard-library cp -a contribs/ $(DESTDIR)/ma/ +install_conclusion: + uninstall: rm -rf $(DESTDIR) @@ -293,9 +287,9 @@ ifeq ($(HAVE_OCAMLOPT),yes) static: $(STATIC_LINK) $(PROGRAMS_STATIC) else upx: - @echo "Native code compilation is disabled" + $(H)echo "Native code compilation is disabled" static: - @echo "Native code compilation is disabled" + $(H)echo "Native code compilation is disabled" endif $(STATIC_LINK): @@ -317,15 +311,15 @@ matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml $(STATIC_EXTRA_CLIBS) strip $@ matitadep.opt.static: matitac.opt.static - @test -f $@ || ln -s $< $@ + $(H)test -f $@ || ln -s $< $@ matitaclean.opt.static: matitac.opt.static - @test -f $@ || ln -s $< $@ + $(H)test -f $@ || ln -s $< $@ matitamake.opt.static: matitac.opt.static - @test -f $@ || ln -s $< $@ + $(H)test -f $@ || ln -s $< $@ cicbrowser.opt.static: matita.opt.static - @test -f $@ || ln -s $< $@ + $(H)test -f $@ || ln -s $< $@ cicbrowser.opt.static.upx: matita.opt.static.upx - @test -f $@ || ln -s $< $@ + $(H)test -f $@ || ln -s $< $@ %.upx: % cp $< $@ @@ -337,27 +331,36 @@ cicbrowser.opt.static.upx: matita.opt.static.upx tags: TAGS .PHONY: TAGS TAGS: - cd ..; otags -vi -r components/ matita/ + $(H)cd ..; otags -vi -r components/ matita/ #.depend: matitaGeneratedGui.ml matitaGeneratedGui.mli *.ml *.mli .PHONY: depend + depend: - $(OCAMLDEP) *.ml *.mli > .depend - -include .depend + $(H)echo " OCAMLDEP" + $(H)$(OCAMLDEP) *.ml *.mli > .depend +depend.opt: + $(H)echo " OCAMLDEP -native" + $(H)$(OCAMLDEP) -native *.ml *.mli > .depend + +ifneq ($(MAKECMDGOALS), depend) + ifneq ($(MAKECMDGOALS), depend.opt) + include .depend + endif +endif %.cmi: %.mli - @echo " OCAMLC $<" + $(H)echo " OCAMLC $<" $(H)$(OCAMLC) $(PKGS) -c $< %.cmo %.cmi: %.ml - @echo " OCAMLC $<" + $(H)echo " OCAMLC $<" $(H)$(OCAMLC) $(PKGS) -c $< %.cmx: %.ml - @echo " OCAMLOPT $<" + $(H)echo " OCAMLOPT $<" $(H)$(OCAMLOPT) $(PKGS) -c $< %.annot: %.ml - @echo " OCAMLC -dtypes $<" + $(H)echo " OCAMLC -dtypes $<" $(H)$(OCAMLC) -dtypes $(PKGS) -c $< $(CMOS): $(LIB_DEPS) diff --git a/matita/help/C/sec_install.xml b/matita/help/C/sec_install.xml index 70bd903cc..38218c190 100644 --- a/matita/help/C/sec_install.xml +++ b/matita/help/C/sec_install.xml @@ -333,7 +333,7 @@ world builds components needed by &appname; and &appname; itself - (in bytecode only or in both bytecode and native code depending + (in bytecode or native code depending on the availability of the OCaml native code compiler) @@ -343,10 +343,6 @@ uses the (just built) matitac compiler to build the &appname; standard library. - For this step you will need a working SQL database (for - indexing the standard library while you are compiling it). See - Database setup - for instructions on how to set it up. @@ -356,6 +352,11 @@ installs &appname; related tools, standard library and the needed runtime stuff in the proper places on the filesystem + For this step you will need a working SQL database (for + indexing the standard library while you are compiling it). See + Database setup + for instructions on how to set it up. + diff --git a/matita/matita.conf.xml.in b/matita/matita.conf.xml.in index 2d2f79fd6..37eb92561 100644 --- a/matita/matita.conf.xml.in +++ b/matita/matita.conf.xml.in @@ -34,7 +34,7 @@ --> @DBHOST@ helm - matita + prove-release
cic:/matita/ - file://@RT_BASE_DIR@/stantard-library/ + file://@RT_BASE_DIR@/xml/stantard-library/ ro diff --git a/matita/matita.glade b/matita/matita.glade index 1518409e8..96a016b95 100644 --- a/matita/matita.glade +++ b/matita/matita.glade @@ -2378,16 +2378,29 @@ GTK_CORNER_TOP_LEFT - + True - True - False - False - False - True - False - False - False + GTK_SHADOW_IN + + + + True + Not implemented. + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + PANGO_ELLIPSIZE_NONE + -1 + False + 0 + + diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml index f66ec6aff..b34f1dfc5 100644 --- a/matita/matitaInit.ml +++ b/matita/matitaInit.ml @@ -163,6 +163,8 @@ Options:" Usage: matitamake [ OPTION ... ] (init | clean | list | destroy | build) init Parameters: name (the name of the development, required) + root (the directory in which the delopment is rooted, + optional, default is current working directory) Description: tells matitamake that a new development radicated in the current working directory should be handled. clean @@ -240,7 +242,7 @@ let parse_cmdline init_status = "Turns off profiling printings"; "-bench", Arg.Unit (fun () -> Helm_registry.set_bool "matita.bench" true), - "Turns on timing prints"; + "Turns on parsable output on stdout, that is timings for matitac..."; "-preserve", Arg.Unit (fun () -> Helm_registry.set_bool "matita.preserve" true), "Turns off automatic baseuri cleaning"; diff --git a/matita/matitaMisc.ml b/matita/matitaMisc.ml index 0c4329e55..266aec526 100644 --- a/matita/matitaMisc.ml +++ b/matita/matitaMisc.ml @@ -150,3 +150,9 @@ let list_tl_at ?(equality=(==)) e l = | hd :: tl -> aux tl in aux l + +let shutup () = + HLog.set_log_callback (fun _ _ -> ()); + let out = open_out "/dev/null" in + Unix.dup2 (Unix.descr_of_out_channel out) (Unix.descr_of_out_channel stderr) + diff --git a/matita/matitaMisc.mli b/matita/matitaMisc.mli index 170a87c9b..b91275618 100644 --- a/matita/matitaMisc.mli +++ b/matita/matitaMisc.mli @@ -73,3 +73,6 @@ val singleton: (unit -> 'a) -> (unit -> 'a) (** given the base name of an image, returns its full path *) val image_path: string -> string + + (** 2>/dev/null, HLog = (fun _ -> ()) *) +val shutup: unit -> unit diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml index ca587690c..7efad7721 100644 --- a/matita/matitacLib.ml +++ b/matita/matitacLib.ml @@ -158,7 +158,7 @@ let pp_times fname bench_mode rc big_bang = begin let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in let r = Unix.gettimeofday () -. big_bang in - let extra = try Sys.getenv "DO_TESTS_EXTRA" with Not_found -> "" in + let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in let cc = if Str.string_match (Str.regexp "opt$") Sys.argv.(0) 0 then "matitac.opt" @@ -176,6 +176,15 @@ let pp_times fname bench_mode rc big_bang = in Printf.sprintf "%s %s %s" (fmt r) (fmt u) (fmt s) in + let fname = + match MatitamakeLib.development_for_dir (Filename.dirname fname) with + | None -> fname + | Some d -> + let rootlen = String.length(MatitamakeLib.root_for_development d)in + let fnamelen = String.length fname in + assert (fnamelen > rootlen); + String.sub fname rootlen (fnamelen - rootlen) + in let s = Printf.sprintf "%s\t%-30s %s\t%s\t%s" cc fname rc times extra in @@ -209,12 +218,7 @@ let main ~mode = in if Helm_registry.get_int "matita.verbosity" < 1 then HLog.set_log_callback newcb; - if bench_mode then - begin - HLog.set_log_callback (fun _ _ -> ()); - let out = open_out "/dev/null" in - Unix.dup2 (Unix.descr_of_out_channel out) (Unix.descr_of_out_channel stderr) - end; + if bench_mode then MatitaMisc.shutup (); let matita_debug = Helm_registry.get_bool "matita.debug" in try let time = Unix.time () in diff --git a/matita/matitaclean.ml b/matita/matitaclean.ml index d06671dc5..98d5ffa6b 100644 --- a/matita/matitaclean.ml +++ b/matita/matitaclean.ml @@ -57,6 +57,7 @@ let ask_confirmation _ = let main () = let _ = MatitaInit.initialize_all () in + if Helm_registry.get_bool "matita.bench" then MatitaMisc.shutup (); match Helm_registry.get_list Helm_registry.string "matita.args" with | [ "all" ] -> if Helm_registry.get_bool "matita.system" then diff --git a/matita/matitamakeLib.ml b/matita/matitamakeLib.ml index 10a543869..6af0414af 100644 --- a/matita/matitamakeLib.ml +++ b/matita/matitamakeLib.ml @@ -176,7 +176,9 @@ let make chdir args = let call_make ?matita_flags development target make = let matita_flags = match matita_flags with - | None -> (try Sys.getenv "MATITA_FLAGS" with Not_found -> "") + | None -> + (try Sys.getenv "MATITA_FLAGS" with Not_found -> + if Helm_registry.get_bool "matita.bench" then "-bench" else "") | Some s -> s in rebuild_makefile development; @@ -184,7 +186,7 @@ let call_make ?matita_flags development target make = let nodb = Helm_registry.get_opt_default Helm_registry.bool ~default:false "db.nodb" in - let flags = [] in + let flags = [] in let flags = flags @ if nodb then ["NODB=true"] else [] in let flags = try -- 2.39.2