pkgs/applications/science/logic/hol_light/selfcheckpoint_complex.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 (*              (c) Copyright, John Harrison 1998-2007                       *)
   6 (*              (c) Copyright, Marco Maggesi 2010                            *)
   7 (* ========================================================================= *)
   8
   9 #use "make.ml";;
  10
  11 (* ------------------------------------------------------------------------- *)
  12 (* Non-destructive checkpoint using DMTCP.                                   *)
  13 (* ------------------------------------------------------------------------- *)
  14
  15 let checkpoint bannerstring =
  16   let longer_banner = startup_banner ^ " with DMTCP" in
  17   let complete_banner =
  18     if bannerstring = "" then longer_banner
  19     else longer_banner^"\n        "^bannerstring in
  20   (Gc.compact();
  21    loadt "Examples/update_database.ml";
  22    print_newline ();
  23    Unix.sleep 1;
  24    try ignore(Unix.system ("dmtcp_command -bc")) with _ -> ();
  25    Format.print_string complete_banner;
  26    Format.print_newline(); Format.print_newline());;
  27
  28 loadt "Multivariate/make_complex.ml";;
  29 dmtcp_checkpoint "Preloaded with multivariate-based complex analysis";;