1(* Title: Pure/Tools/build.ML 2 Author: Makarius 3 4Build Isabelle sessions. 5*) 6 7signature BUILD = 8sig 9 val build: string -> unit 10end; 11 12structure Build: BUILD = 13struct 14 15(* command timings *) 16 17type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name, time*) 18 19val empty_timings: timings = Symtab.empty; 20 21fun update_timings props = 22 (case Markup.parse_command_timing_properties props of 23 SOME ({file, offset, name}, time) => 24 Symtab.map_default (file, Inttab.empty) 25 (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time))) 26 | NONE => I); 27 28fun approximative_id name pos = 29 (case (Position.file_of pos, Position.offset_of pos) of 30 (SOME file, SOME offset) => 31 if name = "" then NONE else SOME {file = file, offset = offset, name = name} 32 | _ => NONE); 33 34fun get_timings timings tr = 35 (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of 36 SOME {file, offset, name} => 37 (case Symtab.lookup timings file of 38 SOME offsets => 39 (case Inttab.lookup offsets offset of 40 SOME (name', time) => if name = name' then SOME time else NONE 41 | NONE => NONE) 42 | NONE => NONE) 43 | NONE => NONE) 44 |> the_default Time.zeroTime; 45 46 47(* session timing *) 48 49fun session_timing name verbose f x = 50 let 51 val start = Timing.start (); 52 val y = f x; 53 val timing = Timing.result start; 54 55 val threads = string_of_int (Multithreading.max_threads ()); 56 val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) 57 |> Real.fmt (StringCvt.FIX (SOME 2)); 58 59 val timing_props = 60 [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)]; 61 val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props)); 62 val _ = 63 if verbose then 64 Output.physical_stderr ("Timing " ^ name ^ " (" ^ 65 threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n") 66 else (); 67 in y end; 68 69 70(* protocol messages *) 71 72fun protocol_message props output = 73 (case props of 74 function :: args => 75 if function = Markup.ML_statistics orelse function = Markup.task_statistics then 76 Protocol_Message.inline (#2 function) args 77 else if function = Markup.command_timing then 78 let 79 val name = the_default "" (Properties.get args Markup.nameN); 80 val pos = Position.of_properties args; 81 val {elapsed, ...} = Markup.parse_timing_properties args; 82 val is_significant = 83 Timing.is_relevant_time elapsed andalso 84 elapsed >= Options.default_seconds "command_timing_threshold"; 85 in 86 if is_significant then 87 (case approximative_id name pos of 88 SOME id => 89 Protocol_Message.inline (#2 function) (Markup.command_timing_properties id elapsed) 90 | NONE => ()) 91 else () 92 end 93 else if function = Markup.theory_timing then 94 Protocol_Message.inline (#2 function) args 95 else 96 (case Markup.dest_loading_theory props of 97 SOME name => writeln ("\floading_theory = " ^ name) 98 | NONE => Export.protocol_message props output) 99 | [] => raise Output.Protocol_Message props); 100 101 102(* build theories *) 103 104fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) = 105 let 106 val context = 107 {options = options, symbols = symbols, bibtex_entries = bibtex_entries, 108 last_timing = last_timing}; 109 val condition = space_explode "," (Options.string options "condition"); 110 val conds = filter_out (can getenv_strict) condition; 111 in 112 if null conds then 113 (Options.set_default options; 114 Isabelle_Process.init_options (); 115 Future.fork I; 116 (Thy_Info.use_theories context qualifier master_dir 117 |> 118 (case Options.string options "profiling" of 119 "" => I 120 | "time" => profile_time 121 | "allocations" => profile_allocations 122 | bad => error ("Bad profiling option: " ^ quote bad)) 123 |> Unsynchronized.setmp print_mode 124 (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys) 125 else 126 Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ 127 " (undefined " ^ commas conds ^ ")\n") 128 end; 129 130 131(* build session *) 132 133datatype args = Args of 134 {symbol_codes: (string * int) list, 135 command_timings: Properties.T list, 136 do_output: bool, 137 verbose: bool, 138 browser_info: Path.T, 139 document_files: (Path.T * Path.T) list, 140 graph_file: Path.T, 141 parent_name: string, 142 chapter: string, 143 name: string, 144 master_dir: Path.T, 145 theories: (Options.T * (string * Position.T) list) list, 146 session_positions: (string * Properties.T) list, 147 session_directories: (string * string) list, 148 doc_names: string list, 149 global_theories: (string * string) list, 150 loaded_theories: string list, 151 bibtex_entries: string list}; 152 153fun decode_args yxml = 154 let 155 open XML.Decode; 156 val position = Position.of_properties o properties; 157 val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info, 158 (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir, 159 (theories, (session_positions, (session_directories, (doc_names, (global_theories, 160 (loaded_theories, bibtex_entries))))))))))))))))) = 161 pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string 162 (pair (list (pair string string)) (pair string (pair string (pair string (pair string 163 (pair string 164 (pair (((list (pair Options.decode (list (pair string position)))))) 165 (pair (list (pair string properties)) 166 (pair (list (pair string string)) (pair (list string) 167 (pair (list (pair string string)) (pair (list string) (list string))))))))))))))))) 168 (YXML.parse_body yxml); 169 in 170 Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output, 171 verbose = verbose, browser_info = Path.explode browser_info, 172 document_files = map (apply2 Path.explode) document_files, 173 graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter, 174 name = name, master_dir = Path.explode master_dir, theories = theories, 175 session_positions = session_positions, session_directories = session_directories, 176 doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories, 177 bibtex_entries = bibtex_entries} 178 end; 179 180fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info, 181 document_files, graph_file, parent_name, chapter, name, master_dir, theories, session_positions, 182 session_directories, doc_names, global_theories, loaded_theories, bibtex_entries}) = 183 let 184 val symbols = HTML.make_symbols symbol_codes; 185 186 val _ = 187 Resources.init_session_base 188 {session_positions = session_positions, 189 session_directories = session_directories, 190 docs = doc_names, 191 global_theories = global_theories, 192 loaded_theories = loaded_theories}; 193 194 val _ = 195 Session.init 196 symbols 197 do_output 198 (Options.default_bool "browser_info") 199 browser_info 200 (Options.default_string "document") 201 (Options.default_string "document_output") 202 (Present.document_variants (Options.default ())) 203 document_files 204 graph_file 205 parent_name 206 (chapter, name) 207 verbose; 208 209 val last_timing = get_timings (fold update_timings command_timings empty_timings); 210 211 val res1 = 212 theories |> 213 (List.app (build_theories symbols bibtex_entries last_timing name master_dir) 214 |> session_timing name verbose 215 |> Exn.capture); 216 val res2 = Exn.capture Session.finish (); 217 218 val _ = Resources.finish_session_base (); 219 val _ = Par_Exn.release_all [res1, res2]; 220 in () end; 221 222(*command-line tool*) 223fun build args_file = 224 let 225 val _ = SHA1.test_samples (); 226 val _ = Options.load_default (); 227 val _ = Isabelle_Process.init_options (); 228 val args = decode_args (File.read (Path.explode args_file)); 229 fun error_message msg = writeln ("\ferror_message = " ^ encode_lines (YXML.content_of msg)); 230 val _ = 231 Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message 232 build_session args 233 handle exn => (List.app error_message (Runtime.exn_message_list exn); Exn.reraise exn); 234 val _ = Private_Output.protocol_message_fn := Output.protocol_message_undefined; 235 val _ = Options.reset_default (); 236 in () end; 237 238(*PIDE version*) 239val _ = 240 Isabelle_Process.protocol_command "build_session" 241 (fn [args_yxml] => 242 let 243 val args = decode_args args_yxml; 244 val result = (build_session args; "") handle exn => 245 (Runtime.exn_message exn handle _ (*sic!*) => 246 "Exception raised, but failed to print details!"); 247 in Output.protocol_message Markup.build_session_finished [XML.Text result] end 248 | _ => raise Match); 249 250end; 251