(* Nov 2010 *)


(* Desktop init.                                *)

let set_load_path() = (   load_path:= 
     let dir = (Sys.getenv "FLYSPECK_DIR") in
     let jdir = Filename.concat dir "../jHOLLight" in
      dir::jdir::(!load_path));;

let general_init() = 
  let _ = set_load_path() in
    needs "strictbuild.hl";;

general_init();;
(* #load "unix.cma";; (* dynamic loading not supported *) *)

(* Build.build_all();; *)
flyspeck_needs"build.hl";;
reneeds "strictbuild.hl";;

(* map reneeds Build.build_sequence;; *)
let _ = set_load_path() in
  build_silent();;
build_and_report();;
Debug.silent:=true;; (* don't print debug error messages *)
reset();;


new_build_silent();;
new_build_silent();;

(* searching *)

let open_search =
  let _ = flyspeck_needs "general/tactics.hl" in
  let _ = flyspeck_needs "usr/thales/hales_tactic.hl" in
  let _ = reneeds "usr/thales/searching.hl" in
  let _ = reneeds "usr/thales/init_search.hl" in ();;

open Searching;;
open Hales_tactic;;

(* END LOCAL BUILD *)



(* SEARCH *)

help "ABBREV_TAC";;
help "help";;
help_grep "ASM";;
help_grep "apropos";;
help_flag 'i' "r.*w";;
help_flag 'l' "search";;
help_flag '?' "";;
help_flag 'd' "face";;

help "apropos_searching";;
help "apropos_types";;


(* load misc files *)


(* fin *)