pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml

   1 (* ------------------------------------------------------------------------- *)
   2 (* Create a standalone HOL image. Assumes that we are running under Linux    *)
   3 (* and have the program "dmtcp" available to create checkpoints.             *)
   4 (* ------------------------------------------------------------------------- *)
   5
   6 let dmtcp_checkpoint, dmtcp_selfdestruct =
   7   let call_dmtcp opts bannerstring =
   8     let longer_banner = startup_banner ^ " with DMTCP" in
   9     let complete_banner =
  10       if bannerstring = "" then longer_banner
  11       else longer_banner^"\n        "^bannerstring in
  12     (Gc.compact(); Unix.sleep 1;
  13      Format.print_string "Checkpointing..."; Format.print_newline();
  14      try ignore(Unix.system ("dmtcp_command -bc " ^ opts))
  15      with Unix.Unix_error _ -> ();
  16      Format.print_string complete_banner;
  17      Format.print_newline(); Format.print_newline())
  18   in
  19   call_dmtcp "", call_dmtcp "-q";;