make.ml

   1 (* ========================================================================= *)
   2 (* Create a standalone HOL image. Assumes that we are running under Linux    *)
   3 (* and have the program "ckpt" available to create checkpoints.              *)
   4 (*                                                                           *)
   5 (*              (c) Copyright, John Harrison 1998-2007                       *)
   6 (* ========================================================================= *)
   7
   8 #use "hol.ml";;
   9
  10 (* ------------------------------------------------------------------------- *)
  11 (* Record the build date and OCaml version for the startup banner.           *)
  12 (* ------------------------------------------------------------------------- *)
  13
  14 #load "unix.cma";;
  15
  16 let startup_banner =
  17    let {Unix.tm_mday = d;Unix.tm_mon = m;Unix.tm_year = y;Unix.tm_wday = w} =
  18      Unix.localtime(Unix.time()) in
  19   let nice_date = string_of_int d ^ " " ^
  20     el m ["January"; "February"; "March"; "April"; "May"; "June";
  21           "July"; "August"; "September"; "October"; "November"; "December"] ^
  22     " " ^ string_of_int(1900+y) in
  23   "        HOL Light "^hol_version^
  24   ", built "^nice_date^" on OCaml "^Sys.ocaml_version;;
  25
  26 (* ------------------------------------------------------------------------- *)
  27 (* Self-destruct to create checkpoint file; print banner when restarted.     *)
  28 (* ------------------------------------------------------------------------- *)
  29
  30 let self_destruct bannerstring =
  31   let longer_banner = startup_banner ^ " with ckpt" in
  32   let complete_banner =
  33     if bannerstring = "" then longer_banner
  34     else longer_banner^"\n        "^bannerstring in
  35   (Gc.compact();
  36    ignore(Unix.system "sleep 1s; kill -USR1 $PPID");
  37    Format.print_string complete_banner;
  38    Format.print_newline(); Format.print_newline());;
  39
  40 (* ------------------------------------------------------------------------- *)
  41 (* Non-destructive checkpoint using CryoPID "freeze".                        *)
  42 (* ------------------------------------------------------------------------- *)
  43
  44 let checkpoint bannerstring =
  45   let rec waste_time n = if n = 0 then () else waste_time(n - 1) in
  46   let longer_banner = startup_banner ^ " with CryoPID" in
  47   let complete_banner =
  48     if bannerstring = "" then longer_banner
  49     else longer_banner^"\n        "^bannerstring in
  50   (Gc.compact();
  51    ignore(Unix.system "(sleep 1s; freeze -l hol.snapshot $PPID) &");
  52    waste_time 100000000;
  53    Format.print_string complete_banner;
  54    Format.print_newline(); Format.print_newline());;