(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Build for all chapters                                            *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-07-14                                                           *)
(* ========================================================================== *)


(* 
   Build file for Flyspeck project.
   ocaml needs to be built with Unix.
   ocamlmktop unix.cma str.cma nums.cma -o ocampl

   the system dependent string flyspeck should be set to the "text_formalization" path.
   For example, on my system, I have added a line to my .bashrc file
   export FLYSPECK_DIR="$HOME/Desktop/flyspeck_google/source/text_formalization"

   hol-light should already be loaded
   #use "hol.ml";;

 *)
#load "str.cma";;

(* HOL LIGHT *)
hol_version;;
needs "Multivariate/flyspeck.ml";;
needs "Rqe/num_calc_simp.ml";;  


(*

*)
let flyspeck_dir = 
  (try Sys.getenv "FLYSPECK_DIR" with Not_found -> Sys.getcwd());;

let hollight_dir = 
  (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());;


(* bug: process_to_string does not close forked processes.
   For example process_to_string ("date | grep 'Nov'" ), 
   leaves a process in the background.
   I'm not sure why this happens. *)

let process_to_string unixstring = 
  let p = Unix.open_process_in unixstring
  and b = Buffer.create 64 in
  let rec read () = Buffer.add_channel b p 1; read () in
    try read () with End_of_file -> (Unix.close_process_in p; Buffer.contents b);;

let load_date = process_to_string "date";;

(* potential bug:
   the svn version does not reflect recent commits, unless followed by an update.
*)

let flyspeck_version() = "Flyspeck "^
  process_to_string ("svn info "^flyspeck_dir^ " | grep Revision");;

let hollight_version() = "HOL Light "^
  process_to_string ("svnversion "^hollight_dir);;

let ocaml_version() = "Ocaml "^Sys.ocaml_version;;

let build_date() = "Build: " ^ process_to_string "date";;
let build_user() = "User: " ^ process_to_string "whoami";;
let indent = "   ";;

let build_report s =  build_date() ^ 
  indent ^ build_user() ^ 
  indent ^ hollight_version() ^ 
  indent ^ flyspeck_version() ^ 
  indent ^ ocaml_version() ^ "\n" ^ indent^ s^ "\n";;

let fullpath s = Filename.concat flyspeck_dir s;;


(*
Sys.command("svn info "^flyspeck_dir^" | grep Revison");;
*)



(* boolean valued versions of Harrison's load files that return false
   if load was not a success *)

let use_file_b s =
  if not(Sys.file_exists s) 
  then (report ("File not found "^s); false)
  else 
    (Toploop.use_file Format.std_formatter s) or 
      (Format.print_string("Error in included file "^s);
       Format.print_newline(); false);;

let load_on_path_b p s =
  let s' = file_on_path p s in
  let fileid = (Filename.basename s',Digest.file s') in
    (use_file_b s' && (loaded_files := fileid::(!loaded_files);true));;

let loadb s = load_on_path_b (!load_path) s;;

let needb s =
  let s' = file_on_path (!load_path) s in
  let fileid = (Filename.basename s',Digest.file s') in
    if List.mem fileid (!loaded_files)
    then (Format.print_string("File \""^s^"\" already loaded\n");true) 
    else loadb s;;

(* debugging *)
loadt (fullpath "general/parser_verbose.hl");;
loadt (fullpath "general/debug.hl");;
Debug.set_verbose_parsing();;


(* limit changes in the state of the proof assistant  *)

let CHEAT_TAC = FAIL_TAC "cheaters never prosper";;
let new_axiom _ = failwith "new_axiom has been disabled.";; 
let mk_thm _ = failwith "mk_thm has been disabled.  Use mk_fthm";;

loadt (fullpath "general/state_manager.hl");;
let reneeds s = loadt (fullpath s);;
let rflyspeck_needs = reneeds;;

State_manager.neutralize_state();;

let fileid s = 
  let s' = file_on_path (!load_path) (fullpath s) in
    (Filename.basename s',Digest.file s');;

(* The dependency calculation in flyspeck_needs still has a bug if the
   file does not load correctly, but it calls another file that does load
   correctly.  It seems that the correctly loaded modules disappear from
   the scope when the error is encountered.  Thus, they should be
   filtered out as well from the depend statement.  For now, we offer
   depend_reset to clear the error.
*)

let (flyspeck_needs,filetable,depend,depend_reset)  =
  let ftable = ref [("pervasives",List.length (constants()))] in 
   (* associate constants with files *) 
  let depend = ref ([]:((string*Digest.t)*(string*Digest.t)) list) in 
   (* dependency table *)
  let host = ref (fileid "build.hl") in
  let fn = fun s->
  let id = fileid s in 
    if (List.mem id (!loaded_files))
    then Format.print_string("File \""^s^"\" already loaded\n")
    else
      (
        if List.mem (!host,id) (!depend) then failwith "There may be circular needs.";
	depend := (!host,id)::(!depend);	       
	let h = !host in 
        let _ = (host := id) in
        let b= needb (fullpath s) in
        let _ = (host := h) in
	let _ = try State_manager.neutralize_state () with
	    Failure msg -> Format.print_string("File \""^s^
		 "\"corrupted neutral state.\n"^msg^"\n") in
	  if b then (
            (ftable:= (s,List.length(constants()))::(!ftable));
	    Format.print_string("File \""^s^"\" successfully loaded\n"))
	  else (depend := filter ((<>) (h,id)) (!depend); 
            failwith ("Aborting Flyspeck Needs "^s))
      ) in
    (fn,(fun () -> !ftable),(fun() -> !depend),(fun() -> (depend:=[])));;



(* disable "needs" for now *)
(*
let needs' = needs;;
let needs _ = failwith "Use flyspeck_needs rather than needs";;
*)

(* utilities *)
flyspeck_needs "general/print_types.hl";;
flyspeck_needs  "general/update_database_310.ml";; 
flyspeck_needs "general/prove_by_refinement.hl";;
(* flyspeck_needs "general/flyspeck_utility.hl";; *)
let dest_goal gl = gl;;
let goal_asms = fst;;
let goal_concl = snd;;
let mk_goal(asl,w) = (asl,w);;

(* verbose error reporting *)


let prove_by_refinement = Debug.verbose Prove_by_refinement.prove_by_refinement;;
let prove = Debug.verbose prove;;
let new_definition = Debug.verbose_1 new_definition;;
let ABBREV_TAC = Debug.verbose_1 ABBREV_TAC;;
let EXISTS_TAC = Debug.verbose_1 EXISTS_TAC;;

(* This next one gets iterated in FIRST_ASSUM and creates multiple error messages *)
(* let ISPECL = Debug.verbose_thm ISPECL;; *)

flyspeck_needs "build.hl";;

let build_and_report() = 
  let s = try
    (let _ = map flyspeck_needs Build.build_sequence in  "full load completed")
  with Failure t -> t  in
  let oc = open_out_gen [Open_append;Open_text] 436 (fullpath "log.txt") in
  (Pervasives.output_string oc (build_report s); close_out oc);;

let build_silent() = 
  let s = try
    (let _ = map flyspeck_needs Build.build_sequence in  "full load completed")
  with Failure t ->  t  in
     build_report s;;

let try_do f  = 
  let rec try_dof = function
      [] -> [] 
    | (x::t) -> 
	try
	  (let y = f x in y:: try_dof t)
	with Failure _ -> [] in
    try_dof;;

let already_loaded s =
  let s' = file_on_path (!load_path) s in
  let fileid = (Filename.basename s',Digest.file s') in
    List.mem fileid (!loaded_files);;

let new_build_silent() = 
  let loaded = try_do (fun s -> flyspeck_needs s; s) Build.build_sequence in
  let unloaded = filter(not o already_loaded) Build.build_sequence in
    (loaded,unloaded);;

let rec cut_after f a acc = function
  | [] -> acc
  | b::bs -> if (f b =a) then (b::acc) else cut_after f a (b::acc) bs;;

let reset_after s = 
  (loaded_files := cut_after fst s [] (List.rev (!loaded_files)));;

let reset () = (reset_after "hol_pervasives.hl"; depend_reset());;

(* let reset() = reset_after "flyspeck.ml";; *)