applyTransformation.cmx: applyTransformation.cmi
disambiguatePp.cmo: disambiguatePp.cmi
disambiguatePp.cmx: disambiguatePp.cmi
-dump_moo.cmo: matitaMoo.cmi matitaLog.cmi buildTimeConf.cmo
-dump_moo.cmx: matitaMoo.cmx matitaLog.cmx buildTimeConf.cmx
-matitacleanLib.cmo: matitaSync.cmi matitaMoo.cmi matitaMisc.cmi matitaLog.cmi \
- matitaExcPp.cmi matitaDb.cmi buildTimeConf.cmo matitacleanLib.cmi
-matitacleanLib.cmx: matitaSync.cmx matitaMoo.cmx matitaMisc.cmx matitaLog.cmx \
- matitaExcPp.cmx matitaDb.cmx buildTimeConf.cmx matitacleanLib.cmi
-matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi \
- matitaInit.cmi matitaDb.cmi matitaclean.cmi
-matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx \
- matitaInit.cmx matitaDb.cmx matitaclean.cmi
-matitacLib.cmo: matitacleanLib.cmi matitaTypes.cmi matitaMoo.cmi \
- matitaLog.cmi matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \
- matitaDb.cmi buildTimeConf.cmo matitacLib.cmi
-matitacLib.cmx: matitacleanLib.cmx matitaTypes.cmx matitaMoo.cmx \
- matitaLog.cmx matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \
- matitaDb.cmx buildTimeConf.cmx matitacLib.cmi
+dump_moo.cmo: buildTimeConf.cmo
+dump_moo.cmx: buildTimeConf.cmx
+matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi
+matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi
+matitacLib.cmo: matitaTypes.cmi matitaMisc.cmi matitaInit.cmi matitaExcPp.cmi \
+ matitaEngine.cmi buildTimeConf.cmo matitacLib.cmi
+matitacLib.cmx: matitaTypes.cmx matitaMisc.cmx matitaInit.cmx matitaExcPp.cmx \
+ matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi
matitac.cmo: matitamake.cmo matitadep.cmi matitaclean.cmi matitacLib.cmi
matitac.cmx: matitamake.cmx matitadep.cmx matitaclean.cmx matitacLib.cmx
-matitaDb.cmo: matitaMisc.cmi matitaDb.cmi
-matitaDb.cmx: matitaMisc.cmx matitaDb.cmi
-matitadep.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi matitaInit.cmi \
- matitadep.cmi
-matitadep.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx matitaInit.cmx \
- matitadep.cmi
+matitadep.cmo: matitaMisc.cmi matitaInit.cmi matitadep.cmi
+matitadep.cmx: matitaMisc.cmx matitaInit.cmx matitadep.cmi
matitaDisambiguator.cmo: matitaTypes.cmi matitaDisambiguator.cmi
matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi
-matitaEngine.cmo: matitacleanLib.cmi matitaTypes.cmi matitaSync.cmi \
- matitaMoo.cmi matitaMisc.cmi matitaLog.cmi matitaDisambiguator.cmi \
- matitaDb.cmi matitaEngine.cmi
-matitaEngine.cmx: matitacleanLib.cmx matitaTypes.cmx matitaSync.cmx \
- matitaMoo.cmx matitaMisc.cmx matitaLog.cmx matitaDisambiguator.cmx \
- matitaDb.cmx matitaEngine.cmi
-matitaExcPp.cmo: matitaTypes.cmi matitaMoo.cmi matitaDisambiguator.cmi \
- matitaExcPp.cmi
-matitaExcPp.cmx: matitaTypes.cmx matitaMoo.cmx matitaDisambiguator.cmx \
- matitaExcPp.cmi
+matitaEngine.cmo: matitaTypes.cmi matitaSync.cmi matitaMisc.cmi \
+ matitaDisambiguator.cmi matitaEngine.cmi
+matitaEngine.cmx: matitaTypes.cmx matitaSync.cmx matitaMisc.cmx \
+ matitaDisambiguator.cmx matitaEngine.cmi
+matitaExcPp.cmo: matitaTypes.cmi matitaDisambiguator.cmi matitaExcPp.cmi
+matitaExcPp.cmx: matitaTypes.cmx matitaDisambiguator.cmx matitaExcPp.cmi
matitaGeneratedGui.cmo: matitaGeneratedGui.cmi
matitaGeneratedGui.cmx: matitaGeneratedGui.cmi
matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmi matitaGtkMisc.cmi
matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmi
-matitaGui.cmo: matitamakeLib.cmi matitacleanLib.cmi matitaTypes.cmi \
- matitaScript.cmi matitaMoo.cmi matitaMisc.cmi matitaMathView.cmi \
- matitaLog.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmi matitaExcPp.cmi \
- matitaDisambiguator.cmi buildTimeConf.cmo matitaGui.cmi
-matitaGui.cmx: matitamakeLib.cmx matitacleanLib.cmx matitaTypes.cmx \
- matitaScript.cmx matitaMoo.cmx matitaMisc.cmx matitaMathView.cmx \
- matitaLog.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx matitaExcPp.cmx \
- matitaDisambiguator.cmx buildTimeConf.cmx matitaGui.cmi
-matitaInit.cmo: matitamakeLib.cmi matitaDb.cmi buildTimeConf.cmo \
- matitaInit.cmi
-matitaInit.cmx: matitamakeLib.cmx matitaDb.cmx buildTimeConf.cmx \
- matitaInit.cmi
-matitaLog.cmo: matitaLog.cmi
-matitaLog.cmx: matitaLog.cmi
-matitamakeLib.cmo: matitaLog.cmi buildTimeConf.cmo matitamakeLib.cmi
-matitamakeLib.cmx: matitaLog.cmx buildTimeConf.cmx matitamakeLib.cmi
+matitaGui.cmo: matitamakeLib.cmi matitaTypes.cmi matitaScript.cmi \
+ matitaMisc.cmi matitaMathView.cmi matitaGtkMisc.cmi \
+ matitaGeneratedGui.cmi matitaExcPp.cmi matitaDisambiguator.cmi \
+ buildTimeConf.cmo matitaGui.cmi
+matitaGui.cmx: matitamakeLib.cmx matitaTypes.cmx matitaScript.cmx \
+ matitaMisc.cmx matitaMathView.cmx matitaGtkMisc.cmx \
+ matitaGeneratedGui.cmx matitaExcPp.cmx matitaDisambiguator.cmx \
+ buildTimeConf.cmx matitaGui.cmi
+matitaInit.cmo: matitamakeLib.cmi buildTimeConf.cmo matitaInit.cmi
+matitaInit.cmx: matitamakeLib.cmx buildTimeConf.cmx matitaInit.cmi
+matitamakeLib.cmo: buildTimeConf.cmo matitamakeLib.cmi
+matitamakeLib.cmx: buildTimeConf.cmx matitamakeLib.cmi
matitamake.cmo: matitamakeLib.cmi matitaInit.cmi
matitamake.cmx: matitamakeLib.cmx matitaInit.cmx
matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
- matitaLog.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi \
- buildTimeConf.cmo applyTransformation.cmi matitaMathView.cmi
+ matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi buildTimeConf.cmo \
+ applyTransformation.cmi matitaMathView.cmi
matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
- matitaLog.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx \
- buildTimeConf.cmx applyTransformation.cmx matitaMathView.cmi
+ matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx buildTimeConf.cmx \
+ applyTransformation.cmx matitaMathView.cmi
matitaMisc.cmo: matitaTypes.cmi buildTimeConf.cmo matitaMisc.cmi
matitaMisc.cmx: matitaTypes.cmx buildTimeConf.cmx matitaMisc.cmi
-matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi matitaLog.cmi \
+matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \
matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi matitaEngine.cmi \
buildTimeConf.cmo
-matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx matitaLog.cmx \
+matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \
matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx matitaEngine.cmx \
buildTimeConf.cmx
-matitaMoo.cmo: matitaTypes.cmi matitaMoo.cmi
-matitaMoo.cmx: matitaTypes.cmx matitaMoo.cmi
-matitaScript.cmo: matitamakeLib.cmi matitacleanLib.cmi matitaTypes.cmi \
- matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaEngine.cmi \
- matitaDisambiguator.cmi matitaDb.cmi disambiguatePp.cmi buildTimeConf.cmo \
- matitaScript.cmi
-matitaScript.cmx: matitamakeLib.cmx matitacleanLib.cmx matitaTypes.cmx \
- matitaSync.cmx matitaMisc.cmx matitaLog.cmx matitaEngine.cmx \
- matitaDisambiguator.cmx matitaDb.cmx disambiguatePp.cmx buildTimeConf.cmx \
- matitaScript.cmi
-matitaSync.cmo: matitaTypes.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \
- disambiguatePp.cmi matitaSync.cmi
-matitaSync.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \
- disambiguatePp.cmx matitaSync.cmi
-matitaTypes.cmo: matitaLog.cmi matitaTypes.cmi
-matitaTypes.cmx: matitaLog.cmx matitaTypes.cmi
+matitaScript.cmo: matitamakeLib.cmi matitaTypes.cmi matitaSync.cmi \
+ matitaMisc.cmi matitaEngine.cmi matitaDisambiguator.cmi \
+ disambiguatePp.cmi buildTimeConf.cmo matitaScript.cmi
+matitaScript.cmx: matitamakeLib.cmx matitaTypes.cmx matitaSync.cmx \
+ matitaMisc.cmx matitaEngine.cmx matitaDisambiguator.cmx \
+ disambiguatePp.cmx buildTimeConf.cmx matitaScript.cmi
+matitaSync.cmo: matitaTypes.cmi disambiguatePp.cmi matitaSync.cmi
+matitaSync.cmx: matitaTypes.cmx disambiguatePp.cmx matitaSync.cmi
+matitaTypes.cmo: matitaTypes.cmi
+matitaTypes.cmx: matitaTypes.cmi
matitaDisambiguator.cmi: matitaTypes.cmi
matitaEngine.cmi: matitaTypes.cmi
matitaGtkMisc.cmi: matitaGeneratedGui.cmi
matitaGui.cmi: matitaGuiTypes.cmi matitaDisambiguator.cmi
-matitaGuiTypes.cmi: matitaTypes.cmi matitaLog.cmi matitaGeneratedGui.cmi
+matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmi
matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi
-matitaMoo.cmi: matitaTypes.cmi
matitaScript.cmi: matitaTypes.cmi
matitaSync.cmi: matitaTypes.cmi
# objects for matita (GTK GUI)
CMOS = \
buildTimeConf.cmo \
- matitaLog.cmo \
matitaTypes.cmo \
- matitaMoo.cmo \
matitaMisc.cmo \
- matitaDb.cmo \
matitamakeLib.cmo \
matitaInit.cmo \
disambiguatePp.cmo \
matitaSync.cmo \
matitaDisambiguator.cmo \
matitaExcPp.cmo \
- matitacleanLib.cmo \
matitaEngine.cmo \
matitacLib.cmo \
matitaScript.cmo \
# objects for matitac (batch compiler)
CCMOS = \
buildTimeConf.cmo \
- matitaLog.cmo \
matitaTypes.cmo \
- matitaMoo.cmo \
matitaMisc.cmo \
- matitaDb.cmo \
matitamakeLib.cmo \
matitaInit.cmo \
disambiguatePp.cmo \
matitaSync.cmo \
matitaDisambiguator.cmo \
matitaExcPp.cmo \
- matitacleanLib.cmo \
matitaEngine.cmo \
matitacLib.cmo \
$(NULL)
CLEANCMOS = $(CCMOS)
MAKECMOS = \
buildTimeConf.cmo \
- matitaLog.cmo \
matitamakeLib.cmo \
$(NULL)
PROGRAMS_BYTE = matita matitac cicbrowser matitadep matitaclean matitamake dump_moo
matita.opt: $(LIBX_DEPS) $(CMXS) matita.ml
$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml
-dump_moo: buildTimeConf.cmo matitaLog.cmo matitaMoo.cmo dump_moo.ml
+dump_moo: buildTimeConf.cmo dump_moo.ml
$(OCAMLC) $(PKGS) -linkpkg -o $@ $^
-dump_moo.opt: buildTimeConf.cmx matitaLog.cmx matitaMoo.cmx dump_moo.ml
+dump_moo.opt: buildTimeConf.cmx dump_moo.ml
$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^
matitac: $(CLIB_DEPS) $(CCMOS) $(MAINCMOS) matitac.ml
$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml \
$(STATIC_EXTRA_LIBS)
strip $@
-dump_moo.opt.static: $(STATIC_LINK) buildTimeConf.cmx matitaLog.cmx matitaMoo.cmx dump_moo.ml
+dump_moo.opt.static: $(STATIC_LINK) buildTimeConf.cmx dump_moo.ml
$(STATIC_LINK) $(STATIC_CLIBS) -- \
$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^ \
$(STATIC_EXTRA_CLIBS)
List.iter
(fun fname ->
if not (Sys.file_exists fname) then
- MatitaLog.error (sprintf "Can't find moo '%s', skipping it." fname)
+ HLog.error (sprintf "Can't find moo '%s', skipping it." fname)
else begin
printf "%s:\n" fname; flush stdout;
- let commands, metadata = MatitaMoo.load_moo ~fname in
+ let commands, metadata = GrafiteMarshal.load_moo ~fname in
List.iter
(fun cmd ->
printf " %s\n" (GrafiteAstPp.pp_command cmd); flush stdout)
(CicEnvironment.list_obj ()));
addDebugItem "print selections" (fun () ->
let cicMathView = MatitaMathView.cicMathView_instance () in
- List.iter MatitaLog.debug (cicMathView#string_of_selections));
+ List.iter HLog.debug (cicMathView#string_of_selections));
addDebugItem "dump script status" script#dump;
addDebugItem "dump configuration file to ./foo.conf.xml" (fun _ ->
Helm_registry.save_to "./foo.conf.xml");
addDebugItem "dump metasenv"
(fun _ ->
if script#onGoingProof () then
- MatitaLog.debug (CicMetaSubst.ppmetasenv [] script#proofMetasenv));
+ HLog.debug (CicMetaSubst.ppmetasenv [] script#proofMetasenv));
addDebugItem "dump coercions Db" (fun _ ->
List.iter
(fun (s,t,u) ->
- MatitaLog.debug
+ HLog.debug
(UriManager.name_of_uri u ^ ":"
^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t))
(CoercDb.to_list ()));
(MatitaTypes.get_stack (MatitaScript.current ())#status)));
(* addDebugItem "ask record choice"
(fun _ ->
- MatitaLog.debug (string_of_int
+ HLog.debug (string_of_int
(MatitaGtkMisc.ask_record_choice ~gui ~title:"title" ~message:"msg"
~fields:["a"; "b"; "c"]
~records:[
+Ferruccio ha cambiato matita.lang:
+> <keyword>iforall</keyword>
+> <keyword>iexists</keyword>
+
+- possibile bug cut&paste di pattern profondi nelle ipotesi: secondo
+ me sbaglia il nome dell'ipotesi!
+
TODO
NUCLEO
- http://mowgli.cs.unibo.it:58084/proofCheck?uri=cic:/Coq/Reals/Rtopology/interior_P3.con
+++ /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/
- *)
-
-open Printf ;;
-
-let instance =
- let dbd = lazy (
- HMysql.quick_connect
- ~host:(Helm_registry.get "db.host")
- ~user:(Helm_registry.get "db.user")
- ~database:(Helm_registry.get "db.database")
- ())
- in
- fun () -> Lazy.force dbd
-
-
-let xpointer_RE = Pcre.regexp "#.*$"
-let file_scheme_RE = Pcre.regexp "^file://"
-
-let clean_owner_environment () =
- let dbd = instance () in
- let owner = (Helm_registry.get "matita.owner") in
- 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
- let owned_uris =
- try
- MetadataDb.clean ~dbd
- with Mysql.Error _ as exn ->
- match HMysql.errno dbd with
- | Mysql.No_such_table -> []
- | _ -> raise exn
- in
- List.iter
- (fun uri ->
- let uri = Pcre.replace ~rex:xpointer_RE ~templ:"" uri in
- List.iter
- (fun suffix ->
- try
- MatitaMisc.safe_remove (Http_getter.resolve (uri ^ suffix))
- with Http_getter_types.Key_not_found _ -> ())
- [""; ".body"; ".types"])
- owned_uris;
- List.iter (fun statement ->
- try
- ignore (HMysql.exec dbd statement)
- with Mysql.Error _ as exn ->
- match HMysql.errno dbd with
- | Mysql.Bad_table_error
- | Mysql.No_such_index | Mysql.No_such_table -> ()
- | _ -> raise exn
- ) statements;
-;;
-
-let create_owner_environment () =
- let dbd = instance () in
- 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 (HMysql.exec dbd statement)
- with
- exn ->
- let status = HMysql.status dbd in
- match status with
- | Mysql.StatusError Mysql.Table_exists_error -> ()
- | Mysql.StatusError Mysql.Dup_keyname -> ()
- | Mysql.StatusError _ -> raise exn
- | _ -> ()
- ) statements
-;;
-
-(* removes uri from the ownerized tables, and returns the list of other objects
- * (theyr uris) that ref the one removed.
- * AFAIK there is no need to return it, since the MatitaTypes.staus should
- * contain all defined objects. but to double check we do not garbage the
- * metadata...
- *)
-let remove_uri uri =
- 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 conclno_tbl = MetadataTypes.conclno_tbl () in
- let conclno_hyp_tbl = MetadataTypes.fullno_tbl () in*)
- let count_tbl = MetadataTypes.count_tbl () in
-
- let dbd = instance () in
- let suri = UriManager.string_of_uri uri in
- let query table suri = sprintf
- "DELETE FROM %s WHERE source LIKE '%s%%'" table (HMysql.escape suri)
- in
- List.iter (fun t ->
- try
- ignore (HMysql.exec dbd (query t suri))
- with
- exn -> raise exn (* no errors should be accepted *)
- )
- [obj_tbl;sort_tbl;rel_tbl;name_tbl;(*conclno_tbl;conclno_hyp_tbl*)count_tbl];
- (* and now the debug job *)
- let dbg_q =
- sprintf "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl
- (HMysql.escape suri)
- in
- try
- let rc = HMysql.exec dbd dbg_q in
- let l = ref [] in
- HMysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
- let l = List.sort Pervasives.compare !l in
- HExtlib.list_uniq l
- with
- exn -> raise exn (* no errors should be accepted *)
-
-let xpointers_of_ind uri =
- let dbd = instance () in
- let name_tbl = MetadataTypes.name_tbl () in
- let query = sprintf
- "SELECT source FROM %s WHERE source LIKE '%s#xpointer%%'" name_tbl
- (HMysql.escape (UriManager.string_of_uri uri))
- in
- let rc = HMysql.exec dbd query in
- let l = ref [] in
- HMysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
- List.map UriManager.uri_of_string !l
-
+++ /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/
- *)
-
-val instance: unit -> HMysql.dbd
-
-val create_owner_environment: unit -> unit
-val clean_owner_environment: unit -> unit
-
-(* returns a list of uri thet must be removed sice they reference uri,
- * but this is used only for debugging purposes *)
-val remove_uri: UriManager.uri -> string list
-val xpointers_of_ind: UriManager.uri -> UriManager.uri list
| GrafiteAst.Assumption _ -> Tactics.assumption
| GrafiteAst.Auto (_,depth,width,paramodulation,full) ->
AutoTactic.auto_tac ?depth ?width ?paramodulation ?full
- ~dbd:(MatitaDb.instance ()) ()
+ ~dbd:(LibraryDb.instance ()) ()
| GrafiteAst.Change (_, pattern, with_what) ->
Tactics.change ~pattern with_what
| GrafiteAst.Clear (_,id) -> Tactics.clear id
| GrafiteAst.Ident _ -> assert false
in
let user_types = List.rev_map to_type types in
- let dbd = MatitaDb.instance () in
+ let dbd = LibraryDb.instance () in
let mk_fresh_name_callback = namer_of names in
Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what
| GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
| GrafiteAst.Fourier _ -> Tactics.fourier
| GrafiteAst.FwdSimpl (_, hyp, names) ->
Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names)
- ~dbd:(MatitaDb.instance ()) hyp
+ ~dbd:(LibraryDb.instance ()) hyp
| GrafiteAst.Generalize (_,pattern,ident) ->
let names = match ident with None -> [] | Some id -> [id] in
Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern
in
let (diff, metasenv, cic, _) =
singleton
- (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
+ (MatitaDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
~aliases:status.aliases ~universe:(Some status.multi_aliases)
~context ~metasenv:(MatitaTypes.get_proof_metasenv status) term)
in
let status = !status_ref in
let (diff, metasenv, cic, ugraph) =
singleton
- (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
+ (MatitaDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
~initial_ugraph:ugraph ~aliases:status.aliases
~universe:(Some status.multi_aliases) ~context ~metasenv term)
in
MatitaSync.add_obj uri obj status
with
CicTypeChecker.TypeCheckerFailure s ->
- MatitaLog.message
+ HLog.message
("Unable to create projection " ^ name ^ " cause: " ^ (Lazy.force s));
status
| CicEnvironment.Object_not_found uri ->
let depend = UriManager.name_of_uri uri in
- MatitaLog.message
+ HLog.message
("Unable to create projection " ^ name ^ " because it requires " ^ depend);
status
) status projections
| CicNotationPt.Theorem _ -> None in
let (diff, metasenv, cic, _) =
singleton
- (MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
+ (MatitaDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj)
in
let proof_status =
let status,cmd = disambiguate_command status cmd in
let cmd,notation_ids' = CicNotation.process_notation cmd in
let status =
- { status with notation_ids = notation_ids' @ status.notation_ids }
- in
+ { status with notation_ids = notation_ids' @ status.notation_ids } in
+ let basedir = Helm_registry.get "matita.basedir" in
match cmd with
| GrafiteAst.Default (loc, what, uris) as cmd ->
LibraryObjects.set_default what uris;
add_moo_content [cmd] status
| GrafiteAst.Include (loc, path) ->
let absolute_path = make_absolute opts.include_paths path in
- let moopath = MatitacleanLib.obj_file_of_script absolute_path in
+ let moopath = MatitaMisc.obj_file_of_script ~basedir absolute_path in
let status = ref status in
if not (Sys.file_exists moopath) then
raise (IncludedFileNotCompiled moopath);
with Not_found -> v
in
if not (MatitaMisc.is_empty value) && opts.clean_baseuri then begin
- MatitaLog.warn ("baseuri " ^ value ^ " is not empty");
- MatitaLog.message ("cleaning baseuri " ^ value);
- MatitacleanLib.clean_baseuris [value]
+ HLog.warn ("baseuri " ^ value ^ " is not empty");
+ HLog.message ("cleaning baseuri " ^ value);
+ LibraryClean.clean_baseuris ~basedir [value]
end;
add_moo_metadata [GrafiteAst.Baseuri value] status
end else
| Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
let name = UriManager.name_of_uri uri in
if not(CicPp.check name ty) then
- MatitaLog.error ("Bad name: " ^ name);
+ HLog.error ("Bad name: " ^ name);
if opts.do_heavy_checks then
begin
- let dbd = MatitaDb.instance () in
+ let dbd = LibraryDb.instance () in
let similar = Whelp.match_term ~dbd ty in
let similar_len = List.length similar in
if similar_len> 30 then
- (MatitaLog.message
+ (HLog.message
("Duplicate check will compare your theorem with " ^
string_of_int similar_len ^
" theorems, this may take a while."));
(match convertible with
| [] -> ()
| x::_ ->
- MatitaLog.warn
+ HLog.warn
("Theorem already proved: " ^ UriManager.string_of_uri x ^
"\nPlease use a variant."));
end;
GrafiteAst.Command (DisambiguateTypes.dummy_floc,
(GrafiteAst.reash_cmd_uris cmd)))
in
- let moo, metadata = MatitaMoo.load_moo fname in
+ let moo, metadata = GrafiteMarshal.load_moo fname in
List.iter
(fun ast ->
let ast = ast_of_cmd ast in
?do_heavy_checks ?include_paths ?clean_baseuri status
(Ulexing.from_utf8_string str) (fun _ _ -> ())
-let default_options () =
-(*
- let options =
- StringMap.add "baseuri"
- (String
- (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
- no_options
- in
-*)
- let options =
- StringMap.add "basedir"
- (String (Helm_registry.get "matita.basedir"))
- no_options
- in
- options
+let default_options () = no_options
let initial_status =
lazy {
| Unix.Unix_error (code, api, param) ->
let err = Unix.error_message code in
None, "Unix Error (" ^ api ^ "): " ^ err
- | MatitaMoo.Corrupt_moo fname ->
+ | GrafiteMarshal.Corrupt_moo fname ->
None, sprintf ".moo file '%s' is corrupt (shorter than expected)" fname
- | MatitaMoo.Checksum_failure fname ->
+ | GrafiteMarshal.Checksum_failure fname ->
None,
sprintf "checksum failed for .moo file '%s', please recompile it'" fname
- | MatitaMoo.Version_mismatch fname ->
+ | GrafiteMarshal.Version_mismatch fname ->
None,
sprintf
(".moo file '%s' has been compiled by a different version of matita, "
method debug s = buffer#insert ~iter:buffer#end_iter ~tags:[debug_tag] s
method clear () =
buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter
- method log_callback (tag: MatitaLog.log_tag) s =
+ method log_callback (tag: HLog.log_tag) s =
match tag with
| `Debug -> self#debug (s ^ "\n")
| `Error -> self#error (s ^ "\n")
let clean_current_baseuri status =
try
let baseuri = MatitaTypes.get_string_option status "baseuri" in
- MatitacleanLib.clean_baseuris [baseuri]
+ let basedir = Helm_registry.get "matita.basedir" in
+ LibraryClean.clean_baseuris ~basedir [baseuri]
with MatitaTypes.Option_error _ -> ()
let ask_and_save_moo_if_needed parent fname status =
+ let basedir = Helm_registry.get "matita.basedir" in
let save () =
- let moo_fname = MatitacleanLib.obj_file_of_script fname in
- MatitaMoo.save_moo moo_fname status.MatitaTypes.moo_content_rev in
+ let moo_fname = MatitaMisc.obj_file_of_script ~basedir fname in
+ GrafiteMarshal.save_moo moo_fname
+ status.MatitaTypes.moo_content_rev in
if (MatitaScript.current ())#eos &&
status.MatitaTypes.proof_status = MatitaTypes.No_proof
then
begin
- let mooname =
- MatitacleanLib.obj_file_of_script fname
- in
+ let mooname = MatitaMisc.obj_file_of_script ~basedir fname in
let rc =
MatitaGtkMisc.ask_confirmation
~title:"A .moo can be generated"
newDevel#toplevel#misc#hide()
end
else
- MatitaLog.error ("The selected root does not contain " ^
+ HLog.error ("The selected root does not contain " ^
match next_devel_must_contain with
| Some x -> x
| _ -> assert false));
~check:main#fullscreenMenuItem;
main#fullscreenMenuItem#set_active false;
(* log *)
- MatitaLog.set_log_callback self#console#log_callback;
+ HLog.set_log_callback self#console#log_callback;
GtkSignal.user_handler :=
(fun exn ->
if not (Helm_registry.get_bool "matita.debug") then
source_buffer#place_cursor
(source_buffer#get_iter (`OFFSET x'));
end;
- MatitaLog.error msg
+ HLog.error msg
else raise exn);
(* script *)
ignore (source_buffer#connect#mark_set (fun _ _ -> next_ligatures <- []));
let _ =
match GSourceView.source_language_from_file BuildTimeConf.lang_file with
| None ->
- MatitaLog.warn (sprintf "can't load language file %s"
+ HLog.warn (sprintf "can't load language file %s"
BuildTimeConf.lang_file)
| Some matita_lang ->
source_buffer#set_language matita_lang;
method debug: string -> unit
method clear: unit -> unit
- method log_callback: MatitaLog.log_callback
+ method log_callback: HLog.log_callback
end
class type browserWin =
if not (already_configured [ Db ] init_status) then
begin
MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
- MatitaDb.create_owner_environment ();
+ LibraryDb.create_owner_environment ();
Db::init_status
end
else
+++ /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/
- *)
-
-open Printf
-
-type log_tag = [ `Debug | `Error | `Message | `Warning ]
-type log_callback = log_tag -> string -> unit
-
-(*
-colors=(black red green yellow blue magenta cyan gray white)
-ccodes=(30 31 32 33 34 35 36 37 39)
-*)
-
-let blue = "\e[0;34m"
-let yellow = "\e[0;33m"
-let green = "\e[0;32m"
-let red = "\e[0;31m"
-let black = "\e[0m"
-
-let default_callback tag s =
- let prefix,ch =
- match tag with
- | `Message -> green ^ "Info: ", stdout
- | `Warning -> yellow ^ "Warn: ", stderr
- | `Error -> red ^ "Error: ", stderr
- | `Debug -> blue ^ "Debug: ", stderr
- in
- output_string ch (prefix ^ black ^ s ^ "\n");
- flush ch
-
-let callback = ref default_callback
-
-let set_log_callback f = callback := f
-let get_log_callback () = !callback
-
-let message s = !callback `Message s
-let warn s = !callback `Warning s
-let error s = !callback `Error s
-let debug s = !callback `Debug s
-
+++ /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/
- *)
-
-type log_tag = [ `Debug | `Error | `Message | `Warning ]
-type log_callback = log_tag -> string -> unit
-
-val set_log_callback: log_callback -> unit
-val get_log_callback: unit -> log_callback
-
-val message : string -> unit
-val warn : string -> unit
-val error : string -> unit
-val debug : string -> unit
-
| Some ((None, _, _, _, _, _) as info) ->
(* building a dummy sequent for obj *)
let t = self#find_obj_conclusion id in
- MatitaLog.debug (CicPp.ppterm t);
+ HLog.debug (CicPp.ppterm t);
info, (~-1, [], t)
| None -> assert false
in
ids_to_terms, ids_to_hypotheses, ids_to_father_ids,
Hashtbl.create 1, None));
let name = "sequent_viewer.xml" in
- MatitaLog.debug ("load_sequent: dumping MathML to ./" ^ name);
+ HLog.debug ("load_sequent: dumping MathML to ./" ^ name);
ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ());
self#load_root ~root:mathml#get_documentElement
self#thaw
| _ ->
let name = "cic_browser.xml" in
- MatitaLog.debug ("cic_browser: dumping MathML to ./" ^ name);
+ HLog.debug ("cic_browser: dumping MathML to ./" ^ name);
ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ());
self#load_root ~root:mathml#get_documentElement;
current_mathml <- Some mathml);
| Http_getter_types.Ls_object _ -> false)
(Http_getter.ls (Http_getter_misc.strip_trailing_slash buri ^ "/"))
-let safe_remove fname = if Sys.file_exists fname then Sys.remove fname
-
-let is_dir_empty d =
- try
- let od = Unix.opendir d in
- try
- ignore (Unix.readdir od);
- ignore (Unix.readdir od);
- ignore (Unix.readdir od);
- Unix.closedir od;
- false
- with End_of_file ->
- Unix.closedir od;
- true
- with Unix.Unix_error _ -> true
-
-let safe_rmdir d = try Unix.rmdir d with Unix.Unix_error _ -> ()
-
-let rec rmdir_descend d =
- if is_dir_empty d then
- begin
- safe_rmdir d;
- rmdir_descend (Filename.dirname d)
- end
-
let absolute_path file =
if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file
let end_ma_RE = Pcre.regexp "\\.ma$"
-let obj_file_of_baseuri baseuri =
- let path =
- Helm_registry.get "matita.basedir" ^ "/xml" ^
- Pcre.replace ~pat:"^cic:" ~templ:"" baseuri
- in
- path ^ ".moo"
-
let list_tl_at ?(equality=(==)) e l =
let rec aux =
function
in
aux l
+let baseuri_of_file file =
+ let uri = ref None in
+ let ic = open_in file in
+ let istream = Ulexing.from_utf8_channel ic in
+ (try
+ while true do
+ try
+ let stm = GrafiteParser.parse_statement istream in
+ match baseuri_of_baseuri_decl stm with
+ | Some buri ->
+ let u = strip_trailing_slash buri in
+ if String.length u < 5 || String.sub u 0 5 <> "cic:/" then
+ HLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
+ (try
+ ignore(Http_getter.resolve u)
+ with
+ | Http_getter_types.Unresolvable_URI _ ->
+ HLog.error (file ^ " sets an unresolvable baseuri: "^buri)
+ | Http_getter_types.Key_not_found _ -> ());
+ uri := Some u;
+ raise End_of_file
+ | None -> ()
+ with
+ CicNotationParser.Parse_error err ->
+ HLog.error ("Unable to parse: " ^ file);
+ HLog.error ("Parse error: " ^ err);
+ ()
+ done
+ with End_of_file -> close_in ic);
+ match !uri with
+ | Some uri -> uri
+ | None -> failwith ("No baseuri defined in " ^ file)
+
+let obj_file_of_script ~basedir f =
+ if f = "coq.ma" then BuildTimeConf.coq_notation_script else
+ let baseuri = baseuri_of_file f in
+ LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri
+
(** check whether no objects are defined below a given baseuri *)
val is_empty: string -> bool
-(** removes a file if it exists *)
-val safe_remove: string -> unit
-(** removes a dir if it exists and is empty *)
-val safe_rmdir: string -> unit
-(** checks if the dir is empty *)
-val is_dir_empty: string -> bool
-(** removes a directory and recursively the father (if empty) *)
-val rmdir_descend: string -> unit
-
val absolute_path: string -> string
(** @return true if file is a (textual) proof script *)
(** given the base name of an image, returns its full path *)
val image_path: string -> string
-val obj_file_of_baseuri: string -> string
+val baseuri_of_file: string -> string
+val obj_file_of_script : basedir:string -> string -> string
+++ /dev/null
-(* Copyright (C) 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/
- *)
-
-exception Checksum_failure of string
-exception Corrupt_moo of string
-exception Version_mismatch of string
-
-let marshal_flags = []
-
-(** .moo file format
- * - an integer -- magic number -- denoting the version of the dumped data
- * structure. Different magic numbers stand for incompatible data structures
- * - an integer -- checksum -- denoting the hash value (computed with
- * Hashtbl.hash) of the string representation of the dumped data structur
- * - marshalled pair: first component is a list of GrafiteAst.command (real moo
- * content), second component is a list of GrafiteAst.metadata
- *)
-
-let save_moo ~fname (moo, metadata) =
- let oc = open_out fname in
- let marshalled =
- Marshal.to_string (List.rev moo, List.rev metadata) marshal_flags
- in
- let checksum = Hashtbl.hash marshalled in
- output_binary_int oc GrafiteAst.magic;
- output_binary_int oc checksum;
- output_string oc marshalled;
- close_out oc
-
-let load_moo ~fname =
- let ic = open_in fname in
- HExtlib.finally
- (fun () -> close_in ic)
- (fun () ->
- try
- let moo_magic = input_binary_int ic in
- if moo_magic <> GrafiteAst.magic then raise (Version_mismatch fname);
- let moo_checksum = input_binary_int ic in
- let marshalled = HExtlib.input_all ic in
- let checksum = Hashtbl.hash marshalled in
- if checksum <> moo_checksum then raise (Checksum_failure fname);
- let (moo: MatitaTypes.moo) =
- Marshal.from_string marshalled 0
- in
- moo
- with End_of_file -> raise (Corrupt_moo fname))
- ()
-
+++ /dev/null
-(* Copyright (C) 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/
- *)
-
- (** name of the corrupt .moo file *)
-exception Checksum_failure of string
-exception Corrupt_moo of string
-exception Version_mismatch of string
-
-val save_moo: fname:string -> MatitaTypes.moo -> unit
-
- (** @raise Corrupt_moo *)
-val load_moo: fname:string -> MatitaTypes.moo
-
let disambiguate_macro_term term status user_goal =
let module MD = MatitaDisambiguator in
- let dbd = MatitaDb.instance () in
+ let dbd = LibraryDb.instance () in
let metasenv = MatitaTypes.get_proof_metasenv status in
let context = MatitaTypes.get_proof_context status user_goal in
let interps =
let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
let module TAPp = GrafiteAstPp in
let module MQ = MetadataQuery in
- let module MDB = MatitaDb in
+ let module MDB = LibraryDb in
let module CTC = CicTypeChecker in
let module CU = CicUniv in
(* no idea why ocaml wants this *)
let parsed_text_length = String.length parsed_text in
- let dbd = MatitaDb.instance () in
+ let dbd = LibraryDb.instance () in
match mac with
(* WHELP's stuff *)
| TA.WMatch (loc, term) ->
in
[ new_status , (extra_text, ast) ], parsed_text_length
| _ ->
- MatitaLog.error
+ HLog.error
"The result of the urichooser should be only 1 uri, not:\n";
List.iter (
- fun u -> MatitaLog.error (UriManager.string_of_uri u ^ "\n")
+ fun u -> HLog.error (UriManager.string_of_uri u ^ "\n")
) selected;
assert false)
| TA.Check (_,term) ->
=
let module TAPp = GrafiteAstPp in
let module MD = MatitaDisambiguator in
- let module ML = MatitacleanLib in
+ let module ML = MatitaMisc in
match ex with
| TA.Command (loc, _) | TA.Tactical (loc, _, _) ->
(try
"Do you want to redefine the corresponding "^
"part of the library?")
with
- | `YES -> MatitacleanLib.clean_baseuris [u]
+ | `YES ->
+ let basedir = Helm_registry.get "matita.basedir" in
+ LibraryClean.clean_baseuris ~basedir [u]
| `NO -> ()
| `CANCEL -> raise MatitaTypes.Cancel);
eval_with_engine
*)
in
let s = match statement with Some s -> s | None -> self#getFuture in
- MatitaLog.debug ("evaluating: " ^ first_line s ^ " ...");
+ HLog.debug ("evaluating: " ^ first_line s ^ " ...");
(try aux (`Raw s) with End_of_file -> raise Margin)
method private _retract offset status new_statements new_history =
output_string oc (buffer#get_text ~start:buffer#start_iter
~stop:buffer#end_iter ());
close_out oc;
- MatitaLog.debug ("backup " ^ f ^ " saved")
+ HLog.debug ("backup " ^ f ^ " saved")
end
method private goto_top =
(* debug *)
method dump () =
- MatitaLog.debug "script status:";
- MatitaLog.debug ("history size: " ^ string_of_int (List.length history));
- MatitaLog.debug (sprintf "%d statements:" (List.length statements));
- List.iter MatitaLog.debug statements;
- MatitaLog.debug ("Current file name: " ^
+ HLog.debug "script status:";
+ HLog.debug ("history size: " ^ string_of_int (List.length history));
+ HLog.debug (sprintf "%d statements:" (List.length statements));
+ List.iter HLog.debug statements;
+ HLog.debug ("Current file name: " ^
(match guistuff.filenamedata with
|None,_ -> "[ no name ]"
| Some f,_ -> f));
let extract_alias types uri =
fst(List.fold_left (
fun (acc,i) (name, _, _, cl) ->
- (name, UriManager.string_of_uri (UriManager.uri_of_uriref uri i None))
- ::
+ (name, UriManager.uri_of_uriref uri i None) ::
(fst(List.fold_left (
fun (acc,j) (name,_) ->
- (((name,UriManager.string_of_uri (UriManager.uri_of_uriref uri i
- (Some j))) :: acc) , j+1)
+ (((name,UriManager.uri_of_uriref uri i
+ (Some j)) :: acc) , j+1)
) (acc,1) cl)),i+1
) ([],0) types)
let build_aliases =
List.map
- (fun (name,suri) ->
+ (fun (name,uri) ->
DisambiguateTypes.Id name,
- (suri, fun _ _ _ -> CicUtil.term_of_uri (UriManager.uri_of_string suri)))
+ (UriManager.string_of_uri uri, fun _ _ _ -> CicUtil.term_of_uri uri))
-let add_aliases_for_inductive_def status types suri =
- let uri = UriManager.uri_of_string suri in
+let add_aliases_for_inductive_def status types uri =
let aliases = build_aliases (extract_alias types uri) in
set_proof_aliases status aliases
-let add_alias_for_constant status suri =
- let uri = UriManager.uri_of_string suri in
+let add_alias_for_constant status uri =
let name = UriManager.name_of_uri uri in
- let new_env = build_aliases [(name,suri)] in
+ let new_env = build_aliases [(name,uri)] in
set_proof_aliases status new_env
-let add_aliases_for_object status suri =
+let add_aliases_for_object status uri =
function
Cic.InductiveDefinition (types,_,_,_) ->
- add_aliases_for_inductive_def status types suri
- | Cic.Constant _ -> add_alias_for_constant status suri
+ add_aliases_for_inductive_def status types uri
+ | Cic.Constant _ -> add_alias_for_constant status uri
| Cic.Variable _
| Cic.CurrentProof _ -> assert false
-let paths_and_uris_of_obj uri status =
- let basedir = get_string_option status "basedir" ^ "/xml" in
- let innertypesuri = UriManager.innertypesuri_of_uri uri in
- let bodyuri = UriManager.bodyuri_of_uri uri in
- let univgraphuri = UriManager.univgraphuri_of_uri uri in
- let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
- (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in
- let innertypespath = basedir ^ "/" ^ innertypesfilename in
- let xmlfilename = Str.replace_first (Str.regexp "^cic:/") ""
- (UriManager.string_of_uri uri) ^ ".xml.gz" in
- let xmlpath = basedir ^ "/" ^ xmlfilename in
- let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") ""
- (UriManager.string_of_uri uri) ^ ".body.xml.gz" in
- let xmlbodypath = basedir ^ "/" ^ xmlbodyfilename in
- let xmlunivgraphfilename = Str.replace_first (Str.regexp "^cic:/") ""
- (UriManager.string_of_uri univgraphuri) ^ ".xml.gz" in
- let xmlunivgraphpath = basedir ^ "/" ^ xmlunivgraphfilename in
- xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
- xmlunivgraphpath, univgraphuri
-
-let save_object_to_disk status uri obj ugraph univlist =
- let ensure_path_exists path =
- let dir = Filename.dirname path in
- HExtlib.mkdir dir
- in
- (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
- let annobj = Cic2acic.plain_acic_object_of_cic_object obj in
- (* prepare XML *)
- let xml, bodyxml =
- Cic2Xml.print_object
- uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj
- in
- let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
- xmlunivgraphpath, univgraphuri =
- paths_and_uris_of_obj uri status
- in
- List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]);
- (* now write to disk *)
- ensure_path_exists xmlpath;
- Xml.pp ~gzip:true xml (Some xmlpath);
- CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist;
- (* we return a list of uri,path we registered/created *)
- (uri,xmlpath) ::
- (univgraphuri,xmlunivgraphpath) ::
- (* now the optional body, both write and register *)
- (match bodyxml,bodyuri with
- None,None -> []
- | Some bodyxml,Some bodyuri->
- ensure_path_exists xmlbodypath;
- Xml.pp ~gzip:true bodyxml (Some xmlbodypath);
- [bodyuri, xmlbodypath]
- | _-> assert false)
-
-let typecheck_obj =
- let profiler = HExtlib.profile "add_obj.typecheck_obj" in
- fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
-
-let index_obj =
- let profiler = HExtlib.profile "add_obj.index_obj" in
- fun ~dbd ~uri ->
- profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
-
let add_obj uri obj status =
- let dbd = MatitaDb.instance () in
- let suri = UriManager.string_of_uri uri in
- if CicEnvironment.in_library uri then
- command_error (sprintf "%s already defined" suri)
- else begin
- typecheck_obj uri obj; (* 1 *)
- let _, ugraph, univlist =
- CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in
- try
- index_obj ~dbd ~uri; (* 2 must be in the env *)
- try
- let new_stuff=save_object_to_disk status uri obj ugraph univlist in(*3*)
- try
- MatitaLog.message (sprintf "%s defined" suri);
- let status = add_aliases_for_object status suri obj in
- { status with objects = new_stuff @ status.objects;
- proof_status = No_proof }
- with exc ->
- List.iter MatitaMisc.safe_remove (List.map snd new_stuff); (* -3 *)
- raise exc
- with exc ->
- ignore(MatitaDb.remove_uri uri); (* -2 *)
- raise exc
- with exc ->
- CicEnvironment.remove_obj uri; (* -1 *)
- raise exc
- end
+ let basedir = Helm_registry.get "matita.basedir" in
+ let status =
+ { add_aliases_for_object status uri obj with proof_status = No_proof}
+ in
+ LibrarySync.add_obj uri obj basedir;
+ status
let add_obj =
let profiler = HExtlib.profile "add_obj" in
let diff = S.diff s2 s1 in
S.fold (fun uri uris -> uri :: uris) diff []
-let remove_coercion uri =
- CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri)
-
let time_travel ~present ~past =
let objs_to_remove = urixstring_list_diff present.objects past.objects in
let coercions_to_remove = uri_list_diff present.coercions past.coercions in
id_list_diff present.notation_ids past.notation_ids
in
let debug_list = ref [] in
- List.iter remove_coercion coercions_to_remove;
+ List.iter
+ (fun uri -> CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri))
+ coercions_to_remove;
List.iter
(fun (uri,p) ->
- MatitaMisc.safe_remove p;
+ HExtlib.safe_remove p;
(try
CicEnvironment.remove_obj uri
with CicEnvironment.Object_not_found _ ->
- MatitaLog.debug
+ HLog.debug
(sprintf "time_travel removes from cache %s that is not in"
(UriManager.string_of_uri uri)));
- let l = MatitaDb.remove_uri uri in
+ let l = LibraryDb.remove_uri uri in
debug_list := UriManager.string_of_uri uri :: !debug_list @ l)
objs_to_remove;
List.iter CicNotation.remove_notation notation_to_remove
List.iter2 (fun x y -> if x <> y then raise Exit) l1 l2
with
| Invalid_argument _ | Exit ->
- MatitaLog.debug "It seems you garbaged something...";
- MatitaLog.debug "l1:";
- List.iter MatitaLog.debug l1;
- MatitaLog.debug "l2:";
- List.iter MatitaLog.debug l2
+ HLog.debug "It seems you garbaged something...";
+ HLog.debug "l1:";
+ List.iter HLog.debug l1;
+ HLog.debug "l2:";
+ List.iter HLog.debug l2
*)
-
-let last_baseuri = ref ""
-
-let remove ?(verbose=false) uri =
- let derived_uris_of_uri uri =
- UriManager.innertypesuri_of_uri uri ::
- UriManager.univgraphuri_of_uri uri ::
- (match UriManager.bodyuri_of_uri uri with
- | None -> []
- | Some u -> [u])
- in
- let to_remove =
- uri ::
- (if UriManager.uri_is_ind uri then MatitaDb.xpointers_of_ind uri else []) @
- derived_uris_of_uri uri
- in
- List.iter
- (fun uri ->
- (try
- (* WARNING: non reentrant debugging code *)
- if verbose then
- let baseuri = UriManager.buri_of_uri uri in
- if !last_baseuri <> baseuri then
- begin
- MatitaLog.debug ("Removing: " ^ baseuri ^ "/*");
- last_baseuri := baseuri
- end;
- let file = Http_getter.resolve' uri in
- MatitaMisc.safe_remove file;
- MatitaMisc.rmdir_descend (Filename.dirname file)
- with Http_getter_types.Key_not_found _ -> ());
- remove_coercion uri;
- ignore (MatitaDb.remove_uri uri);
- CicEnvironment.remove_obj uri)
- to_remove
MatitaTypes.status ->
(DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list ->
MatitaTypes.status
-
- (* removes the object from DB, Disk, CoercionsDB, CicEnvironment, getter
- * asserts the uri is resolved to file:// so it is only for
- * user's objects
- * @param verbose defaults to false *)
-val remove: ?verbose:bool -> UriManager.uri -> unit
-
{ status with proof_status = proof_status }
let dump_status status =
- MatitaLog.message "status.aliases:\n";
- MatitaLog.message "status.proof_status:";
- MatitaLog.message
+ HLog.message "status.aliases:\n";
+ HLog.message "status.proof_status:";
+ HLog.message
(match status.proof_status with
| No_proof -> "no proof\n"
| Incomplete_proof _ -> "incomplete proof\n"
| Proof _ -> "proof\n"
| Intermediate _ -> "Intermediate\n");
- MatitaLog.message "status.options\n";
+ HLog.message "status.options\n";
StringMap.iter (fun k v ->
let v =
match v with
| String s -> s
| Int i -> string_of_int i
in
- MatitaLog.message (k ^ "::=" ^ v)) status.options;
- MatitaLog.message "status.coercions\n";
- MatitaLog.message "status.objects:\n";
+ HLog.message (k ^ "::=" ^ v)) status.options;
+ HLog.message "status.coercions\n";
+ HLog.message "status.objects:\n";
List.iter
(fun (u,_) ->
- MatitaLog.message (UriManager.string_of_uri u)) status.objects
+ HLog.message (UriManager.string_of_uri u)) status.objects
let get_option status name =
try
let s = Str.global_replace (Str.regexp "/$") "" s in
s
in
- let types =
- [ "baseuri", (`String, mangle_dir);
- "basedir", (`String, mangle_dir);
- ]
- in
+ let types = [ "baseuri", (`String, mangle_dir); ] in
let ty_and_mangler =
try
List.assoc name types
type options = option_value StringMap.t
val no_options : 'a StringMap.t
-type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command
-type moo = ast_command list * GrafiteAst.metadata list (** <moo, metadata> *)
-
type status = {
aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
multi_aliases: DisambiguateTypes.multiple_environment;
- moo_content_rev: moo;
+ moo_content_rev: GrafiteMarshal.moo;
proof_status: proof_status; (** logical status *)
options: options;
objects: (UriManager.uri * string) list; (** in-scope objects, with paths *)
val set_metasenv: Cic.metasenv -> status -> status
(** list is not reversed, head command will be the first emitted *)
-val add_moo_content: ast_command list -> status -> status
+val add_moo_content: GrafiteMarshal.ast_command list -> status -> status
val add_moo_metadata: GrafiteAst.metadata list -> status -> status
val dump_status : status -> unit
else
stm
in
- MatitaLog.debug ("Executing: ``" ^ stm ^ "''"))
+ HLog.debug ("Executing: ``" ^ stm ^ "''"))
in
try
eval_function status is cb
| End_of_file
| CicNotationParser.Parse_error _ as exn -> raise exn
| exn ->
- MatitaLog.error (snd (MatitaExcPp.to_string exn));
+ HLog.error (snd (MatitaExcPp.to_string exn));
raise exn
let fname () =
| _ -> MatitaInit.die_usage ()
let pp_ocaml_mode () =
- MatitaLog.message "";
- MatitaLog.message " ** Entering Ocaml mode ** ";
- MatitaLog.message "";
- MatitaLog.message "Type 'go ();;' to enter an interactive matitac";
- MatitaLog.message ""
+ HLog.message "";
+ HLog.message " ** Entering Ocaml mode ** ";
+ HLog.message "";
+ HLog.message "Type 'go ();;' to enter an interactive matitac";
+ HLog.message ""
let clean_exit n =
let opt_exit =
| Some status ->
try
let baseuri = MatitaTypes.get_string_option !status "baseuri" in
- MatitacleanLib.clean_baseuris ~verbose:false [baseuri];
+ let basedir = Helm_registry.get "matita.basedir" in
+ LibraryClean.clean_baseuris ~basedir ~verbose:false [baseuri];
opt_exit n
with MatitaTypes.Option_error("baseuri", "not found") ->
(* no baseuri ==> nothing to clean yet *)
"matita.includes"))
with
| MatitaEngine.Drop -> pp_ocaml_mode ()
- | Sys.Break -> MatitaLog.error "user break!"; interactive_loop ()
+ | Sys.Break -> HLog.error "user break!"; interactive_loop ()
| MatitaTypes.Command_error _ -> interactive_loop ()
| End_of_file ->
print_newline ();
clean_exit (Some 0)
| HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
let (x, y) = HExtlib.loc_of_floc floc in
- MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err);
+ HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
interactive_loop ()
- | exn -> MatitaLog.error (Printexc.to_string exn); interactive_loop ()
+ | exn -> HLog.error (Printexc.to_string exn); interactive_loop ()
let go () =
Helm_registry.load_from BuildTimeConf.matita_conf;
CicNotation.load_notation BuildTimeConf.core_notation_script;
Http_getter.init ();
MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
- MatitaDb.create_owner_environment ();
+ LibraryDb.create_owner_environment ();
CicEnvironment.set_trust (* environment trust *)
(let trust = Helm_registry.get_bool "matita.environment_trust" in
fun _ -> trust);
let fname = fname () in
status := Some (ref (Lazy.force MatitaEngine.initial_status));
Sys.catch_break true;
- let origcb = MatitaLog.get_log_callback () in
+ let origcb = HLog.get_log_callback () in
let newcb tag s =
match tag with
| `Debug | `Message -> ()
| `Warning | `Error -> origcb tag s
in
if Helm_registry.get_bool "matita.quiet" then
- MatitaLog.set_log_callback newcb;
+ HLog.set_log_callback newcb;
let matita_debug = Helm_registry.get_bool "matita.debug" in
try
let time = Unix.time () in
if Helm_registry.get_bool "matita.quiet" then
origcb `Message ("compiling " ^ Filename.basename fname ^ "...")
else
- MatitaLog.message (sprintf "execution of %s started:" fname);
+ HLog.message (sprintf "execution of %s started:" fname);
let is =
Ulexing.from_utf8_channel
(match fname with
let hou =
if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else ""
in
- let proof_status,moo_content_rev =
+ let proof_status,moo_content_rev,status =
match !status with
- | Some s -> !s.proof_status, !s.moo_content_rev
+ | Some s -> !s.proof_status, !s.moo_content_rev, !s
| None -> assert false
in
if proof_status <> MatitaTypes.No_proof then
begin
- MatitaLog.error
+ HLog.error
"there are still incomplete proofs at the end of the script";
clean_exit (Some 2)
end
else
begin
- let moo_fname = MatitacleanLib.obj_file_of_script fname in
- MatitaMoo.save_moo moo_fname moo_content_rev;
- MatitaLog.message
+ let basedir = Helm_registry.get "matita.basedir" in
+ let moo_fname = MatitaMisc.obj_file_of_script ~basedir fname in
+ GrafiteMarshal.save_moo moo_fname moo_content_rev;
+ HLog.message
(sprintf "execution of %s completed in %s." fname (hou^min^sec));
exit 0
end
with
| Sys.Break ->
- MatitaLog.error "user break!";
+ HLog.error "user break!";
if mode = `COMPILER then
clean_exit (Some ~-1)
else
pp_ocaml_mode ()
| HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
let (x, y) = HExtlib.loc_of_floc floc in
- MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err);
+ HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
if mode = `COMPILER then
clean_exit (Some 1)
else
let _ = MatitaInit.initialize_all () in
let uris_to_remove = ref [] in
let files_to_remove = ref [] in
+ let basedir = Helm_registry.get "matita.basedir" in
(match Helm_registry.get_list Helm_registry.string "matita.args" with
| [ "all" ] ->
- MatitaDb.clean_owner_environment ();
- let xmldir = Helm_registry.get "matita.basedir" ^ "/xml" in
+ LibraryDb.clean_owner_environment ();
+ let xmldir = basedir ^ "/xml" in
ignore
(Sys.command
("find " ^ xmldir ^
UM.buri_of_uri (UM.uri_of_string suri)
with UM.IllFormedUri _ ->
files_to_remove := suri :: !files_to_remove;
- let u = MatitacleanLib.baseuri_of_file suri in
+ let u = MatitaMisc.baseuri_of_file suri in
if String.length u < 5 || String.sub u 0 5 <> "cic:/" then begin
- MatitaLog.error (sprintf "File %s defines a bad baseuri: %s"
+ HLog.error (sprintf "File %s defines a bad baseuri: %s"
suri u);
exit 1
end else
in
uris_to_remove := uri :: !uris_to_remove)
files);
- MatitacleanLib.clean_baseuris !uris_to_remove;
- let moos = List.map MatitacleanLib.obj_file_of_script !files_to_remove in
- List.iter MatitaMisc.safe_remove moos
+ LibraryClean.clean_baseuris ~basedir !uris_to_remove;
+ let moos =
+ List.map (MatitaMisc.obj_file_of_script ~basedir) !files_to_remove
+ in
+ List.iter HExtlib.safe_remove moos
+++ /dev/null
-(* Copyright (C) 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/
- *)
-
-open Printf
-
-let debug = false
-let debug_prerr = if debug then prerr_endline else ignore
-
-module HGT = Http_getter_types;;
-module HG = Http_getter;;
-module HGM = Http_getter_misc;;
-module UM = UriManager;;
-module TA = GrafiteAst;;
-
-let cache_of_processed_baseuri = Hashtbl.create 1024
-
-let one_step_depend suri =
- let buri =
- try
- UM.buri_of_uri (UM.uri_of_string suri)
- with UM.IllFormedUri _ -> suri
- in
- if Hashtbl.mem cache_of_processed_baseuri buri then
- []
- else
- begin
- Hashtbl.add cache_of_processed_baseuri buri true;
- let query =
- let buri = buri ^ "/" in
- let buri = HMysql.escape buri in
- let obj_tbl = MetadataTypes.obj_tbl () in
- sprintf
- ("SELECT source, h_occurrence FROM %s WHERE " ^^
- "h_occurrence REGEXP '^%s[^/]*$'")
- obj_tbl buri
- in
- try
- let rc = HMysql.exec (MatitaDb.instance ()) query in
- let l = ref [] in
- HMysql.iter rc (
- fun row ->
- match row.(0), row.(1) with
- | Some uri, Some occ when Filename.dirname occ = buri ->
- l := uri :: !l
- | _ -> ());
- let l = List.sort Pervasives.compare !l in
- HExtlib.list_uniq l
- with
- exn -> raise exn (* no errors should be accepted *)
- end
-
-let safe_buri_of_suri suri =
- try
- UM.buri_of_uri (UM.uri_of_string suri)
- with
- UM.IllFormedUri _ -> suri
-
-let close_uri_list uri_to_remove =
- (* to remove an uri you have to remove the whole script *)
- let buri_to_remove =
- HExtlib.list_uniq
- (List.fast_sort Pervasives.compare
- (List.map safe_buri_of_suri uri_to_remove))
- in
- (* cleand the already visided baseuris *)
- let buri_to_remove =
- List.filter
- (fun buri ->
- if Hashtbl.mem cache_of_processed_baseuri buri then false
- else true)
- buri_to_remove
- in
- (* now calculate the list of objects that belong to these baseuris *)
- let uri_to_remove =
- try
- List.fold_left
- (fun acc buri ->
- let inhabitants = HG.ls (buri ^ "/") in
- let inhabitants = List.filter
- (function HGT.Ls_object _ -> true | _ -> false)
- inhabitants
- in
- let inhabitants = List.map
- (function
- | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri
- | _ -> assert false)
- inhabitants
- in
- inhabitants @ acc)
- [] buri_to_remove
- with HGT.Invalid_URI u ->
- MatitaLog.error ("We were listing an invalid buri: " ^ u);
- exit 1
- in
- (* now we want the list of all uri that depend on them *)
- let depend =
- List.fold_left
- (fun acc u -> one_step_depend u @ acc) [] uri_to_remove
- in
- let depend =
- HExtlib.list_uniq (List.fast_sort Pervasives.compare depend)
- in
- uri_to_remove, depend
-
-let rec close_using_db uris next =
- match next with
- | [] -> uris
- | l -> let uris, next = close_uri_list l in close_using_db uris next @ uris
-
-let cleaned_no = ref 0;;
-
- (** TODO repellent code ... *)
-let moo_root_dir = lazy (
- let url =
- List.assoc "cic:/matita/"
- (List.map
- (fun pair ->
- match
- Str.split (Str.regexp "[ \t\r\n]+") (HExtlib.trim_blanks pair)
- with
- | [a;b] -> a, b
- | _ -> assert false)
- (Helm_registry.get_list Helm_registry.string "getter.prefix"))
- in
- String.sub url 7 (String.length url - 7) (* remove heading "file:///" *)
-)
-
-let close_using_moos buris =
- let rev_deps = Hashtbl.create 97 in
- let all_moos =
- HExtlib.find ~test:(fun name -> Filename.check_suffix name ".moo")
- (Lazy.force moo_root_dir)
- in
- List.iter
- (fun path ->
- let _, metadata = MatitaMoo.load_moo ~fname:path in
- let baseuri_of_current_moo =
- let rec aux = function
- | [] -> assert false
- | GrafiteAst.Baseuri buri::_ -> buri
- | _ :: tl -> aux tl
- in
- aux metadata
- in
- let deps =
- HExtlib.filter_map
- (function
- | GrafiteAst.Dependency buri -> Some buri
- | _ -> None )
- metadata
- in
- List.iter
- (fun buri -> Hashtbl.add rev_deps buri baseuri_of_current_moo) deps)
- all_moos;
- let buris_to_remove =
- HExtlib.list_uniq
- (List.fast_sort Pervasives.compare
- (List.flatten (List.map (Hashtbl.find_all rev_deps) buris)))
- in
- let objects_to_remove =
- let objs_of_buri buri =
- HExtlib.filter_map
- (function
- | Http_getter_types.Ls_object o ->
- Some (buri ^ "/" ^ o.Http_getter_types.uri)
- | _ -> None)
- (Http_getter.ls buri)
- in
- List.flatten (List.map objs_of_buri (buris @ buris_to_remove))
- in
- objects_to_remove
-
-let clean_baseuris ?(verbose=true) buris =
- Hashtbl.clear cache_of_processed_baseuri;
- let buris = List.map HGM.strip_trailing_slash buris in
- debug_prerr "clean_baseuris called on:";
- if debug then
- List.iter debug_prerr buris;
- let l =
- if Helm_registry.get_bool "db.nodb" then
- close_using_moos buris
- else
- close_using_db [] buris
- in
- let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in
- let l = List.map UriManager.uri_of_string l in
- debug_prerr "clean_baseuri will remove:";
- if debug then
- List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l;
- List.iter
- (fun buri ->
- MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri))
- (HExtlib.list_uniq (List.fast_sort Pervasives.compare
- (List.map (UriManager.buri_of_uri) l)));
- List.iter (MatitaSync.remove ~verbose) l;
- cleaned_no := !cleaned_no + List.length l;
- if !cleaned_no > 30 then
- begin
- cleaned_no := 0;
- List.iter
- (function table ->
- ignore (HMysql.exec (MatitaDb.instance ()) ("OPTIMIZE TABLE " ^ table)))
- [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
- MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
- MetadataTypes.count_tbl()]
- end
-
-let baseuri_of_file file =
- let uri = ref None in
- let ic = open_in file in
- let istream = Ulexing.from_utf8_channel ic in
- (try
- while true do
- try
- let stm = GrafiteParser.parse_statement istream in
- match MatitaMisc.baseuri_of_baseuri_decl stm with
- | Some buri ->
- let u = MatitaMisc.strip_trailing_slash buri in
- if String.length u < 5 || String.sub u 0 5 <> "cic:/" then
- MatitaLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
- (try
- ignore(Http_getter.resolve u)
- with
- | Http_getter_types.Unresolvable_URI _ ->
- MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri)
- | Http_getter_types.Key_not_found _ -> ());
- uri := Some u;
- raise End_of_file
- | None -> ()
- with
- CicNotationParser.Parse_error _ as exn ->
- prerr_endline ("Unable to parse: " ^ file);
- prerr_endline (snd (MatitaExcPp.to_string exn));
- ()
- done
- with End_of_file -> close_in ic);
- match !uri with
- | Some uri -> uri
- | None -> failwith ("No baseuri defined in " ^ file)
-
-let obj_file_of_script f =
- if f = "coq.ma" then BuildTimeConf.coq_notation_script else
- let baseuri = baseuri_of_file f in
- MatitaMisc.obj_file_of_baseuri baseuri
-
+++ /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/
- *)
-
-val clean_baseuris : ?verbose:bool -> string list -> unit
-
-val baseuri_of_file: string -> string
-val obj_file_of_script : string -> string
-
try
aux paths
with Sys_error _ as exc ->
- MatitaLog.error ("Unable to read " ^ path);
- MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths);
+ HLog.error ("Unable to read " ^ path);
+ HLog.error ("opts.include_paths was " ^ String.concat ":" paths);
raise exc
in
MatitaInit.load_configuration_file ();
MatitaInit.parse_cmdline ();
+ let basedir = Helm_registry.get "matita.basedir" in
List.iter
(fun file ->
let ic = open_in file in
| GrafiteAst.IncludeDep path ->
try
let ma_file = if path <> "coq.ma" then find path else path in
- let moo_file = MatitacleanLib.obj_file_of_script ma_file in
+ let moo_file = MatitaMisc.obj_file_of_script ~basedir ma_file in
Hashtbl.add include_deps file moo_file
with Sys_error _ ->
- MatitaLog.warn
+ HLog.warn
("Unable to find " ^ path ^ " that is included in " ^ file))
dependencies)
(Helm_registry.get_list Helm_registry.string "matita.args");
match dep with
| None -> ()
| Some u ->
- Hashtbl.add include_deps file (MatitaMisc.obj_file_of_baseuri u))
+ Hashtbl.add include_deps file
+ (LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri:u))
uri_deps;
List.iter
(fun file ->
let deps = List.fast_sort Pervasives.compare deps in
let deps = HExtlib.list_uniq deps in
let deps = file :: deps in
- let moo = MatitacleanLib.obj_file_of_script file in
+ let moo = MatitaMisc.obj_file_of_script ~basedir file in
Printf.printf "%s: %s\n" moo (String.concat " " deps);
Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" file) moo)
(Helm_registry.get_list Helm_registry.string "matita.args")
let logger = fun mark ->
match mark with
- | `Error -> MatitaLog.error
- | `Warning -> MatitaLog.warn
- | `Debug -> MatitaLog.debug
- | `Message -> MatitaLog.message
+ | `Error -> HLog.error
+ | `Warning -> HLog.warn
+ | `Debug -> HLog.debug
+ | `Message -> HLog.message
;;
type development =
let rex_noendline = Pcre.regexp "\\n" in
let s = Pcre.replace ~rex:rex_noendline s in
let tokens = Pcre.split ~rex s in
- let logger = ref MatitaLog.message in
+ let logger = ref HLog.message in
let rec aux =
function
| [] -> ()
| s::tl ->
(if Pcre.pmatch ~rex:rex_i s then
- logger := MatitaLog.message
+ logger := HLog.message
else if Pcre.pmatch ~rex:rex_w s then
- logger := MatitaLog.warn
+ logger := HLog.warn
else if Pcre.pmatch ~rex:rex_e s then
- logger := MatitaLog.error
+ logger := HLog.error
else if Pcre.pmatch ~rex:rex_d s then
- logger := MatitaLog.debug
+ logger := HLog.debug
else
!logger s);
aux tl
-requires="helm-cic_proof_checking"
+requires="helm-cic_proof_checking helm-library"
version="0.0.1"
archive(byte)="cic_unification.cma"
archive(native)="cic_unification.cmxa"
--- /dev/null
+requires="helm-grafite helm-metadata"
+version="0.0.1"
+archive(byte)="library.cma"
+archive(native)="library.cmxa"
+linkopts=""
getter \
cic \
cic_proof_checking \
- cic_unification \
cic_acic \
acic_content \
content_pres \
grafite \
metadata \
+ library \
+ cic_unification \
whelp \
tactics \
cic_disambiguation \
-coercGraph.cmi: coercDb.cmi
cicMetaSubst.cmo: cicMetaSubst.cmi
cicMetaSubst.cmx: cicMetaSubst.cmi
cicMkImplicit.cmo: cicMkImplicit.cmi
cicMkImplicit.cmx: cicMkImplicit.cmi
cicUnification.cmo: cicMetaSubst.cmi cicUnification.cmi
cicUnification.cmx: cicMetaSubst.cmx cicUnification.cmi
-coercDb.cmo: coercDb.cmi
-coercDb.cmx: coercDb.cmi
-coercGraph.cmo: coercDb.cmi coercGraph.cmi
-coercGraph.cmx: coercDb.cmx coercGraph.cmi
+coercGraph.cmo: coercGraph.cmi
+coercGraph.cmx: coercGraph.cmi
cicRefine.cmo: coercGraph.cmi cicUnification.cmi cicMkImplicit.cmi \
cicMetaSubst.cmi cicRefine.cmi
cicRefine.cmx: coercGraph.cmx cicUnification.cmx cicMkImplicit.cmx \
cicMetaSubst.mli \
cicMkImplicit.mli \
cicUnification.mli \
- coercDb.mli \
coercGraph.mli \
cicRefine.mli
IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
+++ /dev/null
-(* Copyright (C) 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/
- *)
-
-type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
-exception EqCarrNotImplemented of string Lazy.t
-exception EqCarrOnNonMetaClosed
-
-let db = ref []
-let use_coercions = ref true
-
-let coerc_carr_of_term t =
- try
- Uri (CicUtil.uri_of_term t)
- with Invalid_argument _ ->
- match t with
- | Cic.Sort s -> Sort s
- | t -> Term t
-;;
-
-let eq_carr src tgt =
- match src, tgt with
- | Uri src, Uri tgt -> UriManager.eq src tgt
- | Sort (Cic.Type _), Sort (Cic.Type _) -> true
- | Sort src, Sort tgt when src = tgt -> true
- | Term t1, Term t2 ->
- if CicUtil.is_meta_closed t1 && CicUtil.is_meta_closed t2 then
- raise
- (EqCarrNotImplemented
- (lazy ("Unsupported carr for coercions: " ^
- CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2)))
- else raise EqCarrOnNonMetaClosed
- | _, _ -> false
-
-let name_of_carr = function
- | Uri u -> UriManager.name_of_uri u
- | Sort s -> CicPp.ppsort s
- | Term t -> CicPp.ppterm t
-
-
-let to_list () =
- !db
-
-let add_coercion c =
- db := c :: !db
-
-let remove_coercion p =
- db := List.filter (fun u -> not(p u)) !db
-
-let find_coercion f =
- if !use_coercions then
- List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db)
- else []
-
+++ /dev/null
-(* Copyright (C) 2000, 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://cs.unibo.it/helm/.
- *)
-
- (** XXX WARNING: non-reentrant *)
-type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
-exception EqCarrNotImplemented of string Lazy.t
-exception EqCarrOnNonMetaClosed
-val eq_carr: coerc_carr -> coerc_carr -> bool
-val coerc_carr_of_term: Cic.term -> coerc_carr
-val name_of_carr: coerc_carr -> string
-
-val use_coercions: bool ref (** initial status is true *)
-
-val to_list:
- unit ->
- (coerc_carr * coerc_carr * UriManager.uri) list
-
-val add_coercion:
- coerc_carr * coerc_carr * UriManager.uri -> unit
-
-val remove_coercion:
- (coerc_carr * coerc_carr * UriManager.uri -> bool) -> unit
-
-val find_coercion:
- (coerc_carr * coerc_carr -> bool) -> UriManager.uri list
-
hExtlib.cmx: hExtlib.cmi
patternMatcher.cmo: patternMatcher.cmi
patternMatcher.cmx: patternMatcher.cmi
+hLog.cmo: hLog.cmi
+hLog.cmx: hLog.cmi
INTERFACE_FILES = \
hExtlib.mli \
patternMatcher.mli \
+ hLog.mli \
$(NULL)
IMPLEMENTATION_FILES = \
$(INTERFACE_FILES:%.mli=%.ml)
in
aux [] [path]
+let safe_remove fname = if Sys.file_exists fname then Sys.remove fname
+
+let is_dir_empty d =
+ let od = Unix.opendir d in
+ let rec aux () =
+ let name = Unix.readdir od in
+ if name <> "." && name <> ".." then false else aux () in
+ let res = try aux () with End_of_file -> true in
+ Unix.closedir od;
+ res
+
+let safe_rmdir d = try Unix.rmdir d with Unix.Unix_error _ -> ()
+
+let rec rmdir_descend d =
+ if is_dir_empty d then
+ begin
+ safe_rmdir d;
+ rmdir_descend (Filename.dirname d)
+ end
+
+
(** {2 Exception handling} *)
let finally at_end f arg =
val is_regular: string -> bool (** @return true if file is a regular file *)
val mkdir: string -> unit (** create dir and parents. @raise Failure *)
val tilde_expand: string -> string (** bash-like (head) tilde expansion *)
+val safe_remove: string -> unit (** removes a file if it exists *)
+val safe_rmdir: string -> unit (** removes a dir if it exists and is empty *)
+val is_dir_empty: string -> bool (** checks if the dir is empty *)
+val rmdir_descend: string -> unit (** rmdir -p *)
+
(** find all _files_ matching test under a filesystem root *)
val find: ?test:(string -> bool) -> string -> string list
--- /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/
+ *)
+
+open Printf
+
+type log_tag = [ `Debug | `Error | `Message | `Warning ]
+type log_callback = log_tag -> string -> unit
+
+(*
+colors=(black red green yellow blue magenta cyan gray white)
+ccodes=(30 31 32 33 34 35 36 37 39)
+*)
+
+let blue = "\e[0;34m"
+let yellow = "\e[0;33m"
+let green = "\e[0;32m"
+let red = "\e[0;31m"
+let black = "\e[0m"
+
+let default_callback tag s =
+ let prefix,ch =
+ match tag with
+ | `Message -> green ^ "Info: ", stdout
+ | `Warning -> yellow ^ "Warn: ", stderr
+ | `Error -> red ^ "Error: ", stderr
+ | `Debug -> blue ^ "Debug: ", stderr
+ in
+ output_string ch (prefix ^ black ^ s ^ "\n");
+ flush ch
+
+let callback = ref default_callback
+
+let set_log_callback f = callback := f
+let get_log_callback () = !callback
+
+let message s = !callback `Message s
+let warn s = !callback `Warning s
+let error s = !callback `Error s
+let debug s = !callback `Debug s
+
--- /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/
+ *)
+
+type log_tag = [ `Debug | `Error | `Message | `Warning ]
+type log_callback = log_tag -> string -> unit
+
+val set_log_callback: log_callback -> unit
+val get_log_callback: unit -> log_callback
+
+val message : string -> unit
+val warn : string -> unit
+val error : string -> unit
+val debug : string -> unit
+
grafiteAstPp.cmi: grafiteAst.cmo
grafiteParser.cmi: grafiteAst.cmo
cicNotation.cmi: grafiteAst.cmo
+grafiteMarshal.cmi: grafiteAst.cmo
grafiteAstPp.cmo: grafiteAst.cmo grafiteAstPp.cmi
grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi
grafiteParser.cmo: grafiteAst.cmo grafiteParser.cmi
grafiteParser.cmx: grafiteAst.cmx grafiteParser.cmi
cicNotation.cmo: grafiteParser.cmi grafiteAst.cmo cicNotation.cmi
cicNotation.cmx: grafiteParser.cmx grafiteAst.cmx cicNotation.cmi
+grafiteMarshal.cmo: grafiteAst.cmo grafiteMarshal.cmi
+grafiteMarshal.cmx: grafiteAst.cmx grafiteMarshal.cmi
grafiteAstPp.mli \
grafiteParser.mli \
cicNotation.mli \
+ grafiteMarshal.mli \
$(NULL)
IMPLEMENTATION_FILES = \
grafiteAst.ml \
--- /dev/null
+(* Copyright (C) 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/
+ *)
+
+exception Checksum_failure of string
+exception Corrupt_moo of string
+exception Version_mismatch of string
+
+type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command
+type moo = ast_command list * GrafiteAst.metadata list (** <moo, metadata> *)
+
+let marshal_flags = []
+
+(** .moo file format
+ * - an integer -- magic number -- denoting the version of the dumped data
+ * structure. Different magic numbers stand for incompatible data structures
+ * - an integer -- checksum -- denoting the hash value (computed with
+ * Hashtbl.hash) of the string representation of the dumped data structur
+ * - marshalled pair: first component is a list of GrafiteAst.command (real moo
+ * content), second component is a list of GrafiteAst.metadata
+ *)
+
+let save_moo ~fname (moo, metadata) =
+ let oc = open_out fname in
+ let marshalled =
+ Marshal.to_string (List.rev moo, List.rev metadata) marshal_flags
+ in
+ let checksum = Hashtbl.hash marshalled in
+ output_binary_int oc GrafiteAst.magic;
+ output_binary_int oc checksum;
+ output_string oc marshalled;
+ close_out oc
+
+let load_moo ~fname =
+ let ic = open_in fname in
+ HExtlib.finally
+ (fun () -> close_in ic)
+ (fun () ->
+ try
+ let moo_magic = input_binary_int ic in
+ if moo_magic <> GrafiteAst.magic then raise (Version_mismatch fname);
+ let moo_checksum = input_binary_int ic in
+ let marshalled = HExtlib.input_all ic in
+ let checksum = Hashtbl.hash marshalled in
+ if checksum <> moo_checksum then raise (Checksum_failure fname);
+ let (moo:moo) =
+ Marshal.from_string marshalled 0
+ in
+ moo
+ with End_of_file -> raise (Corrupt_moo fname))
+ ()
+
--- /dev/null
+(* Copyright (C) 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/
+ *)
+
+ (** name of the corrupt .moo file *)
+exception Checksum_failure of string
+exception Corrupt_moo of string
+exception Version_mismatch of string
+
+type ast_command = (CicNotationPt.term, CicNotationPt.obj) GrafiteAst.command
+type moo = ast_command list * GrafiteAst.metadata list (** <moo, metadata> *)
+
+val save_moo: fname:string -> moo -> unit
+
+ (** @raise Corrupt_moo *)
+val load_moo: fname:string -> moo
+
--- /dev/null
+*.cmi
+*.cma
+*.cmo
+*.cmx
+*.cmxa
+*.o
+*.a
--- /dev/null
+PACKAGE = library
+PREDICATES =
+
+INTERFACE_FILES = \
+ libraryMisc.mli \
+ libraryDb.mli \
+ coercDb.mli \
+ librarySync.mli \
+ libraryClean.mli \
+ $(NULL)
+IMPLEMENTATION_FILES = \
+ $(INTERFACE_FILES:%.mli=%.ml)
+
+include ../Makefile.common
--- /dev/null
+(* Copyright (C) 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/
+ *)
+
+type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
+exception EqCarrNotImplemented of string Lazy.t
+exception EqCarrOnNonMetaClosed
+
+let db = ref []
+let use_coercions = ref true
+
+let coerc_carr_of_term t =
+ try
+ Uri (CicUtil.uri_of_term t)
+ with Invalid_argument _ ->
+ match t with
+ | Cic.Sort s -> Sort s
+ | t -> Term t
+;;
+
+let eq_carr src tgt =
+ match src, tgt with
+ | Uri src, Uri tgt -> UriManager.eq src tgt
+ | Sort (Cic.Type _), Sort (Cic.Type _) -> true
+ | Sort src, Sort tgt when src = tgt -> true
+ | Term t1, Term t2 ->
+ if CicUtil.is_meta_closed t1 && CicUtil.is_meta_closed t2 then
+ raise
+ (EqCarrNotImplemented
+ (lazy ("Unsupported carr for coercions: " ^
+ CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2)))
+ else raise EqCarrOnNonMetaClosed
+ | _, _ -> false
+
+let name_of_carr = function
+ | Uri u -> UriManager.name_of_uri u
+ | Sort s -> CicPp.ppsort s
+ | Term t -> CicPp.ppterm t
+
+
+let to_list () =
+ !db
+
+let add_coercion c =
+ db := c :: !db
+
+let remove_coercion p =
+ db := List.filter (fun u -> not(p u)) !db
+
+let find_coercion f =
+ if !use_coercions then
+ List.map (fun (_,_,x) -> x) (List.filter (fun (s,t,_) -> f (s,t)) !db)
+ else []
+
--- /dev/null
+(* Copyright (C) 2000, 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://cs.unibo.it/helm/.
+ *)
+
+ (** XXX WARNING: non-reentrant *)
+type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
+exception EqCarrNotImplemented of string Lazy.t
+exception EqCarrOnNonMetaClosed
+val eq_carr: coerc_carr -> coerc_carr -> bool
+val coerc_carr_of_term: Cic.term -> coerc_carr
+val name_of_carr: coerc_carr -> string
+
+val use_coercions: bool ref (** initial status is true *)
+
+val to_list:
+ unit ->
+ (coerc_carr * coerc_carr * UriManager.uri) list
+
+val add_coercion:
+ coerc_carr * coerc_carr * UriManager.uri -> unit
+
+val remove_coercion:
+ (coerc_carr * coerc_carr * UriManager.uri -> bool) -> unit
+
+val find_coercion:
+ (coerc_carr * coerc_carr -> bool) -> UriManager.uri list
+
--- /dev/null
+(* Copyright (C) 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/
+ *)
+
+open Printf
+
+let debug = false
+let debug_prerr = if debug then prerr_endline else ignore
+
+module HGT = Http_getter_types;;
+module HG = Http_getter;;
+module HGM = Http_getter_misc;;
+module UM = UriManager;;
+module TA = GrafiteAst;;
+
+let cache_of_processed_baseuri = Hashtbl.create 1024
+
+let one_step_depend suri =
+ let buri =
+ try
+ UM.buri_of_uri (UM.uri_of_string suri)
+ with UM.IllFormedUri _ -> suri
+ in
+ if Hashtbl.mem cache_of_processed_baseuri buri then
+ []
+ else
+ begin
+ Hashtbl.add cache_of_processed_baseuri buri true;
+ let query =
+ let buri = buri ^ "/" in
+ let buri = HMysql.escape buri in
+ let obj_tbl = MetadataTypes.obj_tbl () in
+ sprintf
+ ("SELECT source, h_occurrence FROM %s WHERE " ^^
+ "h_occurrence REGEXP '^%s[^/]*$'")
+ obj_tbl buri
+ in
+ try
+ let rc = HMysql.exec (LibraryDb.instance ()) query in
+ let l = ref [] in
+ HMysql.iter rc (
+ fun row ->
+ match row.(0), row.(1) with
+ | Some uri, Some occ when Filename.dirname occ = buri ->
+ l := uri :: !l
+ | _ -> ());
+ let l = List.sort Pervasives.compare !l in
+ HExtlib.list_uniq l
+ with
+ exn -> raise exn (* no errors should be accepted *)
+ end
+
+let safe_buri_of_suri suri =
+ try
+ UM.buri_of_uri (UM.uri_of_string suri)
+ with
+ UM.IllFormedUri _ -> suri
+
+let close_uri_list uri_to_remove =
+ (* to remove an uri you have to remove the whole script *)
+ let buri_to_remove =
+ HExtlib.list_uniq
+ (List.fast_sort Pervasives.compare
+ (List.map safe_buri_of_suri uri_to_remove))
+ in
+ (* cleand the already visided baseuris *)
+ let buri_to_remove =
+ List.filter
+ (fun buri ->
+ if Hashtbl.mem cache_of_processed_baseuri buri then false
+ else true)
+ buri_to_remove
+ in
+ (* now calculate the list of objects that belong to these baseuris *)
+ let uri_to_remove =
+ try
+ List.fold_left
+ (fun acc buri ->
+ let inhabitants = HG.ls (buri ^ "/") in
+ let inhabitants = List.filter
+ (function HGT.Ls_object _ -> true | _ -> false)
+ inhabitants
+ in
+ let inhabitants = List.map
+ (function
+ | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri
+ | _ -> assert false)
+ inhabitants
+ in
+ inhabitants @ acc)
+ [] buri_to_remove
+ with HGT.Invalid_URI u ->
+ HLog.error ("We were listing an invalid buri: " ^ u);
+ exit 1
+ in
+ (* now we want the list of all uri that depend on them *)
+ let depend =
+ List.fold_left
+ (fun acc u -> one_step_depend u @ acc) [] uri_to_remove
+ in
+ let depend =
+ HExtlib.list_uniq (List.fast_sort Pervasives.compare depend)
+ in
+ uri_to_remove, depend
+
+let rec close_using_db uris next =
+ match next with
+ | [] -> uris
+ | l -> let uris, next = close_uri_list l in close_using_db uris next @ uris
+
+let cleaned_no = ref 0;;
+
+ (** TODO repellent code ... *)
+let moo_root_dir = lazy (
+ let url =
+ List.assoc "cic:/matita/"
+ (List.map
+ (fun pair ->
+ match
+ Str.split (Str.regexp "[ \t\r\n]+") (HExtlib.trim_blanks pair)
+ with
+ | [a;b] -> a, b
+ | _ -> assert false)
+ (Helm_registry.get_list Helm_registry.string "getter.prefix"))
+ in
+ String.sub url 7 (String.length url - 7) (* remove heading "file:///" *)
+)
+
+let close_using_moos buris =
+ let rev_deps = Hashtbl.create 97 in
+ let all_moos =
+ HExtlib.find ~test:(fun name -> Filename.check_suffix name ".moo")
+ (Lazy.force moo_root_dir)
+ in
+ List.iter
+ (fun path ->
+ let _, metadata = GrafiteMarshal.load_moo ~fname:path in
+ let baseuri_of_current_moo =
+ let rec aux = function
+ | [] -> assert false
+ | GrafiteAst.Baseuri buri::_ -> buri
+ | _ :: tl -> aux tl
+ in
+ aux metadata
+ in
+ let deps =
+ HExtlib.filter_map
+ (function
+ | GrafiteAst.Dependency buri -> Some buri
+ | _ -> None )
+ metadata
+ in
+ List.iter
+ (fun buri -> Hashtbl.add rev_deps buri baseuri_of_current_moo) deps)
+ all_moos;
+ let buris_to_remove =
+ HExtlib.list_uniq
+ (List.fast_sort Pervasives.compare
+ (List.flatten (List.map (Hashtbl.find_all rev_deps) buris)))
+ in
+ let objects_to_remove =
+ let objs_of_buri buri =
+ HExtlib.filter_map
+ (function
+ | Http_getter_types.Ls_object o ->
+ Some (buri ^ "/" ^ o.Http_getter_types.uri)
+ | _ -> None)
+ (Http_getter.ls buri)
+ in
+ List.flatten (List.map objs_of_buri (buris @ buris_to_remove))
+ in
+ objects_to_remove
+
+let clean_baseuris ?(verbose=true) ~basedir buris =
+ Hashtbl.clear cache_of_processed_baseuri;
+ let buris = List.map HGM.strip_trailing_slash buris in
+ debug_prerr "clean_baseuris called on:";
+ if debug then
+ List.iter debug_prerr buris;
+ let l =
+ if Helm_registry.get_bool "db.nodb" then
+ close_using_moos buris
+ else
+ close_using_db [] buris
+ in
+ let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in
+ let l = List.map UriManager.uri_of_string l in
+ debug_prerr "clean_baseuri will remove:";
+ if debug then
+ List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l;
+ List.iter
+ (fun buri ->
+ HExtlib.safe_remove (LibraryMisc.obj_file_of_baseuri basedir buri))
+ (HExtlib.list_uniq (List.fast_sort Pervasives.compare
+ (List.map (UriManager.buri_of_uri) l)));
+ List.iter
+ (let last_baseuri = ref "" in
+ fun uri ->
+ let buri = UriManager.buri_of_uri uri in
+ if buri <> !last_baseuri then
+ begin
+ HLog.message ("Removing: " ^ buri ^ "/*");
+ last_baseuri := buri
+ end;
+ LibrarySync.remove_obj uri
+ ) l;
+ cleaned_no := !cleaned_no + List.length l;
+ if !cleaned_no > 30 then
+ begin
+ cleaned_no := 0;
+ List.iter
+ (function table ->
+ ignore (HMysql.exec (LibraryDb.instance ()) ("OPTIMIZE TABLE " ^ table)))
+ [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
+ MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
+ MetadataTypes.count_tbl()]
+ end
--- /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/
+ *)
+
+val clean_baseuris : ?verbose:bool -> basedir:string -> string list -> unit
--- /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/
+ *)
+
+open Printf ;;
+
+let instance =
+ let dbd = lazy (
+ HMysql.quick_connect
+ ~host:(Helm_registry.get "db.host")
+ ~user:(Helm_registry.get "db.user")
+ ~database:(Helm_registry.get "db.database")
+ ())
+ in
+ fun () -> Lazy.force dbd
+
+
+let xpointer_RE = Pcre.regexp "#.*$"
+let file_scheme_RE = Pcre.regexp "^file://"
+
+let clean_owner_environment () =
+ let dbd = instance () in
+ let owner = (Helm_registry.get "matita.owner") in
+ 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
+ let owned_uris =
+ try
+ MetadataDb.clean ~dbd
+ with Mysql.Error _ as exn ->
+ match HMysql.errno dbd with
+ | Mysql.No_such_table -> []
+ | _ -> raise exn
+ in
+ List.iter
+ (fun uri ->
+ let uri = Pcre.replace ~rex:xpointer_RE ~templ:"" uri in
+ List.iter
+ (fun suffix ->
+ try
+ HExtlib.safe_remove (Http_getter.resolve (uri ^ suffix))
+ with Http_getter_types.Key_not_found _ -> ())
+ [""; ".body"; ".types"])
+ owned_uris;
+ List.iter (fun statement ->
+ try
+ ignore (HMysql.exec dbd statement)
+ with Mysql.Error _ as exn ->
+ match HMysql.errno dbd with
+ | Mysql.Bad_table_error
+ | Mysql.No_such_index | Mysql.No_such_table -> ()
+ | _ -> raise exn
+ ) statements;
+;;
+
+let create_owner_environment () =
+ let dbd = instance () in
+ 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 (HMysql.exec dbd statement)
+ with
+ exn ->
+ let status = HMysql.status dbd in
+ match status with
+ | Mysql.StatusError Mysql.Table_exists_error -> ()
+ | Mysql.StatusError Mysql.Dup_keyname -> ()
+ | Mysql.StatusError _ -> raise exn
+ | _ -> ()
+ ) statements
+;;
+
+(* removes uri from the ownerized tables, and returns the list of other objects
+ * (theyr uris) that ref the one removed.
+ * AFAIK there is no need to return it, since the MatitaTypes.staus should
+ * contain all defined objects. but to double check we do not garbage the
+ * metadata...
+ *)
+let remove_uri uri =
+ 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 conclno_tbl = MetadataTypes.conclno_tbl () in
+ let conclno_hyp_tbl = MetadataTypes.fullno_tbl () in*)
+ let count_tbl = MetadataTypes.count_tbl () in
+
+ let dbd = instance () in
+ let suri = UriManager.string_of_uri uri in
+ let query table suri = sprintf
+ "DELETE FROM %s WHERE source LIKE '%s%%'" table (HMysql.escape suri)
+ in
+ List.iter (fun t ->
+ try
+ ignore (HMysql.exec dbd (query t suri))
+ with
+ exn -> raise exn (* no errors should be accepted *)
+ )
+ [obj_tbl;sort_tbl;rel_tbl;name_tbl;(*conclno_tbl;conclno_hyp_tbl*)count_tbl];
+ (* and now the debug job *)
+ let dbg_q =
+ sprintf "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl
+ (HMysql.escape suri)
+ in
+ try
+ let rc = HMysql.exec dbd dbg_q in
+ let l = ref [] in
+ HMysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
+ let l = List.sort Pervasives.compare !l in
+ HExtlib.list_uniq l
+ with
+ exn -> raise exn (* no errors should be accepted *)
+
+let xpointers_of_ind uri =
+ let dbd = instance () in
+ let name_tbl = MetadataTypes.name_tbl () in
+ let query = sprintf
+ "SELECT source FROM %s WHERE source LIKE '%s#xpointer%%'" name_tbl
+ (HMysql.escape (UriManager.string_of_uri uri))
+ in
+ let rc = HMysql.exec dbd query in
+ let l = ref [] in
+ HMysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
+ List.map UriManager.uri_of_string !l
+
--- /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/
+ *)
+
+val instance: unit -> HMysql.dbd
+
+val create_owner_environment: unit -> unit
+val clean_owner_environment: unit -> unit
+
+(* returns a list of uri thet must be removed sice they reference uri,
+ * but this is used only for debugging purposes *)
+val remove_uri: UriManager.uri -> string list
+val xpointers_of_ind: UriManager.uri -> UriManager.uri list
--- /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 obj_file_of_baseuri ~basedir ~baseuri =
+ let path = basedir ^ "/xml" ^ Pcre.replace ~pat:"^cic:" ~templ:"" baseuri in
+ path ^ ".moo"
--- /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/
+ *)
+
+
+val obj_file_of_baseuri: basedir:string -> baseuri:string -> string
--- /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/
+ *)
+
+exception AlreadyDefined of UriManager.uri
+
+let uris_of_obj uri =
+ let innertypesuri = UriManager.innertypesuri_of_uri uri in
+ let bodyuri = UriManager.bodyuri_of_uri uri in
+ let univgraphuri = UriManager.univgraphuri_of_uri uri in
+ innertypesuri,bodyuri,univgraphuri
+
+let paths_and_uris_of_obj uri ~basedir =
+ let basedir = basedir ^ "/xml" in
+ let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
+ let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
+ (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in
+ let innertypespath = basedir ^ "/" ^ innertypesfilename in
+ let xmlfilename = Str.replace_first (Str.regexp "^cic:/") ""
+ (UriManager.string_of_uri uri) ^ ".xml.gz" in
+ let xmlpath = basedir ^ "/" ^ xmlfilename in
+ let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") ""
+ (UriManager.string_of_uri uri) ^ ".body.xml.gz" in
+ let xmlbodypath = basedir ^ "/" ^ xmlbodyfilename in
+ let xmlunivgraphfilename = Str.replace_first (Str.regexp "^cic:/") ""
+ (UriManager.string_of_uri univgraphuri) ^ ".xml.gz" in
+ let xmlunivgraphpath = basedir ^ "/" ^ xmlunivgraphfilename in
+ xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
+ xmlunivgraphpath, univgraphuri
+
+let save_object_to_disk ~basedir uri obj ugraph univlist =
+ let ensure_path_exists path =
+ let dir = Filename.dirname path in
+ HExtlib.mkdir dir
+ in
+ (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
+ let annobj = Cic2acic.plain_acic_object_of_cic_object obj in
+ (* prepare XML *)
+ let xml, bodyxml =
+ Cic2Xml.print_object
+ uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj
+ in
+ let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri,
+ xmlunivgraphpath, univgraphuri =
+ paths_and_uris_of_obj uri basedir
+ in
+ List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]);
+ (* now write to disk *)
+ ensure_path_exists xmlpath;
+ Xml.pp ~gzip:true xml (Some xmlpath);
+ CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist;
+ (* we return a list of uri,path we registered/created *)
+ (uri,xmlpath) ::
+ (univgraphuri,xmlunivgraphpath) ::
+ (* now the optional body, both write and register *)
+ (match bodyxml,bodyuri with
+ None,None -> []
+ | Some bodyxml,Some bodyuri->
+ ensure_path_exists xmlbodypath;
+ Xml.pp ~gzip:true bodyxml (Some xmlbodypath);
+ [bodyuri, xmlbodypath]
+ | _-> assert false)
+
+
+let typecheck_obj =
+ let profiler = HExtlib.profile "add_obj.typecheck_obj" in
+ fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
+
+let index_obj =
+ let profiler = HExtlib.profile "add_obj.index_obj" in
+ fun ~dbd ~uri ->
+ profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri
+
+let add_obj uri obj ~basedir =
+ let dbd = LibraryDb.instance () in
+ if CicEnvironment.in_library uri then
+ raise (AlreadyDefined uri)
+ else begin
+ typecheck_obj uri obj; (* 1 *)
+ let _, ugraph, univlist =
+ CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in
+ try
+ index_obj ~dbd ~uri; (* 2 must be in the env *)
+ try
+ (*3*)
+ let new_stuff = save_object_to_disk ~basedir uri obj ugraph univlist in
+ try
+ HLog.message
+ (Printf.sprintf "%s defined" (UriManager.string_of_uri uri))
+ with exc ->
+ List.iter HExtlib.safe_remove (List.map snd new_stuff); (* -3 *)
+ raise exc
+ with exc ->
+ ignore(LibraryDb.remove_uri uri); (* -2 *)
+ raise exc
+ with exc ->
+ CicEnvironment.remove_obj uri; (* -1 *)
+ raise exc
+ end
+
+let remove_obj uri =
+ let derived_uris_of_uri uri =
+ let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
+ innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u])
+ in
+ let to_remove =
+ uri ::
+ (if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else []) @
+ derived_uris_of_uri uri
+ in
+ List.iter
+ (fun uri ->
+ (try
+ let file = Http_getter.resolve' uri in
+ HExtlib.safe_remove file;
+ HExtlib.rmdir_descend (Filename.dirname file)
+ with Http_getter_types.Key_not_found _ -> ());
+ ignore (LibraryDb.remove_uri uri);
+ CoercDb.remove_coercion (fun (_,_,u) -> UriManager.eq u uri);
+ CicEnvironment.remove_obj uri)
+ to_remove
--- /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/
+ *)
+
+(* returns a list of added URIs and their paths on disk *)
+(*CSC: the path on disk should be computable from the URI!!! *)
+val add_obj: UriManager.uri -> Cic.obj -> basedir:string -> unit
+
+(* inverse of add_obj; it does not remove the objects depending on it! *)
+val remove_obj: UriManager.uri -> unit
projects / helm.git / commitdiff