X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitamakeLib.ml;h=998dcd70edf225f595509a23ff822d715f63fb98;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=512da157ae5cbdedfbe56b46b36a400699d31aa5;hpb=619a3a478a4f6b0a50782b620009f6a141c30a53;p=helm.git diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml index 512da157a..998dcd70e 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,23 +119,22 @@ 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 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 + HExtlib.output_file ~filename:makefilepath ~text:template (* creates a new development if possible *) let initialize_development name dir = + let name = Pcre.replace ~pat:" " ~templ:"_" name in let dev = {name = name ; root = dir} in match development_for_dir dir with | Some d -> @@ -156,7 +155,10 @@ let make chdir args = let old = Unix.getcwd () in try Unix.chdir chdir; - let rc = Unix.system (String.concat " " ("make"::args)) in + let rc = + Unix.system + (String.concat " " ("make"::(List.map Filename.quote args))) + in Unix.chdir old; match rc with | Unix.WEXITED 0 -> true @@ -166,19 +168,95 @@ let make chdir args = logger `Warning ("Unix Error: " ^ cmd ^ ": " ^ err); false -let call_make development target = +let call_make development target make = rebuild_makefile development; let makefile = makefile_for_development development in + let nodb = + Helm_registry.get_opt_default Helm_registry.bool ~default:false "db.nodb" + in + let flags = if nodb then ["NODB=true"] else [] in make development.root - ["--no-print-directory"; "-s"; "-k"; "-f"; makefile; target] + (["--no-print-directory"; "-s"; "-k"; "-f"; makefile; target] + @ flags) let build_development ?(target="all") development = - call_make development target + call_make development target make + +(* not really good vt100 *) +let vt100 s = + let rex = Pcre.regexp "\\[[0-9;]+m" in + let rex_i = Pcre.regexp "^Info" in + let rex_w = Pcre.regexp "^Warning" in + let rex_e = Pcre.regexp "^Error" in + let rex_d = Pcre.regexp "^Debug" in + let rex_noendline = Pcre.regexp "\\n" in + let s = Pcre.replace ~rex:rex_noendline s in + let len = String.length s in + let tokens = Pcre.split ~rex s in + let logger = ref MatitaLog.message in + let rec aux = + function + | [] -> () + | s::tl -> + (if Pcre.pmatch ~rex:rex_i s then + logger := MatitaLog.message + else if Pcre.pmatch ~rex:rex_w s then + logger := MatitaLog.warn + else if Pcre.pmatch ~rex:rex_e s then + logger := MatitaLog.error + else if Pcre.pmatch ~rex:rex_d s then + logger := MatitaLog.debug + else + !logger s); + aux tl + in + aux tokens + +let mk_maker refresh_cb = + (fun chdir args -> + let out_r,out_w = Unix.pipe () in + let err_r,err_w = Unix.pipe () in + let pid = ref ~-1 in + ignore(Sys.signal Sys.sigchld (Sys.Signal_ignore)); + try + let argv = Array.of_list ("make"::args) in + pid := Unix.create_process "make" argv Unix.stdin out_w err_w; + Unix.close out_w; + Unix.close err_w; + let buf = String.create 1024 in + let rec aux = function + | f::tl -> + let len = Unix.read f buf 0 1024 in + if len = 0 then + raise + (Unix.Unix_error + (Unix.EPIPE,"read","len = 0 (matita internal)")); + vt100 (String.sub buf 0 len); + aux tl + | _ -> () + in + while true do + let r,_,_ = Unix.select [out_r; err_r] [] [] (-. 1.) in + aux r; + refresh_cb () + done; + true + with + | Unix.Unix_error (_,"read",_) + | Unix.Unix_error (_,"select",_) -> true) + +let build_development_in_bg ?(target="all") refresh_cb development = + call_make development target (mk_maker refresh_cb) +;; + let clean_development development = - call_make development "clean" + call_make development "clean" make + +let clean_development_in_bg refresh_cb development = + call_make development "clean" (mk_maker refresh_cb) -let destroy_development development = +let destroy_development_aux development clean_development = let delete_development development = let unlink file = try @@ -198,7 +276,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 @@ -209,6 +286,12 @@ let destroy_development development = logger `Warning "This may cause garbage." end; delete_development development + +let destroy_development development = + destroy_development_aux development clean_development + +let destroy_development_in_bg refresh development = + destroy_development_aux development (clean_development_in_bg refresh) let root_for_development development = development.root let name_for_development development = development.name