text_formalization/strictbuild.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Build for all chapters                                            *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-07-14                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10 (*
  11    Build file for Flyspeck project.
  12    ocaml needs to be built with Unix.
  13    ocamlmktop unix.cma str.cma nums.cma -o ocampl
  14
  15    the system dependent string flyspeck should be set to the "text_formalization" path.
  16    For example, on my system, I have added a line to my .bashrc file
  17    export FLYSPECK_DIR="$HOME/Desktop/flyspeck_google/source/text_formalization"
  18
  19    hol-light should already be loaded
  20    #use "hol.ml";;
  21
  22  *)
  23 #load "str.cma";;
  24
  25 (* HOL LIGHT *)
  26 hol_version;;
  27 needs "Multivariate/flyspeck.ml";;
  28 needs "Rqe/num_calc_simp.ml";;
  29
  30
  31 (*
  32
  33 *)
  34 let flyspeck_dir =
  35   (try Sys.getenv "FLYSPECK_DIR" with Not_found -> Sys.getcwd());;
  36
  37 let hollight_dir =
  38   (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());;
  39
  40
  41 (* bug: process_to_string does not close forked processes.
  42    For example process_to_string ("date | grep 'Nov'" ),
  43    leaves a process in the background.
  44    I'm not sure why this happens. *)
  45
  46 let process_to_string unixstring =
  47   let p = Unix.open_process_in unixstring
  48   and b = Buffer.create 64 in
  49   let rec read () = Buffer.add_channel b p 1; read () in
  50     try read () with End_of_file -> (Unix.close_process_in p; Buffer.contents b);;
  51
  52 let load_date = process_to_string "date";;
  53
  54 (* potential bug:
  55    the svn version does not reflect recent commits, unless followed by an update.
  56 *)
  57
  58 let flyspeck_version() = "Flyspeck "^
  59   process_to_string ("svn info "^flyspeck_dir^ " | grep Revision");;
  60
  61 let hollight_version() = "HOL Light "^
  62   process_to_string ("svnversion "^hollight_dir);;
  63
  64 let ocaml_version() = "Ocaml "^Sys.ocaml_version;;
  65
  66 let build_date() = "Build: " ^ process_to_string "date";;
  67 let build_user() = "User: " ^ process_to_string "whoami";;
  68 let indent = "   ";;
  69
  70 let build_report s =  build_date() ^
  71   indent ^ build_user() ^
  72   indent ^ hollight_version() ^
  73   indent ^ flyspeck_version() ^
  74   indent ^ ocaml_version() ^ "\n" ^ indent^ s^ "\n";;
  75
  76 let fullpath s = Filename.concat flyspeck_dir s;;
  77
  78
  79 (*
  80 Sys.command("svn info "^flyspeck_dir^" | grep Revison");;
  81 *)
  82
  83
  84
  85 (* boolean valued versions of Harrison's load files that return false
  86    if load was not a success *)
  87
  88 let use_file_b s =
  89   if not(Sys.file_exists s)
  90   then (report ("File not found "^s); false)
  91   else
  92     (Toploop.use_file Format.std_formatter s) or
  93       (Format.print_string("Error in included file "^s);
  94        Format.print_newline(); false);;
  95
  96 let load_on_path_b p s =
  97   let s' = file_on_path p s in
  98   let fileid = (Filename.basename s',Digest.file s') in
  99     (use_file_b s' && (loaded_files := fileid::(!loaded_files);true));;
 100
 101 let loadb s = load_on_path_b (!load_path) s;;
 102
 103 let needb s =
 104   let s' = file_on_path (!load_path) s in
 105   let fileid = (Filename.basename s',Digest.file s') in
 106     if List.mem fileid (!loaded_files)
 107     then (Format.print_string("File \""^s^"\" already loaded\n");true)
 108     else loadb s;;
 109
 110 (* debugging *)
 111 loadt (fullpath "general/parser_verbose.hl");;
 112 loadt (fullpath "general/debug.hl");;
 113 Debug.set_verbose_parsing();;
 114
 115
 116 (* limit changes in the state of the proof assistant  *)
 117
 118 let CHEAT_TAC = FAIL_TAC "cheaters never prosper";;
 119 let new_axiom _ = failwith "new_axiom has been disabled.";;
 120 let mk_thm _ = failwith "mk_thm has been disabled.  Use mk_fthm";;
 121
 122 loadt (fullpath "general/state_manager.hl");;
 123 let reneeds s = loadt (fullpath s);;
 124 let rflyspeck_needs = reneeds;;
 125
 126 State_manager.neutralize_state();;
 127
 128 let fileid s =
 129   let s' = file_on_path (!load_path) (fullpath s) in
 130     (Filename.basename s',Digest.file s');;
 131
 132 (* The dependency calculation in flyspeck_needs still has a bug if the
 133    file does not load correctly, but it calls another file that does load
 134    correctly.  It seems that the correctly loaded modules disappear from
 135    the scope when the error is encountered.  Thus, they should be
 136    filtered out as well from the depend statement.  For now, we offer
 137    depend_reset to clear the error.
 138 *)
 139
 140 let (flyspeck_needs,filetable,depend,depend_reset)  =
 141   let ftable = ref [("pervasives",List.length (constants()))] in
 142    (* associate constants with files *)
 143   let depend = ref ([]:((string*Digest.t)*(string*Digest.t)) list) in
 144    (* dependency table *)
 145   let host = ref (fileid "build.hl") in
 146   let fn = fun s->
 147   let id = fileid s in
 148     if (List.mem id (!loaded_files))
 149     then Format.print_string("File \""^s^"\" already loaded\n")
 150     else
 151       (
 152         if List.mem (!host,id) (!depend) then failwith "There may be circular needs.";
 153         depend := (!host,id)::(!depend);
 154         let h = !host in
 155         let _ = (host := id) in
 156         let b= needb (fullpath s) in
 157         let _ = (host := h) in
 158         let _ = try State_manager.neutralize_state () with
 159             Failure msg -> Format.print_string("File \""^s^
 160                  "\"corrupted neutral state.\n"^msg^"\n") in
 161           if b then (
 162             (ftable:= (s,List.length(constants()))::(!ftable));
 163             Format.print_string("File \""^s^"\" successfully loaded\n"))
 164           else (depend := filter ((<>) (h,id)) (!depend);
 165             failwith ("Aborting Flyspeck Needs "^s))
 166       ) in
 167     (fn,(fun () -> !ftable),(fun() -> !depend),(fun() -> (depend:=[])));;
 168
 169
 170
 171 (* disable "needs" for now *)
 172 (*
 173 let needs' = needs;;
 174 let needs _ = failwith "Use flyspeck_needs rather than needs";;
 175 *)
 176
 177 (* utilities *)
 178 flyspeck_needs "general/print_types.hl";;
 179 flyspeck_needs  "general/update_database_310.ml";;
 180 flyspeck_needs "general/prove_by_refinement.hl";;
 181 (* flyspeck_needs "general/flyspeck_utility.hl";; *)
 182 let dest_goal gl = gl;;
 183 let goal_asms = fst;;
 184 let goal_concl = snd;;
 185 let mk_goal(asl,w) = (asl,w);;
 186
 187 (* verbose error reporting *)
 188
 189
 190 let prove_by_refinement = Debug.verbose Prove_by_refinement.prove_by_refinement;;
 191 let prove = Debug.verbose prove;;
 192 let new_definition = Debug.verbose_1 new_definition;;
 193 let ABBREV_TAC = Debug.verbose_1 ABBREV_TAC;;
 194 let EXISTS_TAC = Debug.verbose_1 EXISTS_TAC;;
 195
 196 (* This next one gets iterated in FIRST_ASSUM and creates multiple error messages *)
 197 (* let ISPECL = Debug.verbose_thm ISPECL;; *)
 198
 199 flyspeck_needs "build.hl";;
 200
 201 let build_and_report() =
 202   let s = try
 203     (let _ = map flyspeck_needs Build.build_sequence in  "full load completed")
 204   with Failure t -> t  in
 205   let oc = open_out_gen [Open_append;Open_text] 436 (fullpath "log.txt") in
 206   (Pervasives.output_string oc (build_report s); close_out oc);;
 207
 208 let build_silent() =
 209   let s = try
 210     (let _ = map flyspeck_needs Build.build_sequence in  "full load completed")
 211   with Failure t ->  t  in
 212      build_report s;;
 213
 214 let try_do f  =
 215   let rec try_dof = function
 216       [] -> []
 217     | (x::t) ->
 218         try
 219           (let y = f x in y:: try_dof t)
 220         with Failure _ -> [] in
 221     try_dof;;
 222
 223 let already_loaded s =
 224   let s' = file_on_path (!load_path) s in
 225   let fileid = (Filename.basename s',Digest.file s') in
 226     List.mem fileid (!loaded_files);;
 227
 228 let new_build_silent() =
 229   let loaded = try_do (fun s -> flyspeck_needs s; s) Build.build_sequence in
 230   let unloaded = filter(not o already_loaded) Build.build_sequence in
 231     (loaded,unloaded);;
 232
 233 let rec cut_after f a acc = function
 234   | [] -> acc
 235   | b::bs -> if (f b =a) then (b::acc) else cut_after f a (b::acc) bs;;
 236
 237 let reset_after s =
 238   (loaded_files := cut_after fst s [] (List.rev (!loaded_files)));;
 239
 240 let reset () = (reset_after "hol_pervasives.hl"; depend_reset());;
 241
 242 (* let reset() = reset_after "flyspeck.ml";; *)
 243