1 (* ========================================================================= *)
2 (* FLYSPECK - BOOK FORMALISATION *)
4 (* File to kickstart checkpointed flyspeck using BLCR *)
6 (* Author: Joe Pleso *)
8 (* ========================================================================= *)
11 let backup_stdout=Unix.dup Unix.stdout;;
12 let backup_stderr=Unix.dup Unix.stderr;;
14 let default_flag_list=[Unix.O_TRUNC;Unix.O_WRONLY;Unix.O_CREAT];;
17 let hollight_name = "hol_light";;
18 let hollight_stdout_name= hollight_name ^ ".out";;
19 let hollight_stdout=Unix.openfile hollight_stdout_name default_flag_list 420;;
20 let hollight_stderr_name= hollight_name ^ ".err";;
21 let hollight_stderr=Unix.openfile hollight_stderr_name default_flag_list 420;;
22 Unix.dup2 hollight_stdout Unix.stdout;;
23 Unix.dup2 hollight_stderr Unix.stderr;;
27 let flyspeck_name = "flyspeck";;
28 let flyspeck_stdout_name= flyspeck_name ^ ".out";;
29 let flyspeck_stdout=Unix.openfile flyspeck_stdout_name default_flag_list 420;;
30 let flyspeck_stderr_name= flyspeck_name ^ ".err";;
31 let flyspeck_stderr=Unix.openfile flyspeck_stderr_name default_flag_list 420;;
33 Unix.dup2 flyspeck_stdout Unix.stdout;;
34 Unix.dup2 flyspeck_stderr Unix.stderr;;
35 Unix.close hollight_stdout;;
36 Unix.close hollight_stderr;;
37 #use "strictbuild.hl";;
39 Unix.dup2 backup_stdout Unix.stdout;;
40 Unix.dup2 backup_stderr Unix.stderr;;
41 Unix.close backup_stdout;;
42 Unix.close backup_stderr;;
43 Unix.close flyspeck_stdout;;
44 Unix.close flyspeck_stderr;;
46 let ocampl_pid()=process_to_string "echo -n $PPID";;
47 let blcr()=(build_silent o ignore o Sys.command)
48 ("cr_checkpoint -f context.ocampl --backup --term " ^ (ocampl_pid()) ^ " &");;