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