From 0d681e06c6ced0be7f9dbce417684b082229745a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 30 Jun 2005 07:54:34 +0000 Subject: [PATCH] first matitadep snapshot --- helm/matita/Makefile.in | 12 +++++-- helm/matita/matitaDb.ml | 8 +---- helm/matita/matitaEngine.ml | 9 +++++- helm/matita/matitaMisc.ml | 14 +++++++++ helm/matita/matitaMisc.mli | 4 +++ helm/matita/matitacLib.ml | 1 + helm/matita/matitadep.ml | 63 +++++++++++++++++++++++++++++++++++++ 7 files changed, 100 insertions(+), 11 deletions(-) create mode 100644 helm/matita/matitadep.ml diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 57893de42..c7b250a3b 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -46,7 +46,7 @@ CCMOS = \ matitacLib.cmo -all: matita matitac matitatop cicbrowser +all: matita matitac matitatop cicbrowser matitadep updater: $(LIB_DEPS) $(OCAMLC) $(PKGS) -linkpkg -o $@ updater.ml @@ -56,7 +56,7 @@ CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS)) LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(REQUIRES)) LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(REQUIRES)) -opt: matita.opt matitac.opt cicbrowser.opt +opt: matita.opt matitac.opt cicbrowser.opt matitadep.opt else opt: @echo "Native code compilation is disabled" @@ -75,6 +75,11 @@ matitac.opt: $(LIBX_DEPS) $(CCMXS) matitac.ml matitatop: matitatop.ml $(LIB_DEPS) $(CCMOS) $(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $< +matitadep: matitadep.ml $(LIB_DEPS) $(CCMOS) + $(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) $< +matitadep.opt: matitadep.ml $(LIB_DEPS) $(CCMXS) + $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $< + cicbrowser: matita @test -f $@ || ln -s $< $@ cicbrowser.opt: matita.opt @@ -96,7 +101,8 @@ matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade clean: rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \ matita matita.opt matitac matitac.opt \ - cicbrowser cicbrowser.opt + cicbrowser cicbrowser.opt \ + matitadep matitadep.opt distclean: clean rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli rm -f config.log config.status Makefile buildTimeConf.ml diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml index d4f5d01b1..423fa2b5a 100644 --- a/helm/matita/matitaDb.ml +++ b/helm/matita/matitaDb.ml @@ -146,13 +146,7 @@ let remove_uri uri = let l = ref [] in Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l); let l = List.sort Pervasives.compare !l in - let rec uniq = function - | [] -> [] - | h::[] -> [h] - | h1::h2::tl when h1 = h2 -> uniq (h2 :: tl) - | h1::tl (* when h1 <> h2 *) -> h1 :: uniq tl - in - uniq l + MatitaMisc.list_uniq l with exn -> raise exn (* no errors should be accepted *) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index a28cdedf8..354b18ae5 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -224,7 +224,14 @@ let generate_projections uri fields status = let eval_command status cmd = match cmd with - | TacticAst.Set (loc, name, value) -> set_option status name value + | TacticAst.Set (loc, name, value) -> + let value = + if name = "baseuri" then + MatitaMisc.strip_trailing_slash value + else + value + in + set_option status name value | TacticAst.Drop loc -> raise Drop | TacticAst.Qed loc -> let uri, metasenv, bo, ty = diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 73fdd4c54..ab077d923 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -57,6 +57,10 @@ 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 @@ -194,3 +198,13 @@ 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 rec list_uniq = function + | [] -> [] + | h::[] -> [h] + | h1::h2::tl when h1 = h2 -> list_uniq (h2 :: tl) + | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl + +let end_ma_RE = Pcre.regexp "\\.ma$" diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index acbe3bac6..31efae031 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -39,6 +39,9 @@ val is_proof_object: string -> bool val append_phrase_sep: string -> string val strip_trailing_blanks: string -> string +val strip_trailing_slash: string -> string + +val list_uniq: 'a list -> 'a list (* uniq unix filter on lists *) (** @raise Failure *) val unopt: 'a option -> 'a @@ -89,4 +92,5 @@ 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_script: string -> string diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index d57d211e2..4d04d371c 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -141,6 +141,7 @@ let main ~mode = begin MatitaLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); + close_out (open_out (MatitaMisc.obj_file_of_script fname)); exit 0 end with diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml new file mode 100644 index 000000000..df6cff273 --- /dev/null +++ b/helm/matita/matitadep.ml @@ -0,0 +1,63 @@ +module TA = TacticAst +module U = UriManager + +let deps = Hashtbl.create (Array.length Sys.argv) +let baseuri = ref [] +let aliases = Hashtbl.create (Array.length Sys.argv) + +(* +let uri_of_alias = function + | Ident_alias (_, uri) + | Symbol_alias (_, _, uri) + | Number_alias (_, uri) -> uri +*) + +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 + + (*** TODO MANCANO LE URI VERBATIM DENTRO GLI AST DEI TERMINI ****) + +let main () = + for i = 1 to Array.length Sys.argv - 1 do + let file = Sys.argv.(i) in + let ic = open_in file in + let stms = CicTextualParser2.parse_statements (Stream.of_channel ic) in + close_in ic; + let stms = + List.iter + (function + | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", uri))) -> + let uri = MatitaMisc.strip_trailing_slash uri in + baseuri := (uri, file) :: !baseuri + | TA.Executable (_, TA.Command + (_, TA.Alias (_, TA.Ident_alias(_, uri)))) -> + Hashtbl.add aliases file uri + | _ -> ()) + stms + in + Hashtbl.iter + (fun file alias -> + let dep = resolve alias in + match dep with + | None -> () + | Some d -> Hashtbl.add deps file d) + aliases; + done; + for i = 1 to Array.length Sys.argv - 1 do + let file = Sys.argv.(i) in + 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 = file :: deps in + Printf.printf "%s: %s\n" (MatitaMisc.obj_file_of_script file) + (String.concat " " deps) + done + + +let _ = main () -- 2.39.2