text_formalization/boot.ml

   1 (* ========================================================================= *)
   2 (* FLYSPECK - BOOK FORMALISATION                                             *)
   3 (*                                                                           *)
   4 (* File to kickstart checkpointed flyspeck using BLCR                        *)
   5 (*                                                                           *)
   6 (* Author: Joe Pleso                                                         *)
   7 (* Date:   2011-04-20                                                        *)
   8 (* ========================================================================= *)
   9
  10
  11 let backup_stdout=Unix.dup Unix.stdout;;
  12 let backup_stderr=Unix.dup Unix.stderr;;
  13
  14 let default_flag_list=[Unix.O_TRUNC;Unix.O_WRONLY;Unix.O_CREAT];;
  15
  16
  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;;
  24
  25 #use "hol.ml";;
  26
  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;;
  32
  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";;
  38 build_silent();;
  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;;
  45
  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()) ^ " &");;
  49 blcr();;