X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitamakeLib.ml;h=503ed210f53401414236c2f51eb46d195c7c3cae;hb=d0e212dcd4bdbeaee9979e53bedd3258cd8e8d0f;hp=38f8123888ecdf2a3644788d153faf805e548fae;hpb=3158b6cbc3b374a7840e79c2cd35dd46ffeaf324;p=helm.git diff --git a/matita/matitamakeLib.ml b/matita/matitamakeLib.ml index 38f812388..503ed210f 100644 --- a/matita/matitamakeLib.ml +++ b/matita/matitamakeLib.ml @@ -137,34 +137,35 @@ let rebuild_makefile development = let template = Pcre.replace ~pat:"@CLEAN@" ~templ:rm template in HExtlib.output_file ~filename:makefilepath ~text:template +let rebuild_makefile_devel development = + let path = development.root ^ "/makefile" in + if not (Sys.file_exists path) then + begin + let template = + HExtlib.input_file BuildTimeConf.matitamake_makefile_template_devel + in + let template = + Pcre.replace ~pat:"@MATITA_RT_BASE_DIR@" + ~templ:BuildTimeConf.runtime_base_dir template + in + HExtlib.output_file ~filename:path ~text:template + end + (* 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 dev -> - if dir <> dev.root then begin - logger `Error - (sprintf ("Dir \"%s\" is already handled by development \"%s\"\n" - ^^ "Development \"%s\" is rooted in \"%s\"\n" - ^^ "Dir \"%s\" is a sub-dir of \"%s\"") - dir dev.name dev.name dev.root dir dev.root); - None - end else (* requirement development alreay exists, do nothing *) - Some dev - | None -> - dump_development dev; - rebuild_makefile dev; - developments := dev :: !developments; - Some dev + dump_development dev; + rebuild_makefile dev; + rebuild_makefile_devel dev; + developments := dev :: !developments; + Some dev let make chdir args = let old = Unix.getcwd () in try Unix.chdir chdir; let cmd = String.concat " " ("make" :: List.map Filename.quote args) in - if Helm_registry.get_int "matita.verbosity" > 1 then - HLog.debug (sprintf "MATITAMAKE: %s" cmd); let rc = Unix.system cmd in Unix.chdir old; match rc with @@ -175,24 +176,35 @@ let make chdir args = logger `Warning ("Unix Error: " ^ cmd ^ ": " ^ err); false -let call_make development target make = +let call_make ?matita_flags development target make = + let matita_flags = + let already_defined = + match matita_flags with + | None -> (try Sys.getenv "MATITA_FLAGS" with Not_found -> "") + | Some s -> s + in + already_defined ^ + if Helm_registry.get_bool "matita.bench" then "-bench" else "" + in 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 = [] in + let flags = [] in let flags = flags @ if nodb then ["NODB=true"] else [] in let flags = try - flags @ [ sprintf "MATITA_FLAGS=%s" (Sys.getenv "MATITA_FLAGS") ] + flags @ [ sprintf "MATITA_FLAGS=\"%s\"" matita_flags ] with Not_found -> flags in - make development.root - (["--no-print-directory"; "-s"; "-k"; "-f"; makefile; target] - @ flags) + let args = + ["--no-print-directory"; "-s"; "-k"; "-f"; makefile; target] @ flags + in +(* prerr_endline (String.concat " " args); *) + make development.root args -let build_development ?(target="all") development = - call_make development target make +let build_development ?matita_flags ?(target="all") development = + call_make ?matita_flags development target make (* not really good vt100 *) let vt100 s = @@ -230,7 +242,8 @@ let mk_maker refresh_cb = let err_r,err_w = Unix.pipe () in let pid = ref ~-1 in ignore(Sys.signal Sys.sigchld (Sys.Signal_ignore)); - try + try +(* prerr_endline (String.concat " " args); *) let argv = Array.of_list ("make"::args) in pid := Unix.create_process "make" argv Unix.stdin out_w err_w; Unix.close out_w; @@ -257,23 +270,19 @@ let mk_maker refresh_cb = | 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 build_development_in_bg ?matita_flags ?(target="all") refresh_cb development = + call_make ?matita_flags development target (mk_maker refresh_cb) ;; -let clean_development development = - call_make development "clean" make +let clean_development ?matita_flags development = + call_make ?matita_flags development "clean" make -let clean_development_in_bg refresh_cb development = - call_make development "clean" (mk_maker refresh_cb) +let clean_development_in_bg ?matita_flags refresh_cb development = + call_make development ?matita_flags "clean" (mk_maker refresh_cb) let destroy_development_aux development clean_development = let delete_development development = - let unlink file = - try - Unix.unlink file - with Unix.Unix_error _ -> logger `Debug ("Unable to delete " ^ file) - in + let unlink = HExtlib.safe_remove in let rmdir dir = try Unix.rmdir dir @@ -287,6 +296,7 @@ let destroy_development_aux development clean_development = unlink (makefile_for_development development); unlink (pool () ^ development.name ^ rootfile); unlink (pool () ^ development.name ^ "/depend"); + unlink (pool () ^ development.name ^ "/depend.errors"); rmdir (pool () ^ development.name); developments := List.filter (fun d -> d.name <> development.name) !developments @@ -298,12 +308,45 @@ let destroy_development_aux development clean_development = end; delete_development development -let destroy_development development = - destroy_development_aux development clean_development +let destroy_development ?matita_flags development = + destroy_development_aux development (clean_development ?matita_flags) -let destroy_development_in_bg refresh development = - destroy_development_aux development (clean_development_in_bg refresh) +let destroy_development_in_bg ?matita_flags refresh development = + destroy_development_aux development + (clean_development_in_bg refresh ?matita_flags ) let root_for_development development = development.root let name_for_development development = development.name +let publish_development_bstract build clean devel = + let matita_flags = "\"-system\"" in + HLog.message "cleaning the development before publishing"; + if clean ~matita_flags:"" devel then + begin + HLog.message "rebuilding the development in 'system' space"; + if build ~matita_flags devel then + begin + HLog.message "publishing succeded"; + true + end + else + begin + HLog.error "building process failed, reverting"; + if not (clean ~matita_flags devel) then + HLog.error "cleaning failed, end of the world (2)"; + false + end + end + else + (HLog.error "unable to clean the development, publishing failed"; false) + +let publish_development devel = + publish_development_bstract + (fun ~matita_flags devel -> build_development ~matita_flags devel) + (fun ~matita_flags devel -> clean_development ~matita_flags devel) devel +let publish_development_in_bg cb devel = + publish_development_bstract + (fun ~matita_flags devel -> build_development_in_bg cb ~matita_flags devel) + (fun ~matita_flags devel -> clean_development_in_bg cb ~matita_flags devel) + devel +