From: Enrico Tassi Date: Wed, 15 Mar 2006 15:51:25 +0000 (+0000) Subject: more work for the release X-Git-Tag: 0.4.95@7852~1605 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d4c6f8464dc183326b7f7b4dc6171e69b482a26b;p=helm.git more work for the release --- 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/binaries/dump_db/dump.sh b/components/binaries/dump_db/dump.sh new file mode 100755 index 000000000..e7b43666e --- /dev/null +++ b/components/binaries/dump_db/dump.sh @@ -0,0 +1,20 @@ +ALL_TABLES=`../table_creator/table_creator list all` + +if [ -z "$1" ]; then + echo "Dumps to stdout some tables of a given db on mowgli." + echo "If no tables are given the dump will contain:" + echo " $ALL_TABLES" + echo "" + echo "usage: dump.sh dbname [tables...]" + echo "" + exit 1 +fi +DB=$1 +shift +if [ -z "$1" ]; then + TABLES=$ALL_TABLES +else + TABLES=$@ +fi + +mysqldump -e --add-drop-table -u helm -h mowgli.cs.unibo.it $DB $TABLES diff --git a/components/binaries/extractor/.depend b/components/binaries/extractor/.depend new file mode 100644 index 000000000..e69de29bb diff --git a/components/binaries/extractor/Makefile b/components/binaries/extractor/Makefile new file mode 100644 index 000000000..f7151e3cb --- /dev/null +++ b/components/binaries/extractor/Makefile @@ -0,0 +1,44 @@ +H=@ + +all: extractor extractor_manager + $(H)echo -n +opt: extractor.opt extractor_manager.opt + $(H)echo -n + +clean: + rm -f *.cm[ixo] *.[ao] extractor extractor.opt *.err *.out extractor_manager extractor_manager.opt + +extractor: extractor.ml + $(H)echo " OCAMLC $<" + $(H)$(OCAMLFIND) ocamlc \ + -thread -package mysql,helm-metadata -linkpkg -o $@ $< + +extractor.opt: extractor.ml + $(H)echo " OCAMLOPT $<" + $(H)$(OCAMLFIND) ocamlopt \ + -thread -package mysql,helm-metadata -linkpkg -o $@ $< + +extractor_manager: extractor_manager.ml + $(H)echo " OCAMLC $<" + $(H)$(OCAMLFIND) ocamlc \ + -thread -package mysql,helm-metadata -linkpkg -o $@ $< + +extractor_manager.opt: extractor_manager.ml + $(H)echo " OCAMLOPT $<" + $(H)$(OCAMLFIND) ocamlopt \ + -thread -package mysql,helm-metadata -linkpkg -o $@ $< + +export: extractor.opt extractor_manager.opt + nice -n 20 \ + 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/binaries/extractor/extractor.conf.xml b/components/binaries/extractor/extractor.conf.xml new file mode 100644 index 000000000..8dbc9a935 --- /dev/null +++ b/components/binaries/extractor/extractor.conf.xml @@ -0,0 +1,19 @@ + + +
+ .tmp/ +
+
+ localhost + helm + mowgli +
+
+ + file:///projects/helm/library/coq_contribs + + $(tmp.dir)/cache + $(tmp.dir)/maps + /projects/helm/xml/dtd +
+ diff --git a/components/binaries/extractor/extractor.ml b/components/binaries/extractor/extractor.ml new file mode 100644 index 000000000..418d5ff7c --- /dev/null +++ b/components/binaries/extractor/extractor.ml @@ -0,0 +1,78 @@ +let _ = Helm_registry.load_from "extractor.conf.xml" + +let usage () = + prerr_endline " + +!! This binary should not be called by hand, use the extractor_manager. !! + +usage: ./extractor[.opt] path owner + +path: the path for the getter maps +owner: the owner of the tables to update + +" + +let _ = + try + let _ = Sys.argv.(2), Sys.argv.(1) in + if Sys.argv.(1) = "-h"||Sys.argv.(1) = "-help"||Sys.argv.(1) = "--help" then + begin + usage (); + exit 1 + end + with + Invalid_argument _ -> usage (); exit 1 + +let owner = Sys.argv.(2) +let path = Sys.argv.(1) + +let main () = + print_endline (Printf.sprintf "%d alive on path:%s owner:%s" + (Unix.getpid()) path owner); + Helm_registry.set "tmp.dir" path; + Http_getter.init (); + let dbd = + HMysql.quick_connect + ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") + ~database:(Helm_registry.get "db.database") () + in + MetadataTypes.ownerize_tables owner; + let uris = + let ic = open_in (path ^ "/todo") in + let acc = ref [] in + (try + while true do + let l = input_line ic in + acc := l :: !acc + done + with + End_of_file -> ()); + close_in ic; + !acc + in + let len = float_of_int (List.length uris) in + let i = ref 0 in + let magic = 45 in + List.iter (fun u -> + incr i; + let perc = ((float_of_int !i) /. len *. 100.0) in + let l = String.length u in + let short = + if l < magic then + u ^ String.make (magic + 3 - l) ' ' + else + "..." ^ String.sub u (l - magic) magic + in + Printf.printf "%d (%d of %.0f = %3.1f%%): %s\n" + (Unix.getpid ()) !i len perc short; + flush stdout; + let uri = UriManager.uri_of_string u in + MetadataDb.index_obj ~dbd ~uri; + CicEnvironment.empty ()) + uris; + print_string "END "; Unix.system "date" +;; + +main () + diff --git a/components/binaries/extractor/extractor_manager.ml b/components/binaries/extractor/extractor_manager.ml new file mode 100644 index 000000000..05393b63e --- /dev/null +++ b/components/binaries/extractor/extractor_manager.ml @@ -0,0 +1,306 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +(* HELPERS *) + +let create_all dbd = + let obj_tbl = MetadataTypes.obj_tbl () in + let sort_tbl = MetadataTypes.sort_tbl () in + let rel_tbl = MetadataTypes.rel_tbl () in + let name_tbl = MetadataTypes.name_tbl () in + let count_tbl = MetadataTypes.count_tbl () in + let tbls = [ + (obj_tbl,`RefObj) ; (sort_tbl,`RefSort) ; (rel_tbl,`RefRel) ; + (name_tbl,`ObjectName) ; (count_tbl,`Count) ] + in + let statements = + (SqlStatements.create_tables tbls) @ (SqlStatements.create_indexes tbls) + in + List.iter (fun statement -> + try + ignore (Mysql.exec dbd statement) + with + exn -> + let status = Mysql.status dbd in + match status with + | Mysql.StatusError Mysql.Table_exists_error -> () + | Mysql.StatusError _ -> raise exn + | _ -> () + ) statements + +let drop_all dbd = + let obj_tbl = MetadataTypes.obj_tbl () in + let sort_tbl = MetadataTypes.sort_tbl () in + let rel_tbl = MetadataTypes.rel_tbl () in + let name_tbl = MetadataTypes.name_tbl () in + let count_tbl = MetadataTypes.count_tbl () in + let tbls = [ + (obj_tbl,`RefObj) ; (sort_tbl,`RefSort) ; (rel_tbl,`RefRel) ; + (name_tbl,`ObjectName) ; (count_tbl,`Count) ] + in + let statements = + (SqlStatements.drop_tables tbls) @ (SqlStatements.drop_indexes tbls) + in + List.iter (fun statement -> + try + ignore (Mysql.exec dbd statement) + with Mysql.Error _ as exn -> + match Mysql.errno dbd with + | Mysql.Bad_table_error + | Mysql.No_such_index | Mysql.No_such_table -> () + | _ -> raise exn + ) statements + +let slash_RE = Str.regexp "/" + +let partition l = + let l = List.fast_sort Pervasives.compare l in + let matches s1 s2 = + let l1,l2 = Str.split slash_RE s1, Str.split slash_RE s2 in + match l1,l2 with + | _::x::_,_::y::_ -> x = y + | _ -> false + in + let rec chunk l = + match l with + | [] -> [],[] + | h::(h1::tl as rest) when matches h h1 -> + let ch,todo = chunk rest in + (h::ch),todo + | h::(h1::tl as rest)-> [h],rest + | h::_ -> [h],[] + in + let rec split l = + let ch, todo = chunk l in + match todo with + | [] -> [ch] + | _ -> ch :: split todo + in + split l + + +(* ARGV PARSING *) + +let _ = + try + if Sys.argv.(1) = "-h"||Sys.argv.(1) = "-help"||Sys.argv.(1) = "--help" then + begin + prerr_endline " +usage: ./extractor_manager[.opt] [processes] [owner] + +defaults: + processes = 2 + owner = NEW + +"; + exit 1 + end + with Invalid_argument _ -> () + +let processes = + try + int_of_string (Sys.argv.(1)) + with + Invalid_argument _ -> 2 + +let owner = + try + Sys.argv.(2) + with Invalid_argument _ -> "NEW" + +let create_peons i = + let rec aux = function + | 0 -> [] + | n -> (n,0) :: aux (n-1) + in + ref (aux i) + +let is_a_peon_idle peons = + List.exists (fun (_,x) -> x = 0) !peons + +let get_ide_peon peons = + let p = fst(List.find (fun (_,x) -> x = 0) !peons) in + peons := List.filter (fun (x,_) -> x <> p) !peons; + p + +let assign_peon peon pid peons = + peons := (peon,pid) :: !peons + +let wait_a_peon peons = + let pid,status = Unix.wait () in + (match status with + | Unix.WEXITED 0 -> () + | Unix.WEXITED s -> + prerr_endline (Printf.sprintf "PEON %d EXIT STATUS %d" pid s) + | Unix.WSIGNALED s -> + prerr_endline + (Printf.sprintf "PEON %d HAD A PROBLEM, KILLED BY SIGNAL %d" pid s) + | Unix.WSTOPPED s -> + prerr_endline + (Printf.sprintf "PEON %d HAD A PROBLEM, STOPPED BY %d" pid s)); + let p = fst(List.find (fun (_,x) -> x = pid) !peons) in + peons := List.filter (fun (x,_) -> x <> p) !peons; + peons := (p,0) :: !peons + +let is_a_peon_busy peons = + List.exists (fun (_,x) -> x <> 0) !peons + +(* MAIN *) +let main () = + Helm_registry.load_from "extractor.conf.xml"; + Http_getter.init (); + print_endline "Updating the getter...."; + let base = (Helm_registry.get "tmp.dir") ^ "/maps" in + let formats i = + (Helm_registry.get "tmp.dir") ^ "/"^(string_of_int i)^"/maps" + in + for i = 1 to processes do + let fmt = formats i in + ignore(Unix.system ("rm -rf " ^ fmt)); + ignore(Unix.system ("mkdir -p " ^ fmt)); + ignore(Unix.system ("cp -r " ^ base ^ " " ^ fmt ^ "/../")); + done; + let dbd = + Mysql.quick_connect + ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") + ~database:(Helm_registry.get "db.database") () + in + MetadataTypes.ownerize_tables owner; + let uri_RE = Str.regexp ".*\\(ind\\|var\\|con\\)$" in + drop_all dbd; + create_all dbd; + let uris = Http_getter.getalluris () in + let uris = List.filter (fun u -> Str.string_match uri_RE u 0) uris in + let todo = partition uris in + let cur = ref 0 in + let tot = List.length todo in + let peons = create_peons processes in + print_string "START "; flush stdout; + ignore(Unix.system "date"); + while !cur < tot do + if is_a_peon_idle peons then + let peon = get_ide_peon peons in + let fmt = formats peon in + let oc = open_out (fmt ^ "/../todo") in + List.iter (fun s -> output_string oc (s^"\n")) (List.nth todo !cur); + close_out oc; + let pid = Unix.fork () in + if pid = 0 then + Unix.execv + "./extractor.opt" [| "./extractor.opt" ; fmt ^ "/../" ; owner|] + else + begin + assign_peon peon pid peons; + incr cur + end + else + wait_a_peon peons + done; + while is_a_peon_busy peons do wait_a_peon peons done; + print_string "END "; flush stdout; + ignore(Unix.system "date"); + (* and now the rename table stuff *) + let obj_tbl = MetadataTypes.library_obj_tbl in + let sort_tbl = MetadataTypes.library_sort_tbl in + let rel_tbl = MetadataTypes.library_rel_tbl in + let name_tbl = MetadataTypes.library_name_tbl in + let count_tbl = MetadataTypes.library_count_tbl in + let hits_tbl = MetadataTypes.library_hits_tbl in + let obj_tbl_b = obj_tbl ^ "_BACKUP" in + let sort_tbl_b = sort_tbl ^ "_BACKUP" in + let rel_tbl_b = rel_tbl ^ "_BACKUP" in + let name_tbl_b = name_tbl ^ "_BACKUP" in + let count_tbl_b = count_tbl ^ "_BACKUP" in + let obj_tbl_c = MetadataTypes.obj_tbl () in + let sort_tbl_c = MetadataTypes.sort_tbl () in + let rel_tbl_c = MetadataTypes.rel_tbl () in + let name_tbl_c = MetadataTypes.name_tbl () in + let count_tbl_c = MetadataTypes.count_tbl () in + let stats = + SqlStatements.drop_tables [ + (obj_tbl_b,`RefObj); + (sort_tbl_b,`RefSort); + (rel_tbl_b,`RefRel); + (name_tbl_b,`ObjectName); + (count_tbl_b,`Count); + (hits_tbl,`Hits) ] @ + SqlStatements.drop_indexes [ + (obj_tbl,`RefObj); + (sort_tbl,`RefSort); + (rel_tbl,`RefRel); + (name_tbl,`ObjectName); + (count_tbl,`Count); + (obj_tbl_c,`RefObj); + (sort_tbl_c,`RefSort); + (rel_tbl_c,`RefRel); + (name_tbl_c,`ObjectName); + (count_tbl_c,`Count); + (hits_tbl,`Hits) ] @ + SqlStatements.rename_tables [ + (obj_tbl,obj_tbl_b); + (sort_tbl,sort_tbl_b); + (rel_tbl,rel_tbl_b); + (name_tbl,name_tbl_b); + (count_tbl,count_tbl_b) ] @ + SqlStatements.rename_tables [ + (obj_tbl_c,obj_tbl); + (sort_tbl_c,sort_tbl); + (rel_tbl_c,rel_tbl); + (name_tbl_c,name_tbl); + (count_tbl_c,count_tbl) ] @ + SqlStatements.create_tables [ + (hits_tbl,`Hits) ] @ + SqlStatements.fill_hits obj_tbl hits_tbl @ + SqlStatements.create_indexes [ + (obj_tbl,`RefObj); + (sort_tbl,`RefSort); + (rel_tbl,`RefRel); + (name_tbl,`ObjectName); + (count_tbl,`Count); + (hits_tbl,`Hits) ] + in + List.iter (fun statement -> + try +(* prerr_endline statement;*) + ignore (Mysql.exec dbd statement) + with exn -> + let status = Mysql.status dbd in + match status with + | Mysql.StatusError Mysql.Table_exists_error + | Mysql.StatusError Mysql.Bad_table_error + | Mysql.StatusError Mysql.Cant_drop_field_or_key + | Mysql.StatusError Mysql.Unknown_table -> () + | Mysql.StatusError status -> +(* prerr_endline (string_of_int (Obj.magic status));*) + prerr_endline (Printexc.to_string exn); + raise exn + | _ -> + prerr_endline (Printexc.to_string exn); + ()) + stats +;; + +main () 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/binaries/table_creator/Makefile b/components/binaries/table_creator/Makefile new file mode 100644 index 000000000..15cf1863a --- /dev/null +++ b/components/binaries/table_creator/Makefile @@ -0,0 +1,45 @@ +H=@ + +REQUIRES = mysql helm-metadata + +INTERFACE_FILES = +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_CLEAN = \ + table_creator table_creator.opt table_destructor table_destructor.opt + +all: table_creator table_destructor + $(H)echo -n +opt: table_creator.opt table_destructor.opt + $(H)echo -n + +table_creator: table_creator.ml + $(H)echo " OCAMLC $<" + $(H)$(OCAMLFIND) ocamlc \ + -thread -package mysql,helm-metadata -linkpkg -o $@ $< + +table_destructor: table_creator + $(H)ln -f $< $@ + +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 + $(H)ln -f $< $@ + +clean: + $(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/binaries/table_creator/sync_db.sh b/components/binaries/table_creator/sync_db.sh new file mode 100755 index 000000000..7b201382a --- /dev/null +++ b/components/binaries/table_creator/sync_db.sh @@ -0,0 +1,28 @@ +#!/bin/sh + +# sync metadata from a source database (usually "mowgli") to a target one +# (usually "matita") +# Created: Fri, 13 May 2005 13:50:16 +0200 zacchiro +# Last-Modified: Fri, 13 May 2005 13:50:16 +0200 zacchiro + +SOURCE_DB="mowgli" +TARGET_DB="matita" +MYSQL_FLAGS="-u helm -h localhost" + +MYSQL="mysql $MYSQL_FLAGS -f" +MYSQLDUMP="mysqldump $MYSQL_FLAGS" +MYSQLRESTORE="mysqlrestore $MYSQL_FLAGS" +TABLES=`./table_creator list all` +DUMP="${SOURCE_DB}_dump.gz" + +echo "Dumping source db $SOURCE_DB ..." +$MYSQLDUMP $SOURCE_DB $TABLES | gzip -c > $DUMP +echo "Destroying old tables in target db $TARGET_DB ..." +./table_destructor table all | $MYSQL $TARGET_DB +echo "Creating table structure in target db $TARGET_DB ..." +echo "Filling target db $TARGET_DB ..." +zcat $DUMP | $MYSQL $TARGET_DB +./table_creator index all | $MYSQL $TARGET_DB +rm $DUMP +echo "Done." + diff --git a/components/binaries/table_creator/table_creator.ml b/components/binaries/table_creator/table_creator.ml new file mode 100644 index 000000000..423edfb27 --- /dev/null +++ b/components/binaries/table_creator/table_creator.ml @@ -0,0 +1,83 @@ + +open Printf + +let map = + (MetadataTypes.library_obj_tbl,`RefObj) :: + (MetadataTypes.library_sort_tbl,`RefSort) :: + (MetadataTypes.library_rel_tbl,`RefRel) :: + (MetadataTypes.library_name_tbl,`ObjectName) :: + (MetadataTypes.library_hits_tbl,`Hits) :: + (MetadataTypes.library_count_tbl,`Count) :: [] + +let usage argv_o = + prerr_string "\nusage:"; + prerr_string ("\t" ^ argv_o ^ " what tablename[=rename]\n"); + prerr_string ("\t" ^ argv_o ^ " what all\n\n"); + prerr_endline "what:"; + prerr_endline "\tlist\tlist table names"; + prerr_endline "\ttable\toutput SQL regarding tables"; + prerr_endline "\tindex\toutput SQL regarding indexes"; + prerr_endline "\tfill\toutput SQL filling tables (only \"hits\" supported)\n"; + prerr_string "known tables:\n\t"; + List.iter (fun (n,_) -> prerr_string (" " ^ n)) map; + prerr_endline "\n" + +let eq_RE = Str.regexp "=" + +let parse_args l = + List.map (fun s -> + let parts = Str.split eq_RE s in + let len = List.length parts in + assert (len = 1 || len = 2); + if len = 1 then (s,s) else (List.nth parts 0, List.nth parts 1)) + l + +let destructor_RE = Str.regexp "table_destructor\\(\\|\\.opt\\)$" + +let am_i_destructor () = + try + let _ = Str.search_forward destructor_RE Sys.argv.(0) 0 in true + with Not_found -> false + +let main () = + let len = Array.length Sys.argv in + if len < 3 then + begin + usage Sys.argv.(0); + exit 1 + end + else + begin + let tab,idx,fill = + if am_i_destructor () then + (SqlStatements.drop_tables,SqlStatements.drop_indexes, + fun _ t -> [sprintf "DELETE * FROM %s;" t]) + else + (SqlStatements.create_tables,SqlStatements.create_indexes, + SqlStatements.fill_hits) + in + let from = 2 in + let what = + match Sys.argv.(1) with + | "list" -> `List + | "index" -> `Index + | "table" -> `Table + | "fill" -> `Fill + | _ -> failwith "what must be one of \"index\", \"table\", \"fill\"" + in + let todo = Array.to_list (Array.sub Sys.argv from (len - from)) in + let todo = match todo with ["all"] -> List.map fst map | todo -> todo in + let todo = parse_args todo in + let todo = List.map (fun (x,name) -> name, (List.assoc x map)) todo in + match what with + | `Index -> print_endline (String.concat "\n" (idx todo)) + | `Table -> print_endline (String.concat "\n" (tab todo)) + | `Fill -> + print_endline (String.concat "\n" + (fill MetadataTypes.library_obj_tbl MetadataTypes.library_hits_tbl)) + | `List -> print_endline (String.concat " " (List.map fst map)) + end + +let _ = main () + + diff --git a/components/binaries/utilities/Makefile b/components/binaries/utilities/Makefile new file mode 100644 index 000000000..c22d2a99d --- /dev/null +++ b/components/binaries/utilities/Makefile @@ -0,0 +1,29 @@ +H=@ + +UTILITIES = create_environment parse_library list_uris +UTILITIES_OPT = $(patsubst %,%.opt,$(UTILITIES)) +LINKOPTS = -linkpkg -thread +LIBS = helm-cic_proof_checking +OCAMLC = $(OCAMLFIND) ocamlc $(LINKOPTS) -package $(LIBS) +OCAMLOPT = $(OCAMLFIND) opt $(LINKOPTS) -package $(LIBS) +all: $(UTILITIES) + $(H)echo -n +opt: $(UTILITIES_OPT) + $(H)echo -n +%: %.ml + $(H)echo " OCAMLC $<" + $(H)$(OCAMLC) -o $@ $< +%.opt: %.ml + $(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/binaries/utilities/create_environment.ml b/components/binaries/utilities/create_environment.ml new file mode 100644 index 000000000..8a8524d24 --- /dev/null +++ b/components/binaries/utilities/create_environment.ml @@ -0,0 +1,73 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +let trust = true + +let outfname = + match Sys.argv.(1) with + | "-help" | "--help" | "-h" | "--h" -> + print_endline + ("Usage: create_environment \n" ^ + " is the file where environment will be dumped\n" ^ + " is the file containing the URIs, one per line,\n" ^ + " that will be typechecked. Could be \"-\" for\n" ^ + " standard input"); + flush stdout; + exit 0 + | f -> f +let _ = + CicEnvironment.set_trust (fun _ -> trust); + Helm_registry.set "getter.mode" "remote"; + Helm_registry.set "getter.url" "http://mowgli.cs.unibo.it:58081/"; + Sys.catch_break true; + if Sys.file_exists outfname then begin + let ic = open_in outfname in + CicEnvironment.restore_from_channel ic; + close_in ic + end +let urifname = + try + Sys.argv.(2) + with Invalid_argument _ -> "-" +let ic = + match urifname with + | "-" -> stdin + | fname -> open_in fname +let _ = + try + while true do +(* try *) + let uri = input_line ic in + print_endline uri; + flush stdout; + let uri = UriManager.uri_of_string uri in + ignore (CicTypeChecker.typecheck uri) +(* with Sys.Break -> () *) + done + with End_of_file | Sys.Break -> + let oc = open_out outfname in + CicEnvironment.dump_to_channel oc; + close_out oc + diff --git a/components/binaries/utilities/list_uris.ml b/components/binaries/utilities/list_uris.ml new file mode 100644 index 000000000..90ea51616 --- /dev/null +++ b/components/binaries/utilities/list_uris.ml @@ -0,0 +1,30 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +let ic = open_in Sys.argv.(1) in +CicEnvironment.restore_from_channel ic; +List.iter + (fun uri -> print_endline (UriManager.string_of_uri uri)) + (CicEnvironment.list_uri ()) diff --git a/components/binaries/utilities/parse_library.ml b/components/binaries/utilities/parse_library.ml new file mode 100644 index 000000000..1d65291cb --- /dev/null +++ b/components/binaries/utilities/parse_library.ml @@ -0,0 +1,54 @@ +(* Copyright (C) 2004-2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +let trust = true + +let _ = + CicEnvironment.set_trust (fun _ -> trust); + Helm_registry.set "getter.mode" "remote"; + Helm_registry.set "getter.url" "http://mowgli.cs.unibo.it:58081/" +let urifname = + try + Sys.argv.(1) + with Invalid_argument _ -> "-" +let ic = + match urifname with + | "-" -> stdin + | fname -> open_in fname +let _ = + try + while true do + try + let uri = input_line ic in + prerr_endline uri; + let uri = UriManager.uri_of_string uri in + ignore (CicEnvironment.get_obj CicUniv.empty_ugraph uri) +(* with Sys.Break -> () *) + with + | End_of_file -> raise End_of_file + | exn -> () + done + with End_of_file -> Unix.sleep max_int + 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/cic_proof_checking/utilities/Makefile b/components/cic_proof_checking/utilities/Makefile deleted file mode 100644 index 383391d70..000000000 --- a/components/cic_proof_checking/utilities/Makefile +++ /dev/null @@ -1,21 +0,0 @@ -UTILITIES = create_environment parse_library list_uris -UTILITIES_OPT = $(patsubst %,%.opt,$(UTILITIES)) -LINKOPTS = -linkpkg -thread -LIBS = helm-cic_proof_checking -OCAMLC = $(OCAMLFIND) ocamlc $(LINKOPTS) -package $(LIBS) -OCAMLOPT = $(OCAMLFIND) opt $(LINKOPTS) -package $(LIBS) -all: $(UTILITIES) - @echo -n -opt: $(UTILITIES_OPT) - @echo -n -%: %.ml - @echo " OCAMLC $<" - @$(OCAMLC) -o $@ $< -%.opt: %.ml - @echo " OCAMLOPT $<" - @$(OCAMLOPT) -o $@ $< -clean: - rm -f $(UTILITIES) $(UTILITIES_OPT) *.cm[iox] *.o - -include ../../../Makefile.defs - diff --git a/components/cic_proof_checking/utilities/create_environment.ml b/components/cic_proof_checking/utilities/create_environment.ml deleted file mode 100644 index 8a8524d24..000000000 --- a/components/cic_proof_checking/utilities/create_environment.ml +++ /dev/null @@ -1,73 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -let trust = true - -let outfname = - match Sys.argv.(1) with - | "-help" | "--help" | "-h" | "--h" -> - print_endline - ("Usage: create_environment \n" ^ - " is the file where environment will be dumped\n" ^ - " is the file containing the URIs, one per line,\n" ^ - " that will be typechecked. Could be \"-\" for\n" ^ - " standard input"); - flush stdout; - exit 0 - | f -> f -let _ = - CicEnvironment.set_trust (fun _ -> trust); - Helm_registry.set "getter.mode" "remote"; - Helm_registry.set "getter.url" "http://mowgli.cs.unibo.it:58081/"; - Sys.catch_break true; - if Sys.file_exists outfname then begin - let ic = open_in outfname in - CicEnvironment.restore_from_channel ic; - close_in ic - end -let urifname = - try - Sys.argv.(2) - with Invalid_argument _ -> "-" -let ic = - match urifname with - | "-" -> stdin - | fname -> open_in fname -let _ = - try - while true do -(* try *) - let uri = input_line ic in - print_endline uri; - flush stdout; - let uri = UriManager.uri_of_string uri in - ignore (CicTypeChecker.typecheck uri) -(* with Sys.Break -> () *) - done - with End_of_file | Sys.Break -> - let oc = open_out outfname in - CicEnvironment.dump_to_channel oc; - close_out oc - diff --git a/components/cic_proof_checking/utilities/list_uris.ml b/components/cic_proof_checking/utilities/list_uris.ml deleted file mode 100644 index 90ea51616..000000000 --- a/components/cic_proof_checking/utilities/list_uris.ml +++ /dev/null @@ -1,30 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -let ic = open_in Sys.argv.(1) in -CicEnvironment.restore_from_channel ic; -List.iter - (fun uri -> print_endline (UriManager.string_of_uri uri)) - (CicEnvironment.list_uri ()) diff --git a/components/cic_proof_checking/utilities/parse_library.ml b/components/cic_proof_checking/utilities/parse_library.ml deleted file mode 100644 index 1d65291cb..000000000 --- a/components/cic_proof_checking/utilities/parse_library.ml +++ /dev/null @@ -1,54 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -let trust = true - -let _ = - CicEnvironment.set_trust (fun _ -> trust); - Helm_registry.set "getter.mode" "remote"; - Helm_registry.set "getter.url" "http://mowgli.cs.unibo.it:58081/" -let urifname = - try - Sys.argv.(1) - with Invalid_argument _ -> "-" -let ic = - match urifname with - | "-" -> stdin - | fname -> open_in fname -let _ = - try - while true do - try - let uri = input_line ic in - prerr_endline uri; - let uri = UriManager.uri_of_string uri in - ignore (CicEnvironment.get_obj CicUniv.empty_ugraph uri) -(* with Sys.Break -> () *) - with - | End_of_file -> raise End_of_file - | exn -> () - done - with End_of_file -> Unix.sleep max_int - 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/dump_db/dump.sh b/components/metadata/dump_db/dump.sh deleted file mode 100755 index e7b43666e..000000000 --- a/components/metadata/dump_db/dump.sh +++ /dev/null @@ -1,20 +0,0 @@ -ALL_TABLES=`../table_creator/table_creator list all` - -if [ -z "$1" ]; then - echo "Dumps to stdout some tables of a given db on mowgli." - echo "If no tables are given the dump will contain:" - echo " $ALL_TABLES" - echo "" - echo "usage: dump.sh dbname [tables...]" - echo "" - exit 1 -fi -DB=$1 -shift -if [ -z "$1" ]; then - TABLES=$ALL_TABLES -else - TABLES=$@ -fi - -mysqldump -e --add-drop-table -u helm -h mowgli.cs.unibo.it $DB $TABLES diff --git a/components/metadata/extractor/.depend b/components/metadata/extractor/.depend deleted file mode 100644 index e69de29bb..000000000 diff --git a/components/metadata/extractor/Makefile b/components/metadata/extractor/Makefile deleted file mode 100644 index 579a5655f..000000000 --- a/components/metadata/extractor/Makefile +++ /dev/null @@ -1,36 +0,0 @@ - -all: extractor extractor_manager - @echo -n -opt: extractor.opt extractor_manager.opt - @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 \ - -thread -package mysql,helm-metadata -linkpkg -o $@ $< - -extractor.opt: extractor.ml - @echo " OCAMLOPT $<" - @$(OCAMLFIND) ocamlopt \ - -thread -package mysql,helm-metadata -linkpkg -o $@ $< - -extractor_manager: extractor_manager.ml - @echo " OCAMLC $<" - @$(OCAMLFIND) ocamlc \ - -thread -package mysql,helm-metadata -linkpkg -o $@ $< - -extractor_manager.opt: extractor_manager.ml - @echo " OCAMLOPT $<" - @$(OCAMLFIND) ocamlopt \ - -thread -package mysql,helm-metadata -linkpkg -o $@ $< - -export: extractor.opt extractor_manager.opt - nice -n 20 \ - time \ - ./extractor_manager.opt 1>export.out 2>export.err - -include .depend -include ../../../Makefile.defs diff --git a/components/metadata/extractor/extractor.conf.xml b/components/metadata/extractor/extractor.conf.xml deleted file mode 100644 index 8dbc9a935..000000000 --- a/components/metadata/extractor/extractor.conf.xml +++ /dev/null @@ -1,19 +0,0 @@ - - -
- .tmp/ -
-
- localhost - helm - mowgli -
-
- - file:///projects/helm/library/coq_contribs - - $(tmp.dir)/cache - $(tmp.dir)/maps - /projects/helm/xml/dtd -
- diff --git a/components/metadata/extractor/extractor.ml b/components/metadata/extractor/extractor.ml deleted file mode 100644 index 418d5ff7c..000000000 --- a/components/metadata/extractor/extractor.ml +++ /dev/null @@ -1,78 +0,0 @@ -let _ = Helm_registry.load_from "extractor.conf.xml" - -let usage () = - prerr_endline " - -!! This binary should not be called by hand, use the extractor_manager. !! - -usage: ./extractor[.opt] path owner - -path: the path for the getter maps -owner: the owner of the tables to update - -" - -let _ = - try - let _ = Sys.argv.(2), Sys.argv.(1) in - if Sys.argv.(1) = "-h"||Sys.argv.(1) = "-help"||Sys.argv.(1) = "--help" then - begin - usage (); - exit 1 - end - with - Invalid_argument _ -> usage (); exit 1 - -let owner = Sys.argv.(2) -let path = Sys.argv.(1) - -let main () = - print_endline (Printf.sprintf "%d alive on path:%s owner:%s" - (Unix.getpid()) path owner); - Helm_registry.set "tmp.dir" path; - Http_getter.init (); - let dbd = - HMysql.quick_connect - ~host:(Helm_registry.get "db.host") - ~user:(Helm_registry.get "db.user") - ~database:(Helm_registry.get "db.database") () - in - MetadataTypes.ownerize_tables owner; - let uris = - let ic = open_in (path ^ "/todo") in - let acc = ref [] in - (try - while true do - let l = input_line ic in - acc := l :: !acc - done - with - End_of_file -> ()); - close_in ic; - !acc - in - let len = float_of_int (List.length uris) in - let i = ref 0 in - let magic = 45 in - List.iter (fun u -> - incr i; - let perc = ((float_of_int !i) /. len *. 100.0) in - let l = String.length u in - let short = - if l < magic then - u ^ String.make (magic + 3 - l) ' ' - else - "..." ^ String.sub u (l - magic) magic - in - Printf.printf "%d (%d of %.0f = %3.1f%%): %s\n" - (Unix.getpid ()) !i len perc short; - flush stdout; - let uri = UriManager.uri_of_string u in - MetadataDb.index_obj ~dbd ~uri; - CicEnvironment.empty ()) - uris; - print_string "END "; Unix.system "date" -;; - -main () - diff --git a/components/metadata/extractor/extractor_manager.ml b/components/metadata/extractor/extractor_manager.ml deleted file mode 100644 index 05393b63e..000000000 --- a/components/metadata/extractor/extractor_manager.ml +++ /dev/null @@ -1,306 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* HELPERS *) - -let create_all dbd = - let obj_tbl = MetadataTypes.obj_tbl () in - let sort_tbl = MetadataTypes.sort_tbl () in - let rel_tbl = MetadataTypes.rel_tbl () in - let name_tbl = MetadataTypes.name_tbl () in - let count_tbl = MetadataTypes.count_tbl () in - let tbls = [ - (obj_tbl,`RefObj) ; (sort_tbl,`RefSort) ; (rel_tbl,`RefRel) ; - (name_tbl,`ObjectName) ; (count_tbl,`Count) ] - in - let statements = - (SqlStatements.create_tables tbls) @ (SqlStatements.create_indexes tbls) - in - List.iter (fun statement -> - try - ignore (Mysql.exec dbd statement) - with - exn -> - let status = Mysql.status dbd in - match status with - | Mysql.StatusError Mysql.Table_exists_error -> () - | Mysql.StatusError _ -> raise exn - | _ -> () - ) statements - -let drop_all dbd = - let obj_tbl = MetadataTypes.obj_tbl () in - let sort_tbl = MetadataTypes.sort_tbl () in - let rel_tbl = MetadataTypes.rel_tbl () in - let name_tbl = MetadataTypes.name_tbl () in - let count_tbl = MetadataTypes.count_tbl () in - let tbls = [ - (obj_tbl,`RefObj) ; (sort_tbl,`RefSort) ; (rel_tbl,`RefRel) ; - (name_tbl,`ObjectName) ; (count_tbl,`Count) ] - in - let statements = - (SqlStatements.drop_tables tbls) @ (SqlStatements.drop_indexes tbls) - in - List.iter (fun statement -> - try - ignore (Mysql.exec dbd statement) - with Mysql.Error _ as exn -> - match Mysql.errno dbd with - | Mysql.Bad_table_error - | Mysql.No_such_index | Mysql.No_such_table -> () - | _ -> raise exn - ) statements - -let slash_RE = Str.regexp "/" - -let partition l = - let l = List.fast_sort Pervasives.compare l in - let matches s1 s2 = - let l1,l2 = Str.split slash_RE s1, Str.split slash_RE s2 in - match l1,l2 with - | _::x::_,_::y::_ -> x = y - | _ -> false - in - let rec chunk l = - match l with - | [] -> [],[] - | h::(h1::tl as rest) when matches h h1 -> - let ch,todo = chunk rest in - (h::ch),todo - | h::(h1::tl as rest)-> [h],rest - | h::_ -> [h],[] - in - let rec split l = - let ch, todo = chunk l in - match todo with - | [] -> [ch] - | _ -> ch :: split todo - in - split l - - -(* ARGV PARSING *) - -let _ = - try - if Sys.argv.(1) = "-h"||Sys.argv.(1) = "-help"||Sys.argv.(1) = "--help" then - begin - prerr_endline " -usage: ./extractor_manager[.opt] [processes] [owner] - -defaults: - processes = 2 - owner = NEW - -"; - exit 1 - end - with Invalid_argument _ -> () - -let processes = - try - int_of_string (Sys.argv.(1)) - with - Invalid_argument _ -> 2 - -let owner = - try - Sys.argv.(2) - with Invalid_argument _ -> "NEW" - -let create_peons i = - let rec aux = function - | 0 -> [] - | n -> (n,0) :: aux (n-1) - in - ref (aux i) - -let is_a_peon_idle peons = - List.exists (fun (_,x) -> x = 0) !peons - -let get_ide_peon peons = - let p = fst(List.find (fun (_,x) -> x = 0) !peons) in - peons := List.filter (fun (x,_) -> x <> p) !peons; - p - -let assign_peon peon pid peons = - peons := (peon,pid) :: !peons - -let wait_a_peon peons = - let pid,status = Unix.wait () in - (match status with - | Unix.WEXITED 0 -> () - | Unix.WEXITED s -> - prerr_endline (Printf.sprintf "PEON %d EXIT STATUS %d" pid s) - | Unix.WSIGNALED s -> - prerr_endline - (Printf.sprintf "PEON %d HAD A PROBLEM, KILLED BY SIGNAL %d" pid s) - | Unix.WSTOPPED s -> - prerr_endline - (Printf.sprintf "PEON %d HAD A PROBLEM, STOPPED BY %d" pid s)); - let p = fst(List.find (fun (_,x) -> x = pid) !peons) in - peons := List.filter (fun (x,_) -> x <> p) !peons; - peons := (p,0) :: !peons - -let is_a_peon_busy peons = - List.exists (fun (_,x) -> x <> 0) !peons - -(* MAIN *) -let main () = - Helm_registry.load_from "extractor.conf.xml"; - Http_getter.init (); - print_endline "Updating the getter...."; - let base = (Helm_registry.get "tmp.dir") ^ "/maps" in - let formats i = - (Helm_registry.get "tmp.dir") ^ "/"^(string_of_int i)^"/maps" - in - for i = 1 to processes do - let fmt = formats i in - ignore(Unix.system ("rm -rf " ^ fmt)); - ignore(Unix.system ("mkdir -p " ^ fmt)); - ignore(Unix.system ("cp -r " ^ base ^ " " ^ fmt ^ "/../")); - done; - let dbd = - Mysql.quick_connect - ~host:(Helm_registry.get "db.host") - ~user:(Helm_registry.get "db.user") - ~database:(Helm_registry.get "db.database") () - in - MetadataTypes.ownerize_tables owner; - let uri_RE = Str.regexp ".*\\(ind\\|var\\|con\\)$" in - drop_all dbd; - create_all dbd; - let uris = Http_getter.getalluris () in - let uris = List.filter (fun u -> Str.string_match uri_RE u 0) uris in - let todo = partition uris in - let cur = ref 0 in - let tot = List.length todo in - let peons = create_peons processes in - print_string "START "; flush stdout; - ignore(Unix.system "date"); - while !cur < tot do - if is_a_peon_idle peons then - let peon = get_ide_peon peons in - let fmt = formats peon in - let oc = open_out (fmt ^ "/../todo") in - List.iter (fun s -> output_string oc (s^"\n")) (List.nth todo !cur); - close_out oc; - let pid = Unix.fork () in - if pid = 0 then - Unix.execv - "./extractor.opt" [| "./extractor.opt" ; fmt ^ "/../" ; owner|] - else - begin - assign_peon peon pid peons; - incr cur - end - else - wait_a_peon peons - done; - while is_a_peon_busy peons do wait_a_peon peons done; - print_string "END "; flush stdout; - ignore(Unix.system "date"); - (* and now the rename table stuff *) - let obj_tbl = MetadataTypes.library_obj_tbl in - let sort_tbl = MetadataTypes.library_sort_tbl in - let rel_tbl = MetadataTypes.library_rel_tbl in - let name_tbl = MetadataTypes.library_name_tbl in - let count_tbl = MetadataTypes.library_count_tbl in - let hits_tbl = MetadataTypes.library_hits_tbl in - let obj_tbl_b = obj_tbl ^ "_BACKUP" in - let sort_tbl_b = sort_tbl ^ "_BACKUP" in - let rel_tbl_b = rel_tbl ^ "_BACKUP" in - let name_tbl_b = name_tbl ^ "_BACKUP" in - let count_tbl_b = count_tbl ^ "_BACKUP" in - let obj_tbl_c = MetadataTypes.obj_tbl () in - let sort_tbl_c = MetadataTypes.sort_tbl () in - let rel_tbl_c = MetadataTypes.rel_tbl () in - let name_tbl_c = MetadataTypes.name_tbl () in - let count_tbl_c = MetadataTypes.count_tbl () in - let stats = - SqlStatements.drop_tables [ - (obj_tbl_b,`RefObj); - (sort_tbl_b,`RefSort); - (rel_tbl_b,`RefRel); - (name_tbl_b,`ObjectName); - (count_tbl_b,`Count); - (hits_tbl,`Hits) ] @ - SqlStatements.drop_indexes [ - (obj_tbl,`RefObj); - (sort_tbl,`RefSort); - (rel_tbl,`RefRel); - (name_tbl,`ObjectName); - (count_tbl,`Count); - (obj_tbl_c,`RefObj); - (sort_tbl_c,`RefSort); - (rel_tbl_c,`RefRel); - (name_tbl_c,`ObjectName); - (count_tbl_c,`Count); - (hits_tbl,`Hits) ] @ - SqlStatements.rename_tables [ - (obj_tbl,obj_tbl_b); - (sort_tbl,sort_tbl_b); - (rel_tbl,rel_tbl_b); - (name_tbl,name_tbl_b); - (count_tbl,count_tbl_b) ] @ - SqlStatements.rename_tables [ - (obj_tbl_c,obj_tbl); - (sort_tbl_c,sort_tbl); - (rel_tbl_c,rel_tbl); - (name_tbl_c,name_tbl); - (count_tbl_c,count_tbl) ] @ - SqlStatements.create_tables [ - (hits_tbl,`Hits) ] @ - SqlStatements.fill_hits obj_tbl hits_tbl @ - SqlStatements.create_indexes [ - (obj_tbl,`RefObj); - (sort_tbl,`RefSort); - (rel_tbl,`RefRel); - (name_tbl,`ObjectName); - (count_tbl,`Count); - (hits_tbl,`Hits) ] - in - List.iter (fun statement -> - try -(* prerr_endline statement;*) - ignore (Mysql.exec dbd statement) - with exn -> - let status = Mysql.status dbd in - match status with - | Mysql.StatusError Mysql.Table_exists_error - | Mysql.StatusError Mysql.Bad_table_error - | Mysql.StatusError Mysql.Cant_drop_field_or_key - | Mysql.StatusError Mysql.Unknown_table -> () - | Mysql.StatusError status -> -(* prerr_endline (string_of_int (Obj.magic status));*) - prerr_endline (Printexc.to_string exn); - raise exn - | _ -> - prerr_endline (Printexc.to_string exn); - ()) - stats -;; - -main () 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/components/metadata/table_creator/Makefile b/components/metadata/table_creator/Makefile deleted file mode 100644 index c54e52d4a..000000000 --- a/components/metadata/table_creator/Makefile +++ /dev/null @@ -1,35 +0,0 @@ -REQUIRES = mysql helm-metadata - -INTERFACE_FILES = -IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) -EXTRA_OBJECTS_TO_INSTALL = -EXTRA_OBJECTS_TO_CLEAN = \ - table_creator table_creator.opt table_destructor table_destructor.opt - -all: table_creator table_destructor - @echo -n -opt: table_creator.opt table_destructor.opt - @echo -n - -table_creator: table_creator.ml ../metadata.cma - @echo " OCAMLC $<" - @$(OCAMLFIND) ocamlc \ - -thread -package mysql,helm-metadata -linkpkg -o $@ $< - -table_destructor: table_creator - @ln -f $< $@ - -table_creator.opt: table_creator.ml ../metadata.cmxa - @echo " OCAMLOPT $<" - @$(OCAMLFIND) ocamlopt \ - -thread -package mysql,helm-metadata -linkpkg -o $@ $< - -table_destructor.opt: table_creator.opt - @ln -f $< $@ - -clean: - rm -f *.cm[iox] *.a *.o - rm -f table_creator table_creator.opt table_destructor table_destructor.opt - -include .depend -include ../../../Makefile.defs diff --git a/components/metadata/table_creator/sync_db.sh b/components/metadata/table_creator/sync_db.sh deleted file mode 100755 index 7b201382a..000000000 --- a/components/metadata/table_creator/sync_db.sh +++ /dev/null @@ -1,28 +0,0 @@ -#!/bin/sh - -# sync metadata from a source database (usually "mowgli") to a target one -# (usually "matita") -# Created: Fri, 13 May 2005 13:50:16 +0200 zacchiro -# Last-Modified: Fri, 13 May 2005 13:50:16 +0200 zacchiro - -SOURCE_DB="mowgli" -TARGET_DB="matita" -MYSQL_FLAGS="-u helm -h localhost" - -MYSQL="mysql $MYSQL_FLAGS -f" -MYSQLDUMP="mysqldump $MYSQL_FLAGS" -MYSQLRESTORE="mysqlrestore $MYSQL_FLAGS" -TABLES=`./table_creator list all` -DUMP="${SOURCE_DB}_dump.gz" - -echo "Dumping source db $SOURCE_DB ..." -$MYSQLDUMP $SOURCE_DB $TABLES | gzip -c > $DUMP -echo "Destroying old tables in target db $TARGET_DB ..." -./table_destructor table all | $MYSQL $TARGET_DB -echo "Creating table structure in target db $TARGET_DB ..." -echo "Filling target db $TARGET_DB ..." -zcat $DUMP | $MYSQL $TARGET_DB -./table_creator index all | $MYSQL $TARGET_DB -rm $DUMP -echo "Done." - diff --git a/components/metadata/table_creator/table_creator.ml b/components/metadata/table_creator/table_creator.ml deleted file mode 100644 index 423edfb27..000000000 --- a/components/metadata/table_creator/table_creator.ml +++ /dev/null @@ -1,83 +0,0 @@ - -open Printf - -let map = - (MetadataTypes.library_obj_tbl,`RefObj) :: - (MetadataTypes.library_sort_tbl,`RefSort) :: - (MetadataTypes.library_rel_tbl,`RefRel) :: - (MetadataTypes.library_name_tbl,`ObjectName) :: - (MetadataTypes.library_hits_tbl,`Hits) :: - (MetadataTypes.library_count_tbl,`Count) :: [] - -let usage argv_o = - prerr_string "\nusage:"; - prerr_string ("\t" ^ argv_o ^ " what tablename[=rename]\n"); - prerr_string ("\t" ^ argv_o ^ " what all\n\n"); - prerr_endline "what:"; - prerr_endline "\tlist\tlist table names"; - prerr_endline "\ttable\toutput SQL regarding tables"; - prerr_endline "\tindex\toutput SQL regarding indexes"; - prerr_endline "\tfill\toutput SQL filling tables (only \"hits\" supported)\n"; - prerr_string "known tables:\n\t"; - List.iter (fun (n,_) -> prerr_string (" " ^ n)) map; - prerr_endline "\n" - -let eq_RE = Str.regexp "=" - -let parse_args l = - List.map (fun s -> - let parts = Str.split eq_RE s in - let len = List.length parts in - assert (len = 1 || len = 2); - if len = 1 then (s,s) else (List.nth parts 0, List.nth parts 1)) - l - -let destructor_RE = Str.regexp "table_destructor\\(\\|\\.opt\\)$" - -let am_i_destructor () = - try - let _ = Str.search_forward destructor_RE Sys.argv.(0) 0 in true - with Not_found -> false - -let main () = - let len = Array.length Sys.argv in - if len < 3 then - begin - usage Sys.argv.(0); - exit 1 - end - else - begin - let tab,idx,fill = - if am_i_destructor () then - (SqlStatements.drop_tables,SqlStatements.drop_indexes, - fun _ t -> [sprintf "DELETE * FROM %s;" t]) - else - (SqlStatements.create_tables,SqlStatements.create_indexes, - SqlStatements.fill_hits) - in - let from = 2 in - let what = - match Sys.argv.(1) with - | "list" -> `List - | "index" -> `Index - | "table" -> `Table - | "fill" -> `Fill - | _ -> failwith "what must be one of \"index\", \"table\", \"fill\"" - in - let todo = Array.to_list (Array.sub Sys.argv from (len - from)) in - let todo = match todo with ["all"] -> List.map fst map | todo -> todo in - let todo = parse_args todo in - let todo = List.map (fun (x,name) -> name, (List.assoc x map)) todo in - match what with - | `Index -> print_endline (String.concat "\n" (idx todo)) - | `Table -> print_endline (String.concat "\n" (tab todo)) - | `Fill -> - print_endline (String.concat "\n" - (fill MetadataTypes.library_obj_tbl MetadataTypes.library_hits_tbl)) - | `List -> print_endline (String.concat " " (List.map fst map)) - end - -let _ = main () - - 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