From b2f2e47efe1e01df81cb7659c30eeb76f1f830da Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 26 Sep 2005 08:58:45 +0000 Subject: [PATCH] - added integrity checks on .moo files - removed a lot of auxiliary functions from MatitaMisc since they are now part of our extlib --- helm/matita/.depend | 85 ++++++++++++++++++----------------- helm/matita/Makefile.in | 14 ++++-- helm/matita/dump_moo.ml | 55 +++++++++++++++++++++++ helm/matita/matita.ml | 1 - helm/matita/matitaEngine.ml | 14 +++--- helm/matita/matitaExcPp.ml | 9 ++++ helm/matita/matitaGui.ml | 7 +-- helm/matita/matitaMathView.ml | 8 ++-- helm/matita/matitaMisc.ml | 65 --------------------------- helm/matita/matitaMisc.mli | 22 --------- helm/matita/matitaMoo.ml | 67 +++++++++++++++++++++++++++ helm/matita/matitaMoo.mli | 35 +++++++++++++++ helm/matita/matitaScript.ml | 6 +-- helm/matita/matitaSync.ml | 7 ++- helm/matita/matitacLib.ml | 8 +--- helm/matita/matitacLib.mli | 6 --- helm/matita/matitamakeLib.ml | 12 ++--- 17 files changed, 248 insertions(+), 173 deletions(-) create mode 100644 helm/matita/dump_moo.ml create mode 100644 helm/matita/matitaMoo.ml create mode 100644 helm/matita/matitaMoo.mli diff --git a/helm/matita/.depend b/helm/matita/.depend index d8a04bf10..be561c24a 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,31 +1,45 @@ -matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ - matitaMathView.cmi matitaLog.cmi matitaInit.cmi matitaGui.cmi \ - matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmo -matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ - matitaMathView.cmx matitaLog.cmx matitaInit.cmx matitaGui.cmx \ - matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx +dump_moo.cmo: matitaMoo.cmi matitaLog.cmi buildTimeConf.cmo +dump_moo.cmx: matitaMoo.cmx matitaLog.cmx buildTimeConf.cmx +matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ + matitacleanLib.cmi +matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ + matitacleanLib.cmi +matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi \ + matitaInit.cmi matitaDb.cmi +matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx \ + matitaInit.cmx matitaDb.cmx +matitacLib.cmo: matitacleanLib.cmi matitaTypes.cmi matitaMoo.cmi \ + matitaMisc.cmi matitaLog.cmi matitaInit.cmi matitaExcPp.cmi \ + matitaEngine.cmi matitaDb.cmi buildTimeConf.cmo matitacLib.cmi +matitacLib.cmx: matitacleanLib.cmx matitaTypes.cmx matitaMoo.cmx \ + matitaMisc.cmx matitaLog.cmx matitaInit.cmx matitaExcPp.cmx \ + matitaEngine.cmx matitaDb.cmx buildTimeConf.cmx matitacLib.cmi +matitac.cmo: matitacLib.cmi +matitac.cmx: matitacLib.cmx matitaDb.cmo: matitaMisc.cmi matitaDb.cmi matitaDb.cmx: matitaMisc.cmx matitaDb.cmi +matitadep.cmo: matitaMisc.cmi matitaLog.cmi matitaInit.cmi buildTimeConf.cmo +matitadep.cmx: matitaMisc.cmx matitaLog.cmx matitaInit.cmx buildTimeConf.cmx matitaDisambiguator.cmo: matitaTypes.cmi matitaDisambiguator.cmi matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi matitaEngine.cmo: matitacleanLib.cmi matitaTypes.cmi matitaSync.cmi \ - matitaMisc.cmi matitaLog.cmi matitaDisambiguator.cmi matitaDb.cmi \ - matitaEngine.cmi + matitaMoo.cmi matitaMisc.cmi matitaLog.cmi matitaDisambiguator.cmi \ + matitaDb.cmi matitaEngine.cmi matitaEngine.cmx: matitacleanLib.cmx matitaTypes.cmx matitaSync.cmx \ - matitaMisc.cmx matitaLog.cmx matitaDisambiguator.cmx matitaDb.cmx \ - matitaEngine.cmi -matitaExcPp.cmo: matitaTypes.cmi matitaExcPp.cmi -matitaExcPp.cmx: matitaTypes.cmx matitaExcPp.cmi + matitaMoo.cmx matitaMisc.cmx matitaLog.cmx matitaDisambiguator.cmx \ + matitaDb.cmx matitaEngine.cmi +matitaExcPp.cmo: matitaTypes.cmi matitaMoo.cmi matitaExcPp.cmi +matitaExcPp.cmx: matitaTypes.cmx matitaMoo.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 matitacLib.cmi \ - matitaTypes.cmi matitaScript.cmi matitaMisc.cmi matitaMathView.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 matitacLib.cmx \ - matitaTypes.cmx matitaScript.cmx matitaMisc.cmx matitaMathView.cmx \ +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 \ @@ -34,6 +48,10 @@ 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 +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 matitaMathView.cmi @@ -44,6 +62,14 @@ matitaMisc.cmo: matitaTypes.cmi matitaLog.cmi matitaExcPp.cmi \ buildTimeConf.cmo matitaMisc.cmi matitaMisc.cmx: matitaTypes.cmx matitaLog.cmx matitaExcPp.cmx \ buildTimeConf.cmx matitaMisc.cmi +matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi matitaLog.cmi \ + matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi matitaEngine.cmi \ + buildTimeConf.cmo +matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx matitaLog.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 buildTimeConf.cmo matitaScript.cmi @@ -56,32 +82,6 @@ matitaSync.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ matitaSync.cmi matitaTypes.cmo: matitaLog.cmi matitaTypes.cmi matitaTypes.cmx: matitaLog.cmx matitaTypes.cmi -matitac.cmo: matitacLib.cmi -matitac.cmx: matitacLib.cmx -matitacLib.cmo: matitacleanLib.cmi matitaTypes.cmi matitaMisc.cmi \ - matitaLog.cmi matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ - matitaDb.cmi buildTimeConf.cmo matitacLib.cmi -matitacLib.cmx: matitacleanLib.cmx matitaTypes.cmx matitaMisc.cmx \ - matitaLog.cmx matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ - matitaDb.cmx buildTimeConf.cmx matitacLib.cmi -matitaclean.cmo: matitacleanLib.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ - buildTimeConf.cmo -matitaclean.cmx: matitacleanLib.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ - buildTimeConf.cmx -matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaLog.cmi matitaDb.cmi \ - matitacleanLib.cmi -matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \ - matitacleanLib.cmi -matitadep.cmo: matitaMisc.cmi matitaLog.cmi matitaInit.cmi matitaExcPp.cmi \ - buildTimeConf.cmo -matitadep.cmx: matitaMisc.cmx matitaLog.cmx matitaInit.cmx matitaExcPp.cmx \ - buildTimeConf.cmx -matitamake.cmo: matitamakeLib.cmi matitaInit.cmi -matitamake.cmx: matitamakeLib.cmx matitaInit.cmx -matitamakeLib.cmo: matitaMisc.cmi matitaLog.cmi buildTimeConf.cmo \ - matitamakeLib.cmi -matitamakeLib.cmx: matitaMisc.cmx matitaLog.cmx buildTimeConf.cmx \ - matitamakeLib.cmi matitaDisambiguator.cmi: matitaTypes.cmi matitaEngine.cmi: matitaTypes.cmi matitaGtkMisc.cmi: matitaGeneratedGui.cmi @@ -89,5 +89,6 @@ matitaGui.cmi: matitaGuiTypes.cmi matitaDisambiguator.cmi matitaGuiTypes.cmi: matitaTypes.cmi matitaLog.cmi matitaGeneratedGui.cmi matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi matitaMisc.cmi: matitaTypes.cmi +matitaMoo.cmi: matitaTypes.cmi matitaScript.cmi: matitaTypes.cmi matitaSync.cmi: matitaTypes.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index a519950b0..301eb2efc 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -26,6 +26,7 @@ CMOS = \ buildTimeConf.cmo \ matitaLog.cmo \ matitaTypes.cmo \ + matitaMoo.cmo \ matitaExcPp.cmo \ matitaMisc.cmo \ matitaDb.cmo \ @@ -47,6 +48,7 @@ CCMOS = \ buildTimeConf.cmo \ matitaLog.cmo \ matitaTypes.cmo \ + matitaMoo.cmo \ matitaExcPp.cmo \ matitaMisc.cmo \ matitaDb.cmo \ @@ -60,8 +62,10 @@ CCMOS = \ $(NULL) CLEANCMOS = $(CCMOS) MAKECMOS = $(CCMOS) +PROGRAMS = matita matitac matitatop cicbrowser matitadep matitaclean matitamake +PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS)) -all: matita.conf.xml matita matitac matitatop cicbrowser matitadep matitaclean matitamake +all: matita.conf.xml $(PROGRAMS) dump_moo matita.conf.xml: matita.conf.xml.sample @if diff matita.conf.xml.sample matita.conf.xml 1>/dev/null 2>/dev/null; then\ @@ -98,7 +102,7 @@ CLEANLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -forma CLEANLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(CLEANREQUIRES)) MAKELIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MAKEREQUIRES)) MAKELIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MAKEREQUIRES)) -opt: matita.opt matitac.opt cicbrowser.opt matitadep.opt matitaclean.opt matitamake.opt +opt: $(PROGRAMS_OPT) else opt: @echo "Native code compilation is disabled" @@ -109,6 +113,9 @@ matita: $(LIB_DEPS) $(CMOS) matita.ml 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 + $(OCAMLC) $(PKGS) -linkpkg -o $@ $^ + matitac: $(CLIB_DEPS) $(CCMOS) matitac.ml $(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) matitac.ml matitac.opt: $(CLIBX_DEPS) $(CCMXS) matitac.ml @@ -157,7 +164,8 @@ clean: matitadep matitadep.opt \ matitaclean matitaclean.opt \ matitamake matitamake.opt \ - matitatop matitatop.opt + matitatop matitatop.opt \ + dump_moo distclean: clean rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli rm -f config.log config.status Makefile buildTimeConf.ml diff --git a/helm/matita/dump_moo.ml b/helm/matita/dump_moo.ml new file mode 100644 index 000000000..43d11f9bc --- /dev/null +++ b/helm/matita/dump_moo.ml @@ -0,0 +1,55 @@ +(* 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 arg_spec = + let std_arg_spec = [] in + let debug_arg_spec = [] in + std_arg_spec @ debug_arg_spec + +let usage = + sprintf "MatitaC v%s\nUsage: dump_moo [option ...] file.moo\nOptions:" + BuildTimeConf.version + +let _ = + let moos = ref [] in + let add_moo fname = moos := fname :: !moos in + Arg.parse arg_spec add_moo usage; + if !moos = [] then begin print_endline usage; exit 1 end; + List.iter + (fun fname -> + if not (Sys.file_exists fname) then + MatitaLog.error (sprintf "Can't find moo '%s', skipping it." fname) + else begin + printf "%s:\n" fname; flush stdout; + let commands = MatitaMoo.load_moo ~fname in + List.iter + (fun cmd -> + printf " %s\n" (GrafiteAstPp.pp_command cmd); flush stdout) + commands + end) + (List.rev !moos) + diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 45ad19556..c3fdb2459 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -27,7 +27,6 @@ open Printf open MatitaGtkMisc open MatitaTypes -open MatitaMisc (** {2 Initialization} *) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 0bd5acb95..b06504052 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -634,7 +634,7 @@ let generate_projections uri fields status = ) status projections (* to avoid a long list of recursive functions *) -let eval_from_dump_ref = ref (fun _ _ _ -> assert false);; +let eval_from_moo_ref = ref (fun _ _ _ -> assert false);; let disambiguate_obj status obj = let uri = @@ -712,7 +712,7 @@ let eval_command opts status cmd = let status = ref status in if not (Sys.file_exists moopath) then raise (IncludedFileNotCompiled moopath); - !eval_from_dump_ref status moopath (fun _ _ -> ()); + !eval_from_moo_ref status moopath (fun _ _ -> ()); !status | GrafiteAst.Set (loc, name, value) -> let value = @@ -884,18 +884,16 @@ let eval_ast | GrafiteAst.Executable (_,ex) -> eval_executable opts status ex | GrafiteAst.Comment (_,c) -> eval_comment status c -let eval_from_dump ?do_heavy_checks ?include_paths ?clean_baseuri status fname +let eval_from_moo ?do_heavy_checks ?include_paths ?clean_baseuri status fname cb = - let ic = open_in fname in - let moo = Marshal.from_channel ic in - close_in ic; + let moo = MatitaMoo.load_moo fname in List.iter (fun ast -> let ast = GrafiteAst.Executable (DisambiguateTypes.dummy_floc, GrafiteAst.Command (DisambiguateTypes.dummy_floc, - (GrafiteAst.reash_uris ast))) + (GrafiteAst.reash_cmd_uris ast))) in cb !status ast; status := @@ -915,7 +913,7 @@ let eval_from_stream with End_of_file -> () (* to avoid a long list of recursive functions *) -let _ = eval_from_dump_ref := eval_from_dump +let _ = eval_from_moo_ref := eval_from_moo let eval_from_stream_greedy ?do_heavy_checks ?include_paths ?clean_baseuri status str cb diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml index f141b129a..fce5cf6d9 100644 --- a/helm/matita/matitaExcPp.ml +++ b/helm/matita/matitaExcPp.ml @@ -40,5 +40,14 @@ let to_string = | Unix.Unix_error (code, api, param) -> let err = Unix.error_message code in "Unix Error (" ^ api ^ "): " ^ err + | MatitaMoo.Corrupt_moo fname -> + sprintf ".moo file '%s' is corrupt (shorter than expected)" fname + | MatitaMoo.Checksum_failure fname -> + sprintf "checksum failed for .moo file '%s', please recompile it'" fname + | MatitaMoo.Version_mismatch fname -> + sprintf + (".moo file '%s' has been compiled by a different version of matita, " + ^^ "please recompile it") + fname | exn -> "Uncaught exception: " ^ Printexc.to_string exn diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index e2e490942..5d223208f 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -67,7 +67,8 @@ let clean_current_baseuri status = let ask_and_save_moo_if_needed parent fname status = let save () = - MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev in + let moo_fname = MatitaMisc.obj_file_of_script fname in + MatitaMoo.save_moo moo_fname status.MatitaTypes.moo_content_rev in if (MatitaScript.instance ())#eos && status.MatitaTypes.proof_status = MatitaTypes.No_proof then @@ -494,9 +495,9 @@ class gui () = let fname = fileSel#fileSelectionWin#filename in if Sys.file_exists fname then begin - if is_regular fname && not(_only_directory) then + if HExtlib.is_regular fname && not (_only_directory) then return (Some fname) - else if _only_directory && is_dir fname then + else if _only_directory && HExtlib.is_dir fname then return (Some fname) end else diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 28bd1caaa..6074fdae7 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -206,7 +206,7 @@ object (self) match href_callback with | None -> () | Some f -> - (match MatitaMisc.split href_value with + (match HExtlib.split href_value with | [ uri ] -> f uri | uris -> let menu = GMenu.menu () in @@ -738,11 +738,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_showMath; match self#script#status.proof_status with | Proof (uri, metasenv, bo, ty) -> - let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in + let name = UriManager.name_of_uri (HExtlib.unopt uri) in let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in self#_loadObj obj | Incomplete_proof ((uri, metasenv, bo, ty), _) -> - let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in + let name = UriManager.name_of_uri (HExtlib.unopt uri) in let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in self#_loadObj obj | _ -> self#blank () @@ -798,7 +798,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (** this is what the browser does when you enter a string an hit enter *) method loadInput txt = - let txt = MatitaMisc.trim_blanks txt in + let txt = HExtlib.trim_blanks txt in let fix_uri txt = UriManager.string_of_uri (UriManager.strip_xpointer (UriManager.uri_of_string txt)) diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 56cb4a295..9c0c7db33 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -80,29 +80,6 @@ let is_empty buri = let safe_remove fname = if Sys.file_exists fname then Sys.remove fname -let is_dir fname = - try - (Unix.stat fname).Unix.st_kind = Unix.S_DIR - with Unix.Unix_error _ -> false - -let is_regular fname = - try - (Unix.stat fname).Unix.st_kind = Unix.S_REG - with Unix.Unix_error _ -> false - -let input_file fname = - let size = (Unix.stat fname).Unix.st_size in - let buf = Buffer.create size in - let ic = open_in fname in - Buffer.add_channel buf ic size; - close_in ic; - Buffer.contents buf - -let output_file data file = - let oc = open_out file in - output_string oc data; - close_out oc - let absolute_path file = if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file @@ -116,40 +93,6 @@ let append_phrase_sep s = else s -let mkdir path = - let components = Str.split (Str.regexp "/") path in - let rec aux where = function - | [] -> () - | piece::tl -> - let path = where ^ "/" ^ piece in - (try - Unix.mkdir path 0o755 - with - | Unix.Unix_error (Unix.EEXIST,_,_) -> () - | Unix.Unix_error (e,_,_) -> - raise - (Failure - ("Unix.mkdir " ^ path ^ " 0o755 :" ^ (Unix.error_message e)))); - aux path tl - in - aux "" components - -let trim_blanks = - let rex = Pcre.regexp "^\\s*(.*?)\\s*$" in - fun s -> (Pcre.extract ~rex s).(1) - -let split ?(char = ' ') s = - let pieces = ref [] in - let rec aux idx = - match (try Some (String.index_from s idx char) with Not_found -> None) with - | Some pos -> - pieces := String.sub s idx (pos - idx) :: !pieces; - aux (pos + 1) - | None -> pieces := String.sub s idx (String.length s - idx) :: !pieces - in - aux 0; - List.rev !pieces - let empty_mathml () = DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns) ~qualifiedName:(Gdome.domString "math") ~doctype:None @@ -280,8 +223,6 @@ let get_proof_conclusion status = let qualify status name = get_string_option status "baseuri" ^ "/" ^ name -let unopt = function None -> failwith "unopt: None" | Some v -> v - let image_path n = sprintf "%s/%s" BuildTimeConf.images_dir n let end_ma_RE = Pcre.regexp "\\.ma$" @@ -313,9 +254,3 @@ let list_tl_at ?(equality=(==)) e l = in aux l -let debug_wrap name f = - prerr_endline (sprintf "debug_wrap: ==>> %s" name); - let res = f () in - prerr_endline (sprintf "debug_wrap: <<== %s" name); - res - diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index 21045c0a3..bf51c64e9 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -34,12 +34,6 @@ val is_empty: string -> bool (** removes a file if it exists *) val safe_remove: string -> unit -val is_dir: string -> bool (** @return true if file is a directory *) -val is_regular: string -> bool (** @return true if file is a regular file *) - -val input_file: string -> string (** read all the contents of file to string *) -val output_file: string -> string -> unit (** write string to file *) - val absolute_path: string -> string (** @return true if file is a (textual) proof script *) @@ -52,14 +46,10 @@ val is_proof_object: string -> bool * it *) val append_phrase_sep: string -> string -val trim_blanks: string -> string val strip_trailing_slash: string -> string val normalize_dir: string -> string (** add trailing "/" if missing *) val strip_suffix: suffix:string -> string -> string - (* split a string at character, char defaults to ' ' *) -val split: ?char:char -> string -> string list - val list_uniq: 'a list -> 'a list (* uniq unix filter on lists *) (** @return tl tail of a list starting at a given element @@ -67,9 +57,6 @@ val list_uniq: 'a list -> 'a list (* uniq unix filter on lists *) * @raise Not_found *) val list_tl_at: ?equality:('a -> 'a -> bool) -> 'a -> 'a list -> 'a list - (** @raise Failure *) -val unopt: 'a option -> 'a - (** Gdome.element of a MathML document whose rendering should be blank. Used * by cicBrowser to render "about:blank" document *) val empty_mathml: unit -> Gdome.document @@ -103,10 +90,6 @@ class ['a] browser_history: ?memento:'a memento -> int -> 'a -> ['a] history * first time it gets called. Next invocation will return first value *) val singleton: (unit -> 'a) -> (unit -> 'a) - (** create a directory, building also parents if needed - * @raise Failure when unable to create some directory *) -val mkdir: string -> unit - val qualify: MatitaTypes.status -> string -> string val get_proof_status: MatitaTypes.status -> ProofEngineTypes.status @@ -119,8 +102,3 @@ val image_path: string -> string val obj_file_of_baseuri: string -> string val obj_file_of_script: string -> string - (** invoke a given function and return its value; in addition il will print - * the given string before invoking it and "/" ^ the given string afterwards. - * This permit tracing of functions which does not return a value *) -val debug_wrap: string -> (unit -> 'a) -> 'a - diff --git a/helm/matita/matitaMoo.ml b/helm/matita/matitaMoo.ml new file mode 100644 index 000000000..ea5c748bd --- /dev/null +++ b/helm/matita/matitaMoo.ml @@ -0,0 +1,67 @@ +(* 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 list of GrafiteAst.command + *) + +let save_moo ~fname moo = + let oc = open_out fname in + let marshalled_moo = Marshal.to_string (List.rev moo) marshal_flags in + let checksum = Hashtbl.hash marshalled_moo in + output_binary_int oc GrafiteAst.magic; + output_binary_int oc checksum; + output_string oc marshalled_moo; + 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_moo = HExtlib.input_all ic in + let checksum = Hashtbl.hash marshalled_moo in + if checksum <> moo_checksum then raise (Checksum_failure fname); + let (moo: MatitaTypes.ast_command list) = + Marshal.from_string marshalled_moo 0 + in + moo + with End_of_file -> raise (Corrupt_moo fname)) + () + diff --git a/helm/matita/matitaMoo.mli b/helm/matita/matitaMoo.mli new file mode 100644 index 000000000..3959a120a --- /dev/null +++ b/helm/matita/matitaMoo.mli @@ -0,0 +1,35 @@ +(* 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.ast_command list -> unit + + (** @raise Corrupt_moo *) +val load_moo: fname:string -> MatitaTypes.ast_command list + diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index c58e0fa39..334f3cbe1 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -232,7 +232,7 @@ let eval_macro guistuff status unparsed_text parsed_text script mac = let l = MQ.match_term ~dbd term in let query_url = MatitaMisc.strip_suffix ~suffix:"." - (MatitaMisc.trim_blanks unparsed_text) + (HExtlib.trim_blanks unparsed_text) in let entry = `Whelp (query_url, l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; @@ -583,7 +583,7 @@ object (self) List.iter (fun o -> o status) observers method loadFromFile f = - buffer#set_text (MatitaMisc.input_file f); + buffer#set_text (HExtlib.input_file f); self#reset_buffer; buffer#set_modified false @@ -629,7 +629,7 @@ object (self) buffer#set_modified false method template () = - let template = MatitaMisc.input_file BuildTimeConf.script_template in + let template = HExtlib.input_file BuildTimeConf.script_template in buffer#insert ~iter:(buffer#get_iter `START) template; guistuff.filenamedata <- (None,MatitamakeLib.development_for_dir (Unix.getcwd ())); diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index 9a8cb10ee..3383ee312 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -125,7 +125,7 @@ let paths_and_uris_of_obj uri status = let save_object_to_disk status uri obj ugraph univlist = let ensure_path_exists path = let dir = Filename.dirname path in - MatitaMisc.mkdir dir + 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 @@ -139,14 +139,13 @@ let save_object_to_disk status uri obj ugraph univlist = paths_and_uris_of_obj uri status in let path_scheme_of path = "file://" ^ path in - List.iter MatitaMisc.mkdir - (List.map Filename.dirname [innertypespath; xmlpath]); + 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) :: (innertypesuri,innertypespath) :: + (uri,xmlpath) :: (univgraphuri,xmlunivgraphpath) :: (* now the optional body, both write and register *) (match bodyxml,bodyuri with diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index 48a2f2f9e..fa7e487a9 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -157,11 +157,6 @@ let go () = Sys.catch_break true; interactive_loop () -let dump_moo_to_file file moo = - let os = open_out (MatitaMisc.obj_file_of_script file) in - Marshal.to_channel os (List.rev moo) []; - close_out os - let main ~mode = MatitaInit.initialize_all (); status := Some (ref (Lazy.force MatitaEngine.initial_status)); @@ -215,7 +210,8 @@ let main ~mode = end else begin - dump_moo_to_file fname moo_content_rev; + let moo_fname = MatitaMisc.obj_file_of_script fname in + MatitaMoo.save_moo moo_fname moo_content_rev; MatitaLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); exit 0 diff --git a/helm/matita/matitacLib.mli b/helm/matita/matitacLib.mli index 7c07402d8..636c51d57 100644 --- a/helm/matita/matitacLib.mli +++ b/helm/matita/matitacLib.mli @@ -29,12 +29,6 @@ val interactive_loop : unit -> unit val go : unit -> unit val main : mode:[ `COMPILER | `TOPLEVEL ] -> unit -(** fname is the .ma *) -val dump_moo_to_file: - string -> - (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command list -> - unit - (** clean_exit n if n = Some n it performs an exit [n] after a complete clean-up of what was partially compiled diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml index 6e0d5660c..16f2c67c6 100644 --- a/helm/matita/matitamakeLib.ml +++ b/helm/matita/matitamakeLib.ml @@ -55,7 +55,7 @@ let ls_dir dir = let initialize () = (* create a base env if none *) - MatitaMisc.mkdir (pool ()); + HExtlib.mkdir (pool ()); (* load developments *) match ls_dir (pool ()) with | None -> logger `Error ("Unable to list directory " ^ pool ()) @@ -64,7 +64,7 @@ let initialize () = (fun name -> let root = try - Some (MatitaMisc.input_file (pool () ^ name ^ rootfile)) + Some (HExtlib.input_file (pool () ^ name ^ rootfile)) with Unix.Unix_error _ -> logger `Warning ("Malformed development " ^ name); None @@ -106,8 +106,8 @@ let development_for_name name = (* dumps the deveopment to disk *) let dump_development devel = let devel_dir = pool () ^ devel.name in - MatitaMisc.mkdir devel_dir; - MatitaMisc.output_file devel.root (devel_dir ^ rootfile); + HExtlib.mkdir devel_dir; + HExtlib.output_file ~filename:(devel_dir ^ rootfile) ~text:devel.root ;; let list_known_developments () = @@ -119,7 +119,7 @@ let am_i_opt () = let rebuild_makefile development = let makefilepath = makefile_for_development development in let template = - MatitaMisc.input_file BuildTimeConf.matitamake_makefile_template + HExtlib.input_file BuildTimeConf.matitamake_makefile_template in let cc = BuildTimeConf.runtime_base_dir ^ "/matitac" ^ am_i_opt () in let rm = BuildTimeConf.runtime_base_dir ^ "/matitaclean" ^ am_i_opt () in @@ -130,7 +130,7 @@ let rebuild_makefile development = let template = Pcre.replace ~pat:"@DEP@" ~templ:mm template in let template = Pcre.replace ~pat:"@DEPFILE@" ~templ:df template in let template = Pcre.replace ~pat:"@CLEAN@" ~templ:rm template in - MatitaMisc.output_file template makefilepath + HExtlib.output_file ~filename:makefilepath ~text:template (* creates a new development if possible *) let initialize_development name dir = -- 2.39.2