development/thales/session/localbuild.hl

   1 (* Nov 2010 *)
   2
   3
   4 (* Desktop init.                                *)
   5
   6 let set_load_path() = (   load_path:=
   7      let dir = (Sys.getenv "FLYSPECK_DIR") in
   8      let jdir = Filename.concat dir "../jHOLLight" in
   9       dir::jdir::(!load_path));;
  10
  11 let general_init() =
  12   let _ = set_load_path() in
  13     needs "strictbuild.hl";;
  14
  15 general_init();;
  16 (* #load "unix.cma";; (* dynamic loading not supported *) *)
  17
  18 (* Build.build_all();; *)
  19 flyspeck_needs"build.hl";;
  20 reneeds "strictbuild.hl";;
  21
  22 (* map reneeds Build.build_sequence;; *)
  23 let _ = set_load_path() in
  24   build_silent();;
  25 build_and_report();;
  26 Debug.silent:=true;; (* don't print debug error messages *)
  27 reset();;
  28
  29
  30 new_build_silent();;
  31 new_build_silent();;
  32
  33 (* searching *)
  34
  35 let open_search =
  36   let _ = flyspeck_needs "general/tactics.hl" in
  37   let _ = flyspeck_needs "usr/thales/hales_tactic.hl" in
  38   let _ = reneeds "usr/thales/searching.hl" in
  39   let _ = reneeds "usr/thales/init_search.hl" in ();;
  40
  41 open Searching;;
  42 open Hales_tactic;;
  43
  44 (* END LOCAL BUILD *)
  45
  46
  47
  48 (* SEARCH *)
  49
  50 help "ABBREV_TAC";;
  51 help "help";;
  52 help_grep "ASM";;
  53 help_grep "apropos";;
  54 help_flag 'i' "r.*w";;
  55 help_flag 'l' "search";;
  56 help_flag '?' "";;
  57 help_flag 'd' "face";;
  58
  59 help "apropos_searching";;
  60 help "apropos_types";;
  61
  62
  63 (* load misc files *)
  64
  65
  66 (* fin *)