From d8c17db3c787f3ea964bbcd3b27427ca44b356d0 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 5 Nov 2010 15:18:53 +0000 Subject: [PATCH] Huge change!!! - matitadep & co removed (RIP) - both matita and matitac can now recursively compile files as needed - librarian greatly simplified: now it only handles roots Probably many bugs left. --- .../grafite_engine/grafiteEngine.ml | 1 + .../components/grafite_engine/grafiteTypes.ml | 3 + .../grafite_engine/grafiteTypes.mli | 2 + matita/components/grafite_parser/Makefile | 5 +- .../grafite_parser/dependenciesParser.ml | 86 ----- .../grafite_parser/dependenciesParser.mli | 36 -- matita/components/library/librarian.ml | 261 +------------ matita/components/library/librarian.mli | 43 --- matita/components/ng_library/nCicLibrary.ml | 34 +- matita/components/ng_library/nCicLibrary.mli | 10 +- matita/components/statuses.txt | 2 +- matita/matita/Makefile | 22 +- matita/matita/matitaEngine.ml | 351 +++++++----------- matita/matita/matitaEngine.mli | 16 +- matita/matita/matitaExcPp.ml | 9 +- matita/matita/matitaGui.ml | 2 +- matita/matita/matitaScript.ml | 3 +- matita/matita/matitac.ml | 5 +- matita/matita/matitadep.ml | 251 ------------- matita/matita/matitadep.mli | 27 -- 20 files changed, 204 insertions(+), 965 deletions(-) delete mode 100644 matita/components/grafite_parser/dependenciesParser.ml delete mode 100644 matita/components/grafite_parser/dependenciesParser.mli delete mode 100644 matita/matita/matitadep.ml delete mode 100644 matita/matita/matitadep.mli diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index 855b1f708..0e5f7b529 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -406,6 +406,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = GrafiteTypes.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) status in let status = status#set_dump (obj::status#dump) in + let status = status#set_dependencies (fname::status#dependencies) in (*assert false;*) (* MATITA 1.0mode must be passed to GrafiteTypes.Serializer.require somehow *) status diff --git a/matita/components/grafite_engine/grafiteTypes.ml b/matita/components/grafite_engine/grafiteTypes.ml index 0e1b87fa1..fe27a9656 100644 --- a/matita/components/grafite_engine/grafiteTypes.ml +++ b/matita/components/grafite_engine/grafiteTypes.ml @@ -45,10 +45,13 @@ class status = fun (b : string) -> inherit TermContentPres.status val baseuri = b val ng_mode = (`CommandMode : [`CommandMode | `ProofMode]) + val dependencies = ([] : string list) method baseuri = baseuri method set_baseuri v = {< baseuri = v >} method ng_mode = ng_mode; method set_ng_mode v = {< ng_mode = v >} + method dependencies = dependencies + method set_dependencies v = {< dependencies = v >} end module Serializer = diff --git a/matita/components/grafite_engine/grafiteTypes.mli b/matita/components/grafite_engine/grafiteTypes.mli index 4e226f703..090b81fc1 100644 --- a/matita/components/grafite_engine/grafiteTypes.mli +++ b/matita/components/grafite_engine/grafiteTypes.mli @@ -40,6 +40,8 @@ class status : inherit NCicLibrary.status inherit GrafiteParser.status inherit TermContentPres.status + method dependencies: string list + method set_dependencies: string list -> 'self method baseuri: string method set_baseuri: string -> 'self method ng_mode: [`ProofMode | `CommandMode] diff --git a/matita/components/grafite_parser/Makefile b/matita/components/grafite_parser/Makefile index 1005a0019..164153916 100644 --- a/matita/components/grafite_parser/Makefile +++ b/matita/components/grafite_parser/Makefile @@ -1,10 +1,9 @@ PACKAGE = grafite_parser PREDICATES = -INTERFACE_FILES = \ - dependenciesParser.mli \ +INTERFACE_FILES = \ grafiteParser.mli \ - print_grammar.mli \ + print_grammar.mli \ $(NULL) IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/matita/components/grafite_parser/dependenciesParser.ml b/matita/components/grafite_parser/dependenciesParser.ml deleted file mode 100644 index 16c2a2c69..000000000 --- a/matita/components/grafite_parser/dependenciesParser.ml +++ /dev/null @@ -1,86 +0,0 @@ -(* 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/ - *) - -(* $Id$ *) - -exception UnableToInclude of string - - (* statements meaningful for matitadep *) -type dependency = - | IncludeDep of string - | UriDep of NUri.uri - | InlineDep of string - -let pp_dependency = function - | IncludeDep str -> "include \"" ^ str ^ "\"" - | UriDep uri -> "uri \"" ^ NUri.string_of_uri uri ^ "\"" - | InlineDep str -> "inline \"" ^ str ^ "\"" - -let parse_dependencies lexbuf = - let tok_stream,_ = - let lexers = (CicNotationLexer.mk_lexers []) in - lexers.CicNotationLexer.level2_ast_lexer.Token.tok_func (Obj.magic lexbuf) - in - let rec parse acc = - let continue, acc = - try - (parser - | [< '("QSTRING", s) >] -> - (* because of alias id qstring = qstring :-( *) - (try - if String.sub s 0 5 <> "cic:/" then true,acc - else - true, (UriDep (NUri.uri_of_string s) :: acc) - with Invalid_argument _ -> true,acc) - | [< '("URI", u) >] -> - true, (UriDep (NUri.uri_of_string u) :: acc) - | [< '("IDENT", "include"); '("QSTRING", fname) >] -> - true, (IncludeDep fname :: acc) - | [< '("IDENT", "include"); '("IDENT", "source"); '("QSTRING", fname) >] -> - true, (IncludeDep fname :: acc) - | [< '("IDENT", "include'"); '("QSTRING", fname) >] -> - true, (IncludeDep fname :: acc) - | [< '("IDENT", "inline"); '("QSTRING", fname) >] -> - true, (InlineDep fname :: acc) - | [< '("EOI", _) >] -> false, acc - | [< 'tok >] -> true, acc - | [< >] -> false, acc) tok_stream - with - Stream.Error _ -> false, acc - | CicNotationLexer.Error _ -> true, acc - in - if continue then parse acc else acc - in - List.rev (parse []) - -let deps_of_file ma_file = - try - let ic = open_in ma_file in - let istream = Ulexing.from_utf8_channel ic in - let dependencies = parse_dependencies istream in - close_in ic; - dependencies - with End_of_file -> [] -;; diff --git a/matita/components/grafite_parser/dependenciesParser.mli b/matita/components/grafite_parser/dependenciesParser.mli deleted file mode 100644 index cbdc028dd..000000000 --- a/matita/components/grafite_parser/dependenciesParser.mli +++ /dev/null @@ -1,36 +0,0 @@ -(* 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 UnableToInclude of string - - (* statements meaningful for matitadep *) -type dependency = - | IncludeDep of string - | UriDep of NUri.uri - | InlineDep of string - -val pp_dependency: dependency -> string - -val deps_of_file: string -> dependency list diff --git a/matita/components/library/librarian.ml b/matita/components/library/librarian.ml index 2c2ba6ff2..7d159af24 100644 --- a/matita/components/library/librarian.ml +++ b/matita/components/library/librarian.ml @@ -23,19 +23,6 @@ * http://helm.cs.unibo.it/ *) -let debug = ref 0 - -let time_stamp = - let old = ref 0.0 in - fun msg -> - if !debug > 0 then begin - let times = Unix.times () in - let stamp = times.Unix.tms_utime +. times.Unix.tms_stime in - let lap = stamp -. !old in - Printf.eprintf "TIME STAMP (%s): %f\n" msg lap; flush stderr; - old := stamp - end - exception NoRootFor of string let absolutize path = @@ -166,253 +153,7 @@ let find_roots_in_dir dir = dir ;; -(* make *) -let load_deps_file f = - let deps = ref [] in - let ic = open_in f in - try - while true do - begin - let l = input_line ic in - match Str.split (Str.regexp " ") l with - | [] -> - HLog.error ("Malformed deps file: " ^ f); - raise (Failure ("Malformed deps file: " ^ f)) - | he::tl -> deps := (he,tl) :: !deps - end - done; !deps - with End_of_file -> !deps -;; - -type options = (string * string) list - -module type Format = - sig - type source_object - type target_object - val load_deps_file: string -> (source_object * source_object list) list - val string_of_source_object: source_object -> string - val string_of_target_object: target_object -> string - val build: options -> source_object -> bool - val root_and_target_of: - options -> source_object -> - (* root, relative source, writeable target, read only target *) - string option * source_object * target_object * target_object - val mtime_of_source_object: source_object -> float option - val mtime_of_target_object: target_object -> float option - val is_readonly_buri_of: options -> source_object -> bool - end - -module Make = functor (F:Format) -> struct - - type status = Done of bool - | Ready of bool - - let say s = if !debug > 0 then prerr_endline ("make: "^s);; - - let unopt_or_call x f y = match x with Some _ -> x | None -> f y;; - - let fst4 = function (x,_,_,_) -> x;; - - let modified_before_s_t (_,cs, ct, _, _) a b = - - if !debug > 1 then time_stamp ("L s_t: a " ^ F.string_of_source_object a); - if !debug > 1 then time_stamp ("L s_t: b " ^ F.string_of_target_object b); - - let a = try Hashtbl.find cs a with Not_found -> assert false in - let b = - try - match Hashtbl.find ct b with - | Some _ as x -> x - | None -> - match F.mtime_of_target_object b with - | Some t as x -> - Hashtbl.remove ct b; - Hashtbl.add ct b x; x - | x -> x - with Not_found -> assert false - in - let r = match a, b with - | Some a, Some b -> a <= b - | _ -> false - in - - if !debug > 1 then time_stamp ("L s_t: " ^ string_of_bool r); - - r - - let modified_before_t_t (_,_,ct, _, _) a b = - - if !debug > 1 then time_stamp ("L t_t: a " ^ F.string_of_target_object a); - if !debug > 1 then time_stamp ("L t_t: b " ^ F.string_of_target_object b); - - let a = - try - match Hashtbl.find ct a with - | Some _ as x -> x - | None -> - match F.mtime_of_target_object a with - | Some t as x -> - Hashtbl.remove ct a; - Hashtbl.add ct a x; x - | x -> x - with Not_found -> assert false - in - let b = - try - match Hashtbl.find ct b with - | Some _ as x -> x - | None -> - match F.mtime_of_target_object b with - | Some t as x -> - Hashtbl.remove ct b; - Hashtbl.add ct b x; x - | x -> x - with Not_found -> assert false - in - let r = match a, b with - | Some a, Some b -> - - if !debug > 1 then time_stamp ("tt: a " ^ string_of_float a); - if !debug > 1 then time_stamp ("tt: b " ^ string_of_float b); - - a <= b - | _ -> false - in - - if !debug > 1 then time_stamp ("L t_t: " ^ string_of_bool r); - - r - - let rec purge_unwanted_roots wanted deps = - let roots, rest = - List.partition - (fun (t,_,d,_,_) -> - not (List.exists (fun (_,_,d1,_,_) -> List.mem t d1) deps)) - deps - in - let newroots = List.filter (fun (t,_,_,_,_) -> List.mem t wanted) roots in - if newroots = roots then - deps - else - purge_unwanted_roots wanted (newroots @ rest) - ;; - - let is_not_ro (opts,_,_,_,_) (f,_,_,r,_) = - match r with - | Some root -> not (F.is_readonly_buri_of opts f) - | None -> assert false - ;; - -(* FG: new sorting algorithm ************************************************) - - let rec make_aux root opts ok deps = - List.fold_left (make_one root opts) ok deps - - and make_one root opts ok what = - let lo, _, ct, cc, cd = opts in - let t, path, deps, froot, tgt = what in - let str = F.string_of_source_object t in - let map (okd, okt) d = - let (_, _, _, _, tgtd) as whatd = (Hashtbl.find cd d) in - let r = make_one root opts okd whatd in - r, okt && modified_before_t_t opts tgtd tgt - in - time_stamp ("L : processing " ^ str); - try - let r = Hashtbl.find cc t in - time_stamp ("L : " ^ string_of_bool r ^ " " ^ str); - ok && r -(* say "already built" *) - with Not_found -> - let okd, okt = List.fold_left map (true, modified_before_s_t opts t tgt) deps in - let res = - if okd then - if okt then true else - let build path = match froot with - | Some froot when froot = root -> - if is_not_ro opts what then F.build lo path else - (HLog.error ("Read only baseuri for: " ^ str ^ - ", I won't compile it even if it is out of date"); - false) - | Some froot -> make froot [path] - | None -> HLog.error ("No root for: " ^ str); false - in - Hashtbl.remove ct tgt; - Hashtbl.add ct tgt None; - time_stamp ("L : BUILDING " ^ str); - let res = build path in - time_stamp ("L : DONE " ^ str); res - else false - in - time_stamp ("L : " ^ string_of_bool res ^ " " ^ str); - Hashtbl.add cc t res; ok && res - -(****************************************************************************) - - and make root targets = - time_stamp "L : ENTERING"; - HLog.debug ("Entering directory '"^root^"'"); - let old_root = Sys.getcwd () in - Sys.chdir root; - let deps = F.load_deps_file (root^"/depends") in - let local_options = load_root_file (root^"/root") in - let baseuri = List.assoc "baseuri" local_options in - print_endline ("Entering HELM directory: " ^ baseuri); flush stdout; - let caches,cachet,cachec,cached = - Hashtbl.create 73, Hashtbl.create 73, Hashtbl.create 73, Hashtbl.create 73 - in - (* deps are enriched with these informations to sped up things later *) - let deps = - List.map - (fun (file,d) -> - let r,path,wtgt,rotgt = F.root_and_target_of local_options file in - Hashtbl.add caches file (F.mtime_of_source_object file); - (* if a read only target exists, we use that one, otherwise - we use the writeable one that may be compiled *) - let _,_,_,_, tgt as tuple = - match F.mtime_of_target_object rotgt with - | Some _ as mtime -> - Hashtbl.add cachet rotgt mtime; - (file, path, d, r, rotgt) - | None -> - Hashtbl.add cachet wtgt (F.mtime_of_target_object wtgt); - (file, path, d, r, wtgt) - in - Hashtbl.add cached file tuple; - tuple - ) - deps - in - let opts = local_options, caches, cachet, cachec, cached in - let ok = - if targets = [] then - make_aux root opts true deps - else - make_aux root opts true (purge_unwanted_roots targets deps) - in - print_endline ("Leaving HELM directory: " ^ baseuri); flush stdout; - HLog.debug ("Leaving directory '"^root^"'"); - Sys.chdir old_root; - time_stamp "L : LEAVING"; - ok - ;; - -end - -let write_deps_file where deps = match where with - | Some root -> - let oc = open_out (root ^ "/depends") in - let map (t, d) = output_string oc (t^" "^String.concat " " d^"\n") in - List.iter map deps; close_out oc; - HLog.message ("Generated: " ^ root ^ "/depends") - | None -> - print_endline (String.concat " " (List.flatten (List.map snd deps))) - -(* FG ***********************************************************************) - (* scheme uri part as defined in URI Generic Syntax (RFC 3986) *) let uri_scheme_rex = Pcre.regexp "^[[:alpha:]][[:alnum:]\-+.]*:" -let is_uri str = - Pcre.pmatch ~rex:uri_scheme_rex str +let is_uri str = Pcre.pmatch ~rex:uri_scheme_rex str diff --git a/matita/components/library/librarian.mli b/matita/components/library/librarian.mli index 4eed9051d..040cecf62 100644 --- a/matita/components/library/librarian.mli +++ b/matita/components/library/librarian.mli @@ -58,48 +58,5 @@ val mk_baseuri: string -> string -> string *) val find_roots_in_dir: string -> string list -(* make implementation *) -type options = (string * string) list - -module type Format = - sig - type source_object - type target_object - val load_deps_file: string -> (source_object * source_object list) list - val string_of_source_object: source_object -> string - val string_of_target_object: target_object -> string - val build: options -> source_object -> bool - val root_and_target_of: - options -> source_object -> - (* root, relative source, writeable target, read only target *) - string option * source_object * target_object * target_object - val mtime_of_source_object: source_object -> float option - val mtime_of_target_object: target_object -> float option - val is_readonly_buri_of: options -> source_object -> bool - end - -module Make : - functor (F : Format) -> - sig - (* make [root dir] [targets], targets = [] means make all *) - val make : string -> F.source_object list -> bool - end - -(* deps are made with scripts names, for example lines like - * - * nat/plus.ma nat/nat.ma logic/equality.ma - * - * state that plus.ma needs nat and equality - *) -val load_deps_file: string -> (string * string list) list -val write_deps_file: string option -> (string * string list) list -> unit - -(* FG ***********************************************************************) - (* true if the argunent starts with a uri scheme prefix *) val is_uri: string -> bool - -(* Valid values: 0: no debug; 1: normal debug; > 1: extra debug *) -val debug: int ref - -val time_stamp: string -> unit diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml index ad8084692..ae6666be5 100644 --- a/matita/components/ng_library/nCicLibrary.ml +++ b/matita/components/ng_library/nCicLibrary.ml @@ -48,7 +48,7 @@ let refresh_uri_in_obj (uri,height,metasenv,subst,obj_kind) = NCicUntrusted.map_obj_kind refresh_uri_in_term obj_kind ;; -let path_of_baseuri ?(no_suffix=false) baseuri = +let ng_path_of_baseuri ?(no_suffix=false) baseuri = let uri = NUri.string_of_uri baseuri in let path = String.sub uri 4 (String.length uri - 4) in let path = Helm_registry.get "matita.basedir" ^ path in @@ -70,13 +70,10 @@ let require_path path = dump ;; -let require0 ~baseuri = - require_path (path_of_baseuri baseuri) -;; +let require0 ~baseuri = require_path (ng_path_of_baseuri baseuri) let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";; - type timestamp = [ `Obj of NUri.uri * NCic.obj | `Constr of NCic.universe * NCic.universe] list * @@ -91,6 +88,8 @@ let local_aliases = ref [];; let cache = ref NUri.UriMap.empty;; let includes = ref [];; +let get_already_included () = !includes;; + let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps= let global_aliases = ref [] in let rev_includes_map = ref NUri.UriMap.empty in @@ -149,7 +148,7 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps= let init = load_db;; class status = - object(self) + object val timestamp = (time0 : timestamp) method timestamp = timestamp method set_timestamp v = {< timestamp = v >} @@ -164,14 +163,14 @@ let time_travel status = storage := sto; local_aliases := ali; cache := cac; includes := inc ;; -let serialize ~baseuri dump = - let ch = open_out (path_of_baseuri baseuri) in - Marshal.to_channel ch (magic,dump) []; +let serialize ~baseuri ~dependencies dump = + let ch = open_out (ng_path_of_baseuri baseuri) in + Marshal.to_channel ch (magic,(dependencies,dump)) []; close_out ch; List.iter (function | `Obj (uri,obj) -> - let ch = open_out (path_of_baseuri uri) in + let ch = open_out (ng_path_of_baseuri uri) in Marshal.to_channel ch (magic,obj) []; close_out ch | `Constr _ -> () @@ -184,7 +183,7 @@ let serialize ~baseuri dump = type obj = string * Obj.t class dumpable_status = - object(self) + object val dump = ([] : obj list) method dump = dump method set_dump v = {< dump = v >} @@ -202,9 +201,10 @@ module type SerializerType = dumpable_status -> dumpable_status val register: < run: 'a. string -> 'a register_type -> ('a -> obj) > - val serialize: baseuri:NUri.uri -> obj list -> unit + val serialize: baseuri:NUri.uri -> dependencies:string list -> obj list -> unit (* the obj is the "include" command to be added to the dump list *) val require: baseuri:NUri.uri -> dumpable_status -> dumpable_status * obj + val dependencies_of: baseuri:NUri.uri -> string list end module Serializer(D: sig type dumpable_status end) = @@ -242,11 +242,13 @@ module Serializer(D: sig type dumpable_status end) = let require2 ~baseuri status = try includes := baseuri::!includes; - let dump = require0 ~baseuri in + let _dependencies,dump = require0 ~baseuri in List.fold_right !require1 dump status with Sys_error _ -> - raise (IncludedFileNotCompiled(path_of_baseuri baseuri,NUri.string_of_uri baseuri)) + raise (IncludedFileNotCompiled(ng_path_of_baseuri baseuri,NUri.string_of_uri baseuri)) + + let dependencies_of ~baseuri = fst (require0 ~baseuri) let record_include = let aux baseuri ~refresh_uri_in_universe ~refresh_uri_in_term @@ -266,8 +268,8 @@ let decompile ~baseuri = let baseuris = get_deps baseuri in List.iter (fun baseuri -> remove_deps baseuri; - HExtlib.safe_remove (path_of_baseuri baseuri); - let basepath = path_of_baseuri ~no_suffix:true baseuri in + HExtlib.safe_remove (ng_path_of_baseuri baseuri); + let basepath = ng_path_of_baseuri ~no_suffix:true baseuri in try let od = Unix.opendir basepath in let rec aux names = diff --git a/matita/components/ng_library/nCicLibrary.mli b/matita/components/ng_library/nCicLibrary.mli index 9f641d1ca..4e080e8c2 100644 --- a/matita/components/ng_library/nCicLibrary.mli +++ b/matita/components/ng_library/nCicLibrary.mli @@ -52,9 +52,11 @@ module type SerializerType = dumpable_status -> dumpable_status val register: < run: 'a. string -> 'a register_type -> ('a -> obj) > - val serialize: baseuri:NUri.uri -> obj list -> unit + val serialize: baseuri:NUri.uri -> dependencies:string list -> obj list -> + unit (* the obj is the "include" command to be added to the dump list *) val require: baseuri:NUri.uri -> dumpable_status -> dumpable_status * obj + val dependencies_of: baseuri:NUri.uri -> string list end module Serializer(D: sig type dumpable_status end) : @@ -66,7 +68,11 @@ class dumpable_status : method set_dump: obj list -> 'self end -(* CSC: only required during old-to-NG phase, to be deleted *) val refresh_uri: NUri.uri -> NUri.uri +val ng_path_of_baseuri: ?no_suffix:bool -> NUri.uri -> string + +(* IMPERATIVE STUFF, TO BE PUT IN THE STATUS *) +val get_already_included: unit -> NUri.uri list + (* EOF *) diff --git a/matita/components/statuses.txt b/matita/components/statuses.txt index e6276014b..5e52989f1 100644 --- a/matita/components/statuses.txt +++ b/matita/components/statuses.txt @@ -1,4 +1,4 @@ -grafitetypes(baseuri,ng_mode) +grafitetypes(baseuri,ng_mode,dependencies) |--> dumpable(dump) |--> nciclibrary(timestamp) |--> grafiteparser(db=ast_statement grammarentry) diff --git a/matita/matita/Makefile b/matita/matita/Makefile index 6dd65b616..b269bd04a 100644 --- a/matita/matita/Makefile +++ b/matita/matita/Makefile @@ -25,7 +25,7 @@ OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) $(OCAMLOPT_DEBUG_FLAGS) OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAMLDEP_FLAGS) INSTALL_PROGRAMS= matita matitac INSTALL_PROGRAMS_LINKS_MATITA= -INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitaclean +INSTALL_PROGRAMS_LINKS_MATITAC= matitaclean MATITA_FLAGS = -noprofile NODB=false @@ -38,8 +38,8 @@ MLI = \ matitaTypes.mli \ matitaMisc.mli \ applyTransformation.mli \ - matitaExcPp.mli \ matitaEngine.mli \ + matitaExcPp.mli \ matitaInit.mli \ matitaGtkMisc.mli \ virtuals.mli \ @@ -52,12 +52,11 @@ CMLI = \ matitaTypes.mli \ matitaMisc.mli \ applyTransformation.mli \ - matitaExcPp.mli \ matitaEngine.mli \ + matitaExcPp.mli \ matitaInit.mli \ $(NULL) MAINCMLI = \ - matitadep.mli \ matitaclean.mli \ $(NULL) # objects for matita (GTK GUI) @@ -67,7 +66,7 @@ CML = buildTimeConf.ml $(CMLI:%.mli=%.ml) MAINCML = $(MAINCMLI:%.mli=%.ml) PROGRAMS_BYTE = \ - matita matitac matitadep matitaclean + matita matitac matitaclean PROGRAMS = $(PROGRAMS_BYTE) PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE)) NOINST_PROGRAMS = @@ -137,11 +136,6 @@ rottener.opt: rottener.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) clean-rottened: find . -type f -name "*.ma.*.rottened" -exec rm {} \; -matitadep: matitac - $(H)test -f $@ || ln -s $< $@ -matitadep.opt: matitac.opt - $(H)test -f $@ || ln -s $< $@ - matitaclean: matitac $(H)test -f $@ || ln -s $< $@ matitaclean.opt: matitac.opt @@ -195,9 +189,9 @@ tests.opt: $(foreach d,$(TEST_DIRS_OPT),$(d)-test-opt) cleantests: $(foreach d,$(TEST_DIRS),$(d)-cleantests) cleantests.opt: $(foreach d,$(TEST_DIRS_OPT),$(d)-cleantests-opt) -%-test: matitac matitadep matitaclean +%-test: matitac matitaclean -cd $* && make -k clean all -%-test-opt: matitac.opt matitadep.opt matitaclean.opt +%-test-opt: matitac.opt matitaclean.opt -cd $* && make -k clean.opt opt %-cleantests: matitaclean -cd $* && make clean @@ -210,8 +204,6 @@ ifeq ($(DISTRIBUTED),yes) dist_library: install_preliminaries - $(H)echo "depend" - $(H)cd $(WHERE)/ma/standard-library;(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitadep) $(H)echo "publish" $(H)cd $(WHERE)/ma/standard-library;(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitac -system -noinnertypes) $(H)echo "destroy" @@ -326,8 +318,6 @@ matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \ $(STATIC_EXTRA_CLIBS) strip $@ -matitadep.opt.static: matitac.opt.static - $(H)test -f $@ || ln -s $< $@ matitaclean.opt.static: matitac.opt.static $(H)test -f $@ || ln -s $< $@ diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index 3e13a386a..b04a06672 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -26,10 +26,93 @@ (* $Id$ *) module G = GrafiteAst +open GrafiteTypes +open Printf + +exception TryingToAdd of string Lazy.t +exception EnrichedWithStatus of exn * GrafiteTypes.status +exception AlreadyLoaded of string Lazy.t +exception FailureCompiling of string * exn let debug = false ;; let debug_print = if debug then prerr_endline else ignore ;; +let slash_n_RE = Pcre.regexp "\\n" ;; + +let pp_ast_statement grafite_status stm = + let stm = GrafiteAstPp.pp_statement stm + ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") + in + let stm = Pcre.replace ~rex:slash_n_RE stm in + let stm = + if String.length stm > 50 then String.sub stm 0 50 ^ " ..." + else stm + in + HLog.debug ("Executing: ``" ^ stm ^ "''") +;; + +let clean_exit baseuri exn = + LibraryClean.clean_baseuris ~verbose:false [baseuri]; + raise (FailureCompiling (baseuri,exn)) +;; + +let pp_times fname rc big_bang big_bang_u big_bang_s = + if not (Helm_registry.get_bool "matita.verbose") then + let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in + let r = Unix.gettimeofday () -. big_bang in + let u = u -. big_bang_u in + let s = s -. big_bang_s in + let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in + let rc,rcascii = + if rc then "OK","Ok" else "FAIL","Fail" in + let times = + let fmt t = + let seconds = int_of_float t in + let cents = int_of_float ((t -. floor t) *. 100.0) in + let minutes = seconds / 60 in + let seconds = seconds mod 60 in + Printf.sprintf "%dm%02d.%02ds" minutes seconds cents + in + Printf.sprintf "%s %s %s" (fmt r) (fmt u) (fmt s) + in + let s = Printf.sprintf "%-4s %s %s" rc times extra in + print_endline s; + flush stdout; + HLog.message ("Compilation of "^Filename.basename fname^": "^rc) +;; + +let cut prefix s = + let lenp = String.length prefix in + let lens = String.length s in + assert (lens > lenp); + assert (String.sub s 0 lenp = prefix); + String.sub s lenp (lens-lenp) +;; + +(*MATITA 1.0 assert false;; (* chiamare enrich_include_paths *)*) +let enrich_include_paths ~include_paths = + include_paths @ Helm_registry.get_list Helm_registry.string "matita.includes" +;; + +let activate_extraction baseuri fname = + () + (* MATITA 1.0 + if Helm_registry.get_bool "matita.extract" then + let mangled_baseuri = + let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in + let baseuri = Pcre.replace ~pat:"/" ~templ:"_" baseuri in + String.uncapitalize baseuri in + let f = + open_out + (Filename.dirname fname ^ "/" ^ mangled_baseuri ^ ".ml") in + LibrarySync.add_object_declaration_hook + (fun ~add_obj ~add_coercion _ obj -> + output_string f (CicExportation.ppobj baseuri obj); + flush f; []); + *) +;; + + let eval_macro_screenshot (status : GrafiteTypes.status) name = assert false (* MATITA 1.0 let _,_,metasenv,subst,_ = status#obj in @@ -83,16 +166,29 @@ let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) = (new_status,None)::intermediate_states ;; -exception TryingToAdd of string -exception EnrichedWithStatus of exn * GrafiteTypes.status +let rec get_ast status ~include_paths strm = + match GrafiteParser.parse_statement status strm with + (GrafiteAst.Executable + (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd + -> + let root, buri, _, tgt = + try Librarian.baseuri_of_script ~include_paths mafilename + with Librarian.NoRootFor _ -> + HLog.error ("The included file '"^mafilename^"' has no root file,"); + HLog.error "please create it."; + raise (Failure ("No root file for "^mafilename)) + in + ignore (assert_ng ~include_paths ~root tgt); + cmd + | cmd -> cmd -let eval_from_stream ~include_paths ?do_heavy_checks status str cb = +and eval_from_stream ~include_paths ?do_heavy_checks status str cb = let matita_debug = Helm_registry.get_bool "matita.debug" in let rec loop status = let stop,status = try let cont = - try Some (GrafiteParser.parse_statement status str) + try Some (get_ast status ~include_paths str) with End_of_file -> None in match cont with | None -> true, status @@ -104,7 +200,7 @@ let eval_from_stream ~include_paths ?do_heavy_checks status str cb = match new_statuses with [s,None] -> s | _::(_,Some (_,value))::_ -> - raise (TryingToAdd (GrafiteAstPp.pp_alias value)) + raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value))) | _ -> assert false in false, status @@ -114,101 +210,14 @@ let eval_from_stream ~include_paths ?do_heavy_checks status str cb = if stop then status else loop status in loop status -;; - -(* EX MATITACLIB *) -open Printf - -open GrafiteTypes - -let slash_n_RE = Pcre.regexp "\\n" ;; -let pp_ast_statement grafite_status stm = - let stm = GrafiteAstPp.pp_statement stm - ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") - in - let stm = Pcre.replace ~rex:slash_n_RE stm in - let stm = - if String.length stm > 50 then String.sub stm 0 50 ^ " ..." - else stm - in - HLog.debug ("Executing: ``" ^ stm ^ "''") -;; - -let clean_exit baseuri rc = - LibraryClean.clean_baseuris ~verbose:false [baseuri]; rc -;; - -let pp_times fname rc big_bang big_bang_u big_bang_s = - if not (Helm_registry.get_bool "matita.verbose") then - let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in - let r = Unix.gettimeofday () -. big_bang in - let u = u -. big_bang_u in - let s = s -. big_bang_s in - let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in - let rc,rcascii = - if rc then "OK","Ok" else "FAIL","Fail" in - let times = - let fmt t = - let seconds = int_of_float t in - let cents = int_of_float ((t -. floor t) *. 100.0) in - let minutes = seconds / 60 in - let seconds = seconds mod 60 in - Printf.sprintf "%dm%02d.%02ds" minutes seconds cents - in - Printf.sprintf "%s %s %s" (fmt r) (fmt u) (fmt s) - in - let s = Printf.sprintf "%-4s %s %s" rc times extra in - print_endline s; - flush stdout; - HLog.message ("Compilation of "^Filename.basename fname^": "^rc) -;; - -let cut prefix s = - let lenp = String.length prefix in - let lens = String.length s in - assert (lens > lenp); - assert (String.sub s 0 lenp = prefix); - String.sub s lenp (lens-lenp) -;; - -let get_include_paths options = - let include_paths = - try List.assoc "include_paths" options with Not_found -> "" - in - let include_paths = Str.split (Str.regexp " ") include_paths in - let include_paths = - include_paths @ - Helm_registry.get_list Helm_registry.string "matita.includes" - in - include_paths -;; - -let activate_extraction baseuri fname = - () - (* MATITA 1.0 - if Helm_registry.get_bool "matita.extract" then - let mangled_baseuri = - let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in - let baseuri = Pcre.replace ~pat:"/" ~templ:"_" baseuri in - String.uncapitalize baseuri in - let f = - open_out - (Filename.dirname fname ^ "/" ^ mangled_baseuri ^ ".ml") in - LibrarySync.add_object_declaration_hook - (fun ~add_obj ~add_coercion _ obj -> - output_string f (CicExportation.ppobj baseuri obj); - flush f; []); - *) -;; - -let compile options fname = +and compile ~include_paths fname = let matita_debug = Helm_registry.get_bool "matita.debug" in - let include_paths = get_include_paths options in let root,baseuri,fname,_tgt = Librarian.baseuri_of_script ~include_paths fname in if Http_getter_storage.is_read_only baseuri then assert false; activate_extraction baseuri fname ; + (* MATITA 1.0: debbo fare time_travel sulla ng_library? *) let grafite_status = new GrafiteTypes.status baseuri in let big_bang = Unix.gettimeofday () in let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = @@ -248,12 +257,11 @@ let compile options fname = else pp_ast_statement in let grafite_status = - eval_from_stream ~include_paths grafite_status buf print_cb - in + eval_from_stream ~include_paths grafite_status buf print_cb in let elapsed = Unix.time () -. time in (if Helm_registry.get_bool "matita.moo" then begin GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) - grafite_status#dump + ~dependencies:grafite_status#dependencies grafite_status#dump end; let tm = Unix.gmtime elapsed in let sec = string_of_int tm.Unix.tm_sec ^ "''" in @@ -265,121 +273,48 @@ let compile options fname = in HLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); - pp_times fname true big_bang big_bang_u big_bang_s; -(* + pp_times fname true big_bang big_bang_u big_bang_s +(* MATITA 1.0: debbo fare time_travel sulla ng_library? LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status; -*) - true) +*)) with (* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *) - | EnrichedWithStatus (exn, _grafite) as exn' -> - (match exn with - | Sys.Break -> HLog.error "user break!" - | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> - let (x, y) = HExtlib.loc_of_floc floc in - HLog.error (sprintf "Parse error at %d-%d: %s" x y err) - | exn when matita_debug -> raise exn' - | exn -> HLog.error (snd (MatitaExcPp.to_string exn)) - ); -(* LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status; + | exn when not matita_debug -> +(* MATITA 1.0: debbo fare time_travel sulla ng_library? + LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status; * *) pp_times fname false big_bang big_bang_u big_bang_s; - clean_exit baseuri false - | Sys.Break when not matita_debug -> - HLog.error "user break!"; - pp_times fname false big_bang big_bang_u big_bang_s; - clean_exit baseuri false - | exn when not matita_debug -> - HLog.error - ("Unwrapped exception, please fix: "^ snd (MatitaExcPp.to_string exn)); - pp_times fname false big_bang big_bang_u big_bang_s; - clean_exit baseuri false - -module F = - struct - type source_object = string - type target_object = string - let string_of_source_object s = s;; - let string_of_target_object s = s;; - - let is_readonly_buri_of opts file = - let buri = List.assoc "baseuri" opts in - Http_getter_storage.is_read_only (Librarian.mk_baseuri buri file) - ;; - - let root_and_target_of opts mafile = - try - let include_paths = get_include_paths opts in - let root,baseuri,_,relpath = - Librarian.baseuri_of_script ~include_paths mafile - in - let obj_writeable, obj_read_only = - if Filename.check_suffix mafile ".mma" then - Filename.chop_suffix mafile ".mma" ^ ".ma", - Filename.chop_suffix mafile ".mma" ^ ".ma" - else - LibraryMisc.obj_file_of_baseuri - ~must_exist:false ~baseuri ~writable:true, - LibraryMisc.obj_file_of_baseuri - ~must_exist:false ~baseuri ~writable:false - in - Some root, relpath, obj_writeable, obj_read_only - with Librarian.NoRootFor x -> None, "", "", "" - ;; - - let mtime_of_source_object s = - try Some (Unix.stat s).Unix.st_mtime - with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None - ;; + clean_exit baseuri exn - let mtime_of_target_object s = - try Some (Unix.stat s).Unix.st_mtime - with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> None - ;; - -(* FG: a problem was noticed in relising memory between subsequent *) -(* invocations of the compiler. The following might help *) - let compact r = Gc.compact (); r - - let build options fname = - let matita_debug = Helm_registry.get_bool "matita.debug" in - let compile opts fname = - try - (* MATITA 1.0: c'erano le push/pop per il parser; ma per - * l'environment nuovo? *) - compile opts fname - with - | Sys.Break -> false - | exn when not matita_debug -> - HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn)); - assert false - in - compact (compile options fname) - ;; - - let load_deps_file = Librarian.load_deps_file;; - - end - -module Make = Librarian.Make(F) - -(* FINE EX MATITACLIB *) - -let get_ast status ~include_paths text = - match GrafiteParser.parse_statement status (Ulexing.from_utf8_string text)with - (GrafiteAst.Executable - (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd - -> - let root, buri, _, tgt = - try Librarian.baseuri_of_script ~include_paths mafilename - with Librarian.NoRootFor _ -> - HLog.error ("The included file '"^mafilename^"' has no root file,"); - HLog.error "please create it."; - raise (Failure ("No root file for "^mafilename)) - in - if Make.make root [tgt] then - cmd - else raise (Failure ("Compiling: " ^ tgt)) - | cmd -> cmd -;; +(* BIG BUG: if a file recursively includes itself, anything can happen, + * from divergence to inclusion of an old copy of itself *) +and assert_ng ~include_paths ~root mapath = + let root',baseuri,_,_ = Librarian.baseuri_of_script ~include_paths mapath in + assert (root=root'); + let baseuri = NUri.uri_of_string baseuri in + let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in + let ngtime = + try + Some (Unix.stat ngpath).Unix.st_mtime + with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in + let matime = + try (Unix.stat mapath).Unix.st_mtime + with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = mapath -> assert false + in + let to_be_compiled = + match ngtime with + Some ngtime -> + let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in + let children_bad= List.exists (assert_ng ~include_paths ~root) preamble in + children_bad || matime > ngtime + | None -> true + in + if not to_be_compiled then false + else + (* MATITA 1.0: SHOULD TAKE THIS FROM THE STATUS *) + if List.mem baseuri (NCicLibrary.get_already_included ()) then + (* maybe recompiling it I would get the same... *) + raise (AlreadyLoaded (lazy mapath)) + else + (compile ~include_paths mapath; true) diff --git a/matita/matita/matitaEngine.mli b/matita/matita/matitaEngine.mli index 1175c2403..6af367614 100644 --- a/matita/matita/matitaEngine.mli +++ b/matita/matita/matitaEngine.mli @@ -23,8 +23,13 @@ * http://helm.cs.unibo.it/ *) +exception TryingToAdd of string Lazy.t +exception EnrichedWithStatus of exn * GrafiteTypes.status +exception AlreadyLoaded of string Lazy.t +exception FailureCompiling of string * exn + val get_ast: - #GrafiteParser.status -> include_paths:string list -> string -> + GrafiteTypes.status -> include_paths:string list -> Ulexing.lexbuf -> GrafiteAst.statement (* heavy checks slow down the compilation process but give you some interesting @@ -38,11 +43,4 @@ val eval_ast : (GrafiteTypes.status * (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) option) list - -exception EnrichedWithStatus of exn * GrafiteTypes.status - -(* EX MATITACLIB *) -module Make : sig - val make: string -> string list -> bool -end -(* FINE EX MATITACLIB *) +val assert_ng : include_paths:string list -> root:string -> string -> bool diff --git a/matita/matita/matitaExcPp.ml b/matita/matita/matitaExcPp.ml index 4be948dbb..ac1c23997 100644 --- a/matita/matita/matitaExcPp.ml +++ b/matita/matita/matitaExcPp.ml @@ -147,6 +147,13 @@ let rec to_string = None, "NCicEnvironment object not found: " ^ Lazy.force msg | NCicEnvironment.AlreadyDefined msg -> None, "NCicEnvironment already defined: " ^ Lazy.force msg + | MatitaEngine.TryingToAdd msg -> + None, "Attempt to insert an alias in batch mode: " ^ Lazy.force msg + | MatitaEngine.AlreadyLoaded msg -> + None, "The file " ^ Lazy.force msg ^ " needs recompilation but it is + already loaded; undo the inclusion and try again." + | MatitaEngine.FailureCompiling (filename,exn) -> + None, "Compiling " ^ filename ^ ": " ^ snd (to_string exn) | NCicRefiner.AssertFailure msg -> None, "NRefiner assert failure: " ^ Lazy.force msg | NCicEnvironment.BadDependency (msg,e) -> @@ -160,10 +167,8 @@ let rec to_string = None, "NCicUnification uncertain: " ^ Lazy.force msg | DisambiguateChoices.Choice_not_found msg -> None, ("Disambiguation choice not found: " ^ Lazy.force msg) - (* MATITA 1.0 | MatitaEngine.EnrichedWithStatus (exn,_) -> None, "EnrichedWithStatus "^snd(to_string exn) - *) | NTacStatus.Error (msg,None) -> None, "NTactic error: " ^ Lazy.force msg | NTacStatus.Error (msg,Some exn) -> diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index d963cf6a2..13db5d276 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -76,7 +76,7 @@ let save_moo grafite_status = | true, _ -> () | _, true -> GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) - grafite_status#dump + ~dependencies:grafite_status#dependencies grafite_status#dump | _ -> clean_current_baseuri grafite_status ;; diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 8e1eb69d4..2b849412b 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -188,7 +188,8 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff match statement with | `Raw text -> if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; - let ast = MatitaEngine.get_ast grafite_status include_paths text in + let strm = Ulexing.from_utf8_string text in + let ast = MatitaEngine.get_ast grafite_status include_paths strm in ast, text | `Ast (st, text) -> st, text in diff --git a/matita/matita/matitac.ml b/matita/matita/matitac.ml index 13b2aeb2f..08dab089f 100644 --- a/matita/matita/matitac.ml +++ b/matita/matita/matitac.ml @@ -57,7 +57,7 @@ let main_compiler () = if system_mode then HLog.message "Compiling in system space"; (* here we go *) if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup (); - if MatitaEngine.Make.make root target then + if List.for_all (MatitaEngine.assert_ng ~include_paths:[] ~root) target then (HLog.message "Compilation successful"; 0) else (HLog.message "Compilation failed"; 1) @@ -66,8 +66,7 @@ let main_compiler () = let main () = Sys.catch_break true; let bin = Filename.basename Sys.argv.(0) in - if Pcre.pmatch ~pat:"^matitadep" bin then Matitadep.main () - else if Pcre.pmatch ~pat:"^matitaclean" bin then Matitaclean.main () + if Pcre.pmatch ~pat:"^matitaclean" bin then Matitaclean.main () else exit (main_compiler ()) ;; diff --git a/matita/matita/matitadep.ml b/matita/matita/matitadep.ml deleted file mode 100644 index 315678307..000000000 --- a/matita/matita/matitadep.ml +++ /dev/null @@ -1,251 +0,0 @@ -(* 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/ - *) - -(* $Id$ *) - -module S = Set.Make (String) - -module GA = GrafiteAst -module HR = Helm_registry - -let print_times msg = - let times = Unix.times () in - let stamp = times.Unix.tms_utime +. times.Unix.tms_utime in - Printf.printf "TIME STAMP: %s: %f\n" msg stamp; flush stdout; stamp - -let fix_name f = - let f = - if Pcre.pmatch ~pat:"^\\./" f then String.sub f 2 (String.length f - 2) - else f - in - HExtlib.normalize_path f - -(* FG: old function left for reference *) -let exclude excluded_files files = - let map file = not (List.mem (fix_name file) excluded_files) in - List.filter map files - -let generate_theory theory_file deps = - if theory_file = "" then deps else - let map (files, deps) (t, d) = - if t = theory_file then files, deps else - S.add t files, List.fold_left (fun deps dep -> S.add dep deps) deps d - in - let out_include och dep = - Printf.fprintf och "include \"%s\".\n\n" dep - in - let fileset, depset = List.fold_left map (S.empty, S.empty) deps in - let top_depset = S.diff fileset depset in - let och = open_out theory_file in - begin - MatitaMisc.out_preamble och; - S.iter (out_include och) top_depset; - close_out och; - (theory_file, S.elements top_depset) :: deps - end - -let main () = - let _ = print_times "inizio" in - let include_paths = ref [] in - let use_stdout = ref false in - let theory_file = ref "" in - (* all are maps from "file" to "something" *) - let include_deps = Hashtbl.create 13 in - let baseuri_of = Hashtbl.create 13 in - let baseuri_of_inv = Hashtbl.create 13 in - let dot_name = "depends" in - let dot_file = ref "" in - let set_dot_file () = dot_file := dot_name^".dot" in - let set_theory_file s = theory_file := s ^ ".ma" in - (* helpers *) - let rec baseuri_of_script s = - try Hashtbl.find baseuri_of s - with Not_found -> - let _,b,_,_ = - Librarian.baseuri_of_script ~include_paths:!include_paths s - in - Hashtbl.add baseuri_of s b; - Hashtbl.add baseuri_of_inv b s; - let _ = - if Filename.check_suffix s ".mma" then - let generated = Filename.chop_suffix s ".mma" ^ ".ma" in - ignore (baseuri_of_script generated) - in - b - in - let script_of_baseuri ma b = - try Some (Hashtbl.find baseuri_of_inv b) - with Not_found -> - HLog.error ("Skipping dependency of '"^ma^"' over '"^b^"'"); - HLog.error ("Please include the file defining such baseuri, or fix"); - HLog.error ("possibly incorrect verbatim URIs in the .ma file."); - None - in - let buri alias = NUri.baseuri_of_uri (NUri.uri_of_string alias) in - let resolve alias current_buri = - let buri = buri alias in - if buri <> current_buri then Some buri else None - in - (* initialization *) - MatitaInit.add_cmdline_spec - ["-dot", Arg.Unit set_dot_file, - "Save dependency graph in dot format and generate a png"; - "-stdout", Arg.Set use_stdout, - "Print dependences on stdout"; - "-theory ", Arg.String set_theory_file, - "generate a theory file .ma (it includes all other files)" - ]; - MatitaInit.parse_cmdline_and_configuration_file (); - MatitaInit.initialize_environment (); - if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup (); - let cmdline_args = HR.get_list HR.string "matita.args" in - let test x = - Filename.check_suffix x ".ma" || Filename.check_suffix x ".mma" - in - let files = fun () -> match cmdline_args with - | [] -> HExtlib.find ~test "." - | _ -> cmdline_args - in - let args = - let roots = Librarian.find_roots_in_dir (Sys.getcwd ()) in - match roots with - | [] -> - prerr_endline ("No roots found in " ^ Sys.getcwd ()); - exit 1 - | [x] -> - Sys.chdir (Filename.dirname x); - let opts = Librarian.load_root_file "root" in - include_paths := - (try Str.split (Str.regexp " ") (List.assoc "include_paths" opts) - with Not_found -> []) @ - (HR.get_list HR.string "matita.includes"); - files () - | _ -> - let roots = List.map (HExtlib.chop_prefix (Sys.getcwd()^"/")) roots in - prerr_endline ("Too many roots found:\n\t"^String.concat "\n\t" roots); - prerr_endline ("\nEnter one of these directories and retry"); - exit 1 - in - let ma_files = args in - (* here we go *) - (* fills: - Hashtbl.add include_deps ma_file ma_file - Hashtbl.add include_deps_dot ma_file baseuri - *) - let _ = print_times "prima di iter1" in - List.iter (fun ma_file -> ignore (baseuri_of_script ma_file)) ma_files; - let _ = print_times "in mezzo alle due iter" in - let map s _ l = s :: l in - let ma_files = Hashtbl.fold map baseuri_of [] in - List.iter - (fun ma_file -> - let _ = if Filename.check_suffix ma_file ".mma" then - let generated = Filename.chop_suffix ma_file ".mma" ^ ".ma" in - Hashtbl.add include_deps generated ma_file; - in - let ma_baseuri = baseuri_of_script ma_file in - let dependencies = - let _ = print_times "prima deps_of_iter" in - try DependenciesParser.deps_of_file ma_file - with Sys_error _ -> [] - in - let _ = print_times "dopo deps_of_iter" in - let handle_uri uri = - if not (Http_getter_storage.is_legacy uri) then - let dep = resolve uri ma_baseuri in - match dep with - | None -> () - | Some u -> - match script_of_baseuri ma_file u with - | Some d -> Hashtbl.add include_deps ma_file d - | None -> () - in - let handle_script path = - ignore (baseuri_of_script path); - Hashtbl.add include_deps ma_file path - in - List.iter - (function - | DependenciesParser.UriDep uri -> - let uri = NUri.string_of_uri uri in - handle_uri uri - | DependenciesParser.InlineDep path -> - if Librarian.is_uri path - then handle_uri path else handle_script path - | DependenciesParser.IncludeDep path -> - handle_script path) - dependencies) - ma_files; - (* generate regular depend output *) - let _ = print_times "dopo di iter2" in - let deps = - List.fold_left - (fun acc ma_file -> - let deps = Hashtbl.find_all include_deps ma_file in - let deps = List.fast_sort Pervasives.compare deps in - let deps = HExtlib.list_uniq deps in - let deps = List.map fix_name deps in - (fix_name ma_file, deps) :: acc) - [] ma_files - in - let extern = - List.fold_left - (fun acc (_,d) -> - List.fold_left - (fun a x -> - if List.exists (fun (t,_) -> x=t) deps then a - else x::a) - acc d) - [] deps - in - let where = if !use_stdout then None else Some (Sys.getcwd()) in - let all_deps = - deps @ - HExtlib.list_uniq (List.sort Pervasives.compare (List.map (fun x -> x,[]) extern)) - in - (* theory generation *) - let all_deps_and_theory = generate_theory !theory_file all_deps in - (* matita depend file generation *) - Librarian.write_deps_file where all_deps_and_theory; - (* dot generation *) - if !dot_file <> "" then - begin - let oc = open_out !dot_file in - let fmt = Format.formatter_of_out_channel oc in - GraphvizPp.Dot.header fmt; - List.iter - (fun (ma_file,deps) -> - GraphvizPp.Dot.node ma_file fmt; - List.iter (fun dep -> GraphvizPp.Dot.edge ma_file dep fmt) deps) - deps; - List.iter - (fun x -> GraphvizPp.Dot.node ~attrs:["style","dashed"] x fmt) - extern; - GraphvizPp.Dot.trailer fmt; - close_out oc; - ignore(Sys.command ("tred "^ !dot_file^"| dot -Tpng -o"^dot_name^".png")); - HLog.message ("Type 'eog "^dot_name^".png' to view the graph"); - end; - let _ = print_times "fine" in () diff --git a/matita/matita/matitadep.mli b/matita/matita/matitadep.mli deleted file mode 100644 index 45d57a886..000000000 --- a/matita/matita/matitadep.mli +++ /dev/null @@ -1,27 +0,0 @@ -(* 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/ - *) - -val main: unit -> unit - -- 2.39.2