From efdb0db81ef2594a2aced0310997ef0d74462254 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 22 Jul 2005 13:29:52 +0000 Subject: [PATCH] Big changes: 1. the .moo files are now kept in the logical structure (i.e. in .matita/xml/*) 2. matitaclean is now able to correctly remove all the .moo files 3. the compilation target in library and tests is now foo.mo (it used to be foo.moo) and it is PHONY --- helm/matita/.depend | 24 +++++++----- helm/matita/library/Makefile | 4 +- helm/matita/matitaEngine.ml | 2 +- helm/matita/matitaMisc.ml | 66 +++++++++++++++++++++++++++++--- helm/matita/matitaMisc.mli | 8 ++++ helm/matita/matitaScript.ml | 7 ++-- helm/matita/matitaclean.ml | 2 +- helm/matita/matitacleanLib.ml | 52 ++++--------------------- helm/matita/matitacleanLib.mli | 7 ---- helm/matita/matitadep.ml | 35 ++++++++--------- helm/matita/matitamakeLib.ml | 4 +- helm/matita/template_makefile.in | 17 ++------ helm/matita/tests/Makefile | 4 +- 13 files changed, 119 insertions(+), 113 deletions(-) diff --git a/helm/matita/.depend b/helm/matita/.depend index 95ab00934..c7246ac01 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -8,10 +8,12 @@ matitaDb.cmo: matitaMisc.cmi matitaDb.cmi matitaDb.cmx: matitaMisc.cmx matitaDb.cmi matitaDisambiguator.cmo: matitaTypes.cmi matitaDisambiguator.cmi matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi -matitaEngine.cmo: matitaTypes.cmi matitaSync.cmi matitaMisc.cmi matitaLog.cmi \ - matitaDisambiguator.cmi matitaDb.cmi matitaEngine.cmi -matitaEngine.cmx: matitaTypes.cmx matitaSync.cmx matitaMisc.cmx matitaLog.cmx \ - matitaDisambiguator.cmx matitaDb.cmx matitaEngine.cmi +matitaEngine.cmo: matitacleanLib.cmi matitaTypes.cmi matitaSync.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 matitaGeneratedGui.cmo: matitaGeneratedGui.cmi @@ -34,8 +36,10 @@ matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaGui.cmx matitaGtkMisc.cmx matitaExcPp.cmx buildTimeConf.cmx \ matitaMathView.cmi -matitaMisc.cmo: matitaTypes.cmi buildTimeConf.cmo matitaMisc.cmi -matitaMisc.cmx: matitaTypes.cmx buildTimeConf.cmx matitaMisc.cmi +matitaMisc.cmo: matitaTypes.cmi matitaLog.cmi matitaExcPp.cmi \ + buildTimeConf.cmo matitaMisc.cmi +matitaMisc.cmx: matitaTypes.cmx matitaLog.cmx matitaExcPp.cmx \ + buildTimeConf.cmx matitaMisc.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 @@ -60,10 +64,10 @@ 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 \ - matitaExcPp.cmi matitaDb.cmi matitacleanLib.cmi -matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaLog.cmx \ - matitaExcPp.cmx matitaDb.cmx matitacleanLib.cmi +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 matitaExcPp.cmi buildTimeConf.cmo matitadep.cmx: matitaMisc.cmx matitaLog.cmx matitaExcPp.cmx buildTimeConf.cmx matitamake.cmo: matitamakeLib.cmi buildTimeConf.cmo diff --git a/helm/matita/library/Makefile b/helm/matita/library/Makefile index 392294579..4e85bcccc 100644 --- a/helm/matita/library/Makefile +++ b/helm/matita/library/Makefile @@ -15,7 +15,7 @@ DEPEND_NAME=.depend H=@ -all: $(SRC:%.ma=%.moo) +all: $(SRC:%.ma=%.mo) opt: $(H)make MATITAC="$(MATITACOPT)" MATITACLEAN="$(MATITACLEANOPT)" MATITADEP="$(MATITADEPOPT)" all @@ -38,7 +38,7 @@ depend: make $(DEPEND_NAME) .PHONY: depend -%.moo:%.ma +%.moo: $(H)$(MATITAC) $< $(DEPEND_NAME): $(SRC) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 9707149d5..5c8a55eaf 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -550,7 +550,7 @@ let eval_command opts status cmd = else value in - if not (MatitacleanLib.is_empty value) then + if not (MatitaMisc.is_empty value) then begin MatitaLog.warn ("baseuri " ^ value ^ " is not empty"); if opts.clean_baseuri then diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 99fea1a32..c12a14527 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -26,6 +26,56 @@ open Printf open MatitaTypes +let strip_trailing_slash = + let rex = Pcre.regexp "/$" in + fun s -> Pcre.replace ~rex s + +let baseuri_of_baseuri_decl st = + match st with + | GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Set (_, "baseuri", buri))) -> + Some buri + | _ -> None + +let baseuri_of_file file = + let uri = ref None in + let ic = open_in file in + let istream = Stream.of_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 + 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 (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 is_empty buri = + List.for_all + (function + Http_getter_types.Ls_section _ -> true + | 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 fname = @@ -68,10 +118,6 @@ let strip_trailing_blanks = let rex = Pcre.regexp "\\s*$" in fun s -> Pcre.replace ~rex s -let strip_trailing_slash = - let rex = Pcre.regexp "/$" in - fun s -> Pcre.replace ~rex s - let empty_mathml () = DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns) ~qualifiedName:(Gdome.domString "math") ~doctype:None @@ -221,7 +267,17 @@ 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$" -let obj_file_of_script f = Pcre.replace ~rex:end_ma_RE ~templ:".moo" f + +let obj_file_of_baseuri baseuri = + let path = + Helm_registry.get "matita.basedir" ^ "/xml" ^ + Pcre.replace ~pat:"^cic:" ~templ:"" baseuri + in + path ^ ".moo" + +let obj_file_of_script f = + let baseuri = baseuri_of_file f in + obj_file_of_baseuri baseuri let rec list_uniq = function | [] -> [] diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index eb6e451c7..86c11249a 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -23,6 +23,13 @@ * http://helm.cs.unibo.it/ *) +val baseuri_of_file : string -> string + +val baseuri_of_baseuri_decl : ('a, 'b, 'c) GrafiteAst.statement -> string option + + (** 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 @@ -98,6 +105,7 @@ val get_proof_aliases: MatitaTypes.status -> DisambiguateTypes.environment (** given the base name of an image, returns its full path *) 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 diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 86775f292..f339ebb40 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -149,8 +149,7 @@ let eval_with_engine guistuff status user_goal parsed_text st = with MatitaEngine.UnableToInclude what as exc -> let compile_needed_and_go_on d = - let root = MatitamakeLib.root_for_development d in - let target = root ^ "/" ^ what in + let target = what in let refresh_cb () = while Glib.Main.pending () do ignore(Glib.Main.iteration false); done in @@ -334,10 +333,10 @@ let eval_executable guistuff status user_goal parsed_text script ex = match ex with | TA.Command (loc, _) | TA.Tactical (loc, _) -> (try - (match ML.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with + (match MatitaMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with | None -> () | Some u -> - if not (ML.is_empty u) then + if not (MatitaMisc.is_empty u) then match guistuff.ask_confirmation ~title:"Baseuri redefinition" diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml index 89b602735..553823904 100644 --- a/helm/matita/matitaclean.ml +++ b/helm/matita/matitaclean.ml @@ -63,7 +63,7 @@ let _ = 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 ("File " ^ suri ^ " defines a bad baseuri: "^u); diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml index 51635a30a..d5e4c8dde 100644 --- a/helm/matita/matitacleanLib.ml +++ b/helm/matita/matitacleanLib.ml @@ -32,12 +32,6 @@ module HGM = Http_getter_misc;; module UM = UriManager;; module TA = GrafiteAst;; -let baseuri_of_baseuri_decl st = - match st with - | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) -> - Some buri - | _ -> None - let cache_of_processed_baseuri = Hashtbl.create 1024 let one_step_depend suri = @@ -128,43 +122,10 @@ let close_uri_list uri_to_remove = in uri_to_remove, depend -let baseuri_of_file file = - let uri = ref None in - let ic = open_in file in - let istream = Stream.of_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 = 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(HG.resolve u) - with - | HGT.Unresolvable_URI _ -> - MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri) - | HGT.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 (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 rec fix uris next = +let rec close uris next = match next with | [] -> uris - | l -> let uris, next = close_uri_list l in fix uris next @ uris + | l -> let uris, next = close_uri_list l in close uris next @ uris let cleaned_no = ref 0;; @@ -174,13 +135,17 @@ let clean_baseuris ?(verbose=true) buris = debug_prerr "clean_baseuris called on:"; if debug then List.iter debug_prerr buris; - let l = fix [] buris in + let l = close [] buris in let l = MatitaMisc.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 (MatitaSync.remove ~verbose) l; + Hashtbl.iter + (fun buri _ -> + MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri) + ) cache_of_processed_baseuri; cleaned_no := !cleaned_no + List.length l; if !cleaned_no > 30 then List.iter @@ -189,6 +154,3 @@ let clean_baseuris ?(verbose=true) buris = [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl (); MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl(); MetadataTypes.count_tbl()] - -let is_empty buri = HG.ls (HGM.strip_trailing_slash buri ^ "/") = [] - diff --git a/helm/matita/matitacleanLib.mli b/helm/matita/matitacleanLib.mli index a63a8edb0..f4ce6de57 100644 --- a/helm/matita/matitacleanLib.mli +++ b/helm/matita/matitacleanLib.mli @@ -24,10 +24,3 @@ *) val clean_baseuris : ?verbose:bool -> string list -> unit -val baseuri_of_file : string -> string - -val baseuri_of_baseuri_decl : ('a, 'b, 'c) GrafiteAst.statement -> string option - - (** check whether no objects are defined below a given baseuri *) -val is_empty: string -> bool - diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index 621b20ecf..88cac8280 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -39,7 +39,7 @@ module TA = GrafiteAst module U = UriManager let deps = Hashtbl.create (Array.length Sys.argv) -let baseuri = ref [] +let baseuris = ref [] let aliases = Hashtbl.create (Array.length Sys.argv) (* @@ -53,10 +53,8 @@ let buri alias = U.buri_of_uri (U.uri_of_string alias) let resolve alias = - try - Some (snd(List.find (fun (u, f) -> u = (buri alias)) !baseuri)) - with - | Not_found -> None + let buri = buri alias in + if List.exists (fun u -> u = buri) !baseuris then Some buri else None (*** TODO MANCANO LE URI VERBATIM DENTRO GLI AST DEI TERMINI ****) @@ -82,7 +80,8 @@ let main () = CicNotation.load_notation BuildTimeConf.core_notation_script; let files = ref [] in Arg.parse arg_spec (add_l files) usage; - List.iter (fun file -> + List.iter + (fun file -> let ic = open_in file in let istream = Stream.of_channel ic in (try @@ -91,12 +90,12 @@ let main () = match GrafiteParser.parse_statement istream with | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", uri))) -> let uri = MatitaMisc.strip_trailing_slash uri in - baseuri := (uri, file) :: !baseuri + baseuris := uri :: !baseuris | TA.Executable (_, TA.Command (_, TA.Alias (_, TA.Ident_alias(_, uri)))) -> Hashtbl.add aliases file uri | TA.Executable (_, TA.Command (_, TA.Include (_, path))) -> - Hashtbl.add deps file (find path) + Hashtbl.add deps file (MatitaMisc.obj_file_of_script (find path)) | _ -> () with CicNotationParser.Parse_error _ as exn -> @@ -111,22 +110,20 @@ let main () = let dep = resolve alias in match dep with | None -> () - | Some d -> Hashtbl.add deps file d) - aliases) - !files; - List.iter (fun file -> + | Some u -> Hashtbl.add deps file (MatitaMisc.obj_file_of_baseuri u)) + aliases + ) !files; + List.iter + (fun file -> let deps = Hashtbl.find_all deps file in let deps = List.fast_sort Pervasives.compare deps in let deps = MatitaMisc.list_uniq deps in - let deps = - List.map (fun x -> Pcre.replace ~pat:"ma$" ~templ:"moo" x) deps - in let deps = file :: deps in - Printf.printf "%s: %s\n" (MatitaMisc.obj_file_of_script file) - (String.concat " " deps)) - !files + let moo = MatitaMisc.obj_file_of_script file in + Printf.printf "%s: %s\n" moo (String.concat " " deps); + Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" file) moo + ) !files ;; let _ = main () - diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml index 8dc45faaa..d95bfdbad 100644 --- a/helm/matita/matitamakeLib.ml +++ b/helm/matita/matitamakeLib.ml @@ -125,12 +125,10 @@ let rebuild_makefile development = let rm = BuildTimeConf.runtime_base_dir ^ "/matitaclean" ^ am_i_opt () in let mm = BuildTimeConf.runtime_base_dir ^ "/matitadep" ^ am_i_opt () in let df = pool () ^ development.name ^ "/depend" in - let dfs = pool () ^ development.name ^ "/depend.short" in let template = Pcre.replace ~pat:"@ROOT@" ~templ:development.root template in let template = Pcre.replace ~pat:"@CC@" ~templ:cc template in 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:"@DEPFILESHORT@" ~templ:dfs template in let template = Pcre.replace ~pat:"@CLEAN@" ~templ:rm template in MatitaMisc.output_file template makefilepath @@ -215,6 +213,7 @@ let mk_maker refresh_cb = try let argv = Array.of_list ("make"::args) in pid := Unix.create_process "make" argv Unix.stdin out_w err_w; +let ch = open_out "/tmp/pippo" in output_string ch (String.concat " " ("make"::(Array.to_list argv)) ^ "\n"); flush ch; close_out ch; Unix.close out_w; Unix.close err_w; let buf = String.create 1024 in @@ -269,7 +268,6 @@ let destroy_development development = unlink (makefile_for_development development); unlink (pool () ^ development.name ^ rootfile); unlink (pool () ^ development.name ^ "/depend"); - unlink (pool () ^ development.name ^ "/depend.short"); rmdir (pool () ^ development.name); developments := List.filter (fun d -> d.name <> development.name) !developments diff --git a/helm/matita/template_makefile.in b/helm/matita/template_makefile.in index 1413aedd9..6f4dc6322 100644 --- a/helm/matita/template_makefile.in +++ b/helm/matita/template_makefile.in @@ -11,23 +11,12 @@ clean: $(MATITACLEAN) $(SRC) rm -f $(TODO) -%.moo:%.ma - [ ! -e $@ ] || ($(MATITACLEAN) $< 1>/dev/null 2>/dev/null ; rm -f $@) - ($(MATITAC) -preserve -q -I @ROOT@ $< | (grep -v "^make" || true)) || \ - ($(MATITACLEAN) $< ; exit 1) +%.moo: + ($(MATITAC) -q -I @ROOT@ $< | (grep -v "^make" || true)) -@DEPFILE@ @DEPFILESHORT@: $(SRC) +@DEPFILE@ : $(SRC) @DEP@ -I @ROOT@ $^ > @DEPFILE@ - >@DEPFILESHORT@ - for X in `cat @DEPFILE@ | cut -f 1 -d :`; do\ - TMP=`basename $$X | sed s/\.moo$$//`;\ - echo "$$TMP: $$X" >> @DEPFILESHORT@;\ - done # this is the depend for full targets like: # dir/dir/name.moo: dir/dir/name.ma dir/dep.moo -include @DEPFILE@ - -# this is for short name targets like: -# name: dir/dir/name.moo --include @DEPFILESHORT@ diff --git a/helm/matita/tests/Makefile b/helm/matita/tests/Makefile index 2665c1a1a..602611302 100644 --- a/helm/matita/tests/Makefile +++ b/helm/matita/tests/Makefile @@ -15,7 +15,7 @@ DEPEND_NAME=.depend H=@ -all: $(SRC:%.ma=%.moo) +all: $(SRC:%.ma=%.mo) opt: $(H)make MATITAC="$(MATITACOPT)" MATITACLEAN="$(MATITACLEANOPT)" MATITADEP="$(MATITADEPOPT)" all @@ -38,7 +38,7 @@ depend: make $(DEPEND_NAME) .PHONY: depend -%.moo:%.ma +%.moo: $(H)$(MATITAC) $< $(DEPEND_NAME): $(SRC) -- 2.39.2