X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitamakeLib.ml;h=998dcd70edf225f595509a23ff822d715f63fb98;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=534f2dc7383acba7ad01bac7a2b11dd3334112d3;hpb=3e86f296f53e98401b281ce96fc7ba545dbd05b4;p=helm.git diff --git a/helm/matita/matitamakeLib.ml b/helm/matita/matitamakeLib.ml index 534f2dc73..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 @@ -169,14 +171,17 @@ let make chdir args = 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 make -exception CHILD_DEAD - (* not really good vt100 *) let vt100 s = let rex = Pcre.regexp "\\[[0-9;]+m" in @@ -213,10 +218,8 @@ let mk_maker refresh_cb = 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 _ = - Sys.signal Sys.sigchld (Sys.Signal_handle (fun _ -> raise CHILD_DEAD)) - in let argv = Array.of_list ("make"::args) in pid := Unix.create_process "make" argv Unix.stdin out_w err_w; Unix.close out_w; @@ -226,7 +229,9 @@ let mk_maker refresh_cb = | f::tl -> let len = Unix.read f buf 0 1024 in if len = 0 then - raise CHILD_DEAD; + raise + (Unix.Unix_error + (Unix.EPIPE,"read","len = 0 (matita internal)")); vt100 (String.sub buf 0 len); aux tl | _ -> () @@ -237,11 +242,9 @@ let mk_maker refresh_cb = refresh_cb () done; true - with CHILD_DEAD -> - ignore(Sys.signal Sys.sigchld (Sys.Signal_ignore)); - let _, status = Unix.waitpid [] !pid in - match status with | Unix.WEXITED 0 -> true | _ -> false) - + 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) @@ -253,7 +256,7 @@ let clean_development development = 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 @@ -273,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 @@ -284,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