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