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 ())
(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
(* 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 () =
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 template = Pcre.replace ~pat:"@DEP@" ~templ:mm template in
let template = Pcre.replace ~pat:"@DEPFILE@" ~templ:df 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 ->
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
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
try
let argv = Array.of_list ("make"::args) in
pid := Unix.create_process "make" argv Unix.stdin out_w err_w;
-let ch = open_out "/tmp/pippo" in output_string ch (String.concat " " ("make"::(Array.to_list argv)) ^ "\n"); flush ch; close_out ch;
Unix.close out_w;
Unix.close err_w;
let buf = String.create 1024 in
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
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