1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Chapter: Build for all chapters *)
5 (* Author: Thomas C. Hales *)
7 (* ========================================================================== *)
11 Build file for Flyspeck project.
12 ocaml needs to be built with Unix.
13 ocamlmktop unix.cma str.cma nums.cma -o ocampl
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"
19 hol-light should already be loaded
27 needs "Multivariate/flyspeck.ml";;
28 needs "Rqe/num_calc_simp.ml";;
35 (try Sys.getenv "FLYSPECK_DIR" with Not_found -> Sys.getcwd());;
38 (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());;
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. *)
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);;
52 let load_date = process_to_string "date";;
55 the svn version does not reflect recent commits, unless followed by an update.
58 let flyspeck_version() = "Flyspeck "^
59 process_to_string ("svn info "^flyspeck_dir^ " | grep Revision");;
61 let hollight_version() = "HOL Light "^
62 process_to_string ("svnversion "^hollight_dir);;
64 let ocaml_version() = "Ocaml "^Sys.ocaml_version;;
66 let build_date() = "Build: " ^ process_to_string "date";;
67 let build_user() = "User: " ^ process_to_string "whoami";;
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";;
76 let fullpath s = Filename.concat flyspeck_dir s;;
80 Sys.command("svn info "^flyspeck_dir^" | grep Revison");;
85 (* boolean valued versions of Harrison's load files that return false
86 if load was not a success *)
89 if not(Sys.file_exists s)
90 then (report ("File not found "^s); false)
92 (Toploop.use_file Format.std_formatter s) or
93 (Format.print_string("Error in included file "^s);
94 Format.print_newline(); false);;
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));;
101 let loadb s = load_on_path_b (!load_path) 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)
111 loadt (fullpath "general/parser_verbose.hl");;
112 loadt (fullpath "general/debug.hl");;
113 Debug.set_verbose_parsing();;
116 (* limit changes in the state of the proof assistant *)
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";;
122 loadt (fullpath "general/state_manager.hl");;
123 let reneeds s = loadt (fullpath s);;
124 let rflyspeck_needs = reneeds;;
126 State_manager.neutralize_state();;
129 let s' = file_on_path (!load_path) (fullpath s) in
130 (Filename.basename s',Digest.file s');;
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.
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
148 if (List.mem id (!loaded_files))
149 then Format.print_string("File \""^s^"\" already loaded\n")
152 if List.mem (!host,id) (!depend) then failwith "There may be circular needs.";
153 depend := (!host,id)::(!depend);
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
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))
167 (fn,(fun () -> !ftable),(fun() -> !depend),(fun() -> (depend:=[])));;
171 (* disable "needs" for now *)
174 let needs _ = failwith "Use flyspeck_needs rather than needs";;
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);;
187 (* verbose error reporting *)
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;;
196 (* This next one gets iterated in FIRST_ASSUM and creates multiple error messages *)
197 (* let ISPECL = Debug.verbose_thm ISPECL;; *)
199 flyspeck_needs "build.hl";;
201 let build_and_report() =
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);;
210 (let _ = map flyspeck_needs Build.build_sequence in "full load completed")
211 with Failure t -> t in
215 let rec try_dof = function
219 (let y = f x in y:: try_dof t)
220 with Failure _ -> [] in
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);;
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
233 let rec cut_after f a acc = function
235 | b::bs -> if (f b =a) then (b::acc) else cut_after f a (b::acc) bs;;
238 (loaded_files := cut_after fst s [] (List.rev (!loaded_files)));;
240 let reset () = (reset_after "hol_pervasives.hl"; depend_reset());;
242 (* let reset() = reset_after "flyspeck.ml";; *)