+H=@
include Makefile.defs
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))
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)
-
+H=@
export SHELL=/bin/bash
include ../Makefile.defs
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 \
$(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 .
@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)
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 $@ $<
.PHONY: all opt world backup depend install uninstall clean ocamlinit
ifneq ($(MAKECMDGOALS), depend)
+ ifneq ($(MAKECMDGOALS), depend.opt)
include .depend
+ endif
endif
NULL =
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+ <section name="tmp">
+ <key name="dir">.tmp/</key>
+ </section>
+ <section name="db">
+ <key name="host">localhost</key>
+ <key name="user">helm</key>
+ <key name="database">mowgli</key>
+ </section>
+ <section name="getter">
+ <key name="servers">
+ file:///projects/helm/library/coq_contribs
+ </key>
+ <key name="cache_dir">$(tmp.dir)/cache</key>
+ <key name="maps_dir">$(tmp.dir)/maps</key>
+ <key name="dtd_dir">/projects/helm/xml/dtd</key>
+ </section>
+</helm_registry>
--- /dev/null
+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 ()
+
--- /dev/null
+(* 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 ()
--- /dev/null
+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
--- /dev/null
+#!/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."
+
--- /dev/null
+
+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 ()
+
+
--- /dev/null
+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
+
--- /dev/null
+(* 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 <dumpfile> <uri_index>\n" ^
+ " <dumpfile> is the file where environment will be dumped\n" ^
+ " <uri_index> 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
+
--- /dev/null
+(* 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 ())
--- /dev/null
+(* 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
+
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
-
+++ /dev/null
-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
-
+++ /dev/null
-(* 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 <dumpfile> <uri_index>\n" ^
- " <dumpfile> is the file where environment will be dumped\n" ^
- " <uri_index> 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
-
+++ /dev/null
-(* 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 ())
+++ /dev/null
-(* 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
-
cicNotationLexer.ml.annot: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
cicNotationParser.ml.annot: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
depend: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
+depend.opt: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
# </cross>
grafiteParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
grafiteParser.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
depend: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
+depend.opt: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
# </cross>
#
grafiteParser.cmo: OCAMLC = $(OCAMLC_P4)
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
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
-
+++ /dev/null
-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
+++ /dev/null
-
-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
+++ /dev/null
-<?xml version="1.0" encoding="utf-8"?>
-<helm_registry>
- <section name="tmp">
- <key name="dir">.tmp/</key>
- </section>
- <section name="db">
- <key name="host">localhost</key>
- <key name="user">helm</key>
- <key name="database">mowgli</key>
- </section>
- <section name="getter">
- <key name="servers">
- file:///projects/helm/library/coq_contribs
- </key>
- <key name="cache_dir">$(tmp.dir)/cache</key>
- <key name="maps_dir">$(tmp.dir)/maps</key>
- <key name="dtd_dir">/projects/helm/xml/dtd</key>
- </section>
-</helm_registry>
+++ /dev/null
-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 ()
-
+++ /dev/null
-(* 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 ()
+++ /dev/null
-sql.cmo: sql.cmi
-sql.cmx: sql.cmi
-table_creator.cmo: sql.cmi
-table_creator.cmx: sql.cmx
+++ /dev/null
-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
+++ /dev/null
-#!/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."
-
+++ /dev/null
-
-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 ()
-
-
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 \
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
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
# 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;\
.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) \
.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 \
# {{{ 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
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)
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):
$(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 $< $@
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)
<term><userinput>world</userinput></term>
<listitem>
<para>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) </para>
</listitem>
</varlistentry>
<listitem>
<para>uses the (just built) <application>matitac</application>
compiler to build the &appname; standard library. </para>
- <para>For this step you will need a working SQL database (for
- indexing the standard library while you are compiling it). See
- <ulink type="http" url="#database_setup">Database setup</ulink>
- for instructions on how to set it up.</para>
</listitem>
</varlistentry>
<para>installs &appname; related tools, standard library and the
needed runtime stuff in the proper places on the filesystem
</para>
+ <para>For this step you will need a working SQL database (for
+ indexing the standard library while you are compiling it). See
+ <ulink type="http" url="#database_setup">Database setup</ulink>
+ for instructions on how to set it up.
+ </para>
</listitem>
</varlistentry>
-->
<key name="host">@DBHOST@</key>
<key name="user">helm</key>
- <key name="database">matita</key>
+ <key name="database">prove-release</key>
</section>
<section name="getter">
<!-- Cache dir for CIC XML documents downloaded from the net.
-->
<key name="prefix">
cic:/matita/
- file://@RT_BASE_DIR@/stantard-library/
+ file://@RT_BASE_DIR@/xml/stantard-library/
ro
</key>
<key name="prefix">
<property name="window_placement">GTK_CORNER_TOP_LEFT</property>
<child>
- <widget class="GtkTreeView" id="scriptTreeView">
+ <widget class="GtkViewport" id="viewport1">
<property name="visible">True</property>
- <property name="can_focus">True</property>
- <property name="headers_visible">False</property>
- <property name="rules_hint">False</property>
- <property name="reorderable">False</property>
- <property name="enable_search">True</property>
- <property name="fixed_height_mode">False</property>
- <property name="hover_selection">False</property>
- <property name="hover_expand">False</property>
+ <property name="shadow_type">GTK_SHADOW_IN</property>
+
+ <child>
+ <widget class="GtkLabel" id="label25">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Not implemented.</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ <property name="ellipsize">PANGO_ELLIPSIZE_NONE</property>
+ <property name="width_chars">-1</property>
+ <property name="single_line_mode">False</property>
+ <property name="angle">0</property>
+ </widget>
+ </child>
</widget>
</child>
</widget>
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
"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";
| 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)
+
(** 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
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"
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
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
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
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;
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
projects / helm.git / commitdiff