src/Pure/Tools/build.ML
author wenzelm
Sat May 05 22:33:35 2018 +0200 (18 months ago ago)
changeset 68090 0763d4eb3ebc
parent 67493 c4e9e0c50487
child 68148 fb661e4c4717
permissions -rw-r--r--
protocol message for export of theory resources;
     1 (*  Title:      Pure/Tools/build.ML
     2     Author:     Makarius
     3 
     4 Build Isabelle sessions.
     5 *)
     6 
     7 signature BUILD =
     8 sig
     9   val build: string -> unit
    10 end;
    11 
    12 structure Build: BUILD =
    13 struct
    14 
    15 (* command timings *)
    16 
    17 type timings = ((string * Time.time) Inttab.table) Symtab.table;  (*file -> offset -> name, time*)
    18 
    19 val empty_timings: timings = Symtab.empty;
    20 
    21 fun 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 
    28 fun 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 
    34 fun 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 
    49 fun 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 
    72 fun inline_message a args =
    73   writeln ("\f" ^ a ^ " = " ^ YXML.string_of_body (XML.Encode.properties args));
    74 
    75 fun protocol_message props output =
    76   (case props of
    77     function :: args =>
    78       if function = Markup.ML_statistics orelse function = Markup.task_statistics then
    79         inline_message (#2 function) args
    80       else if function = Markup.command_timing then
    81         let
    82           val name = the_default "" (Properties.get args Markup.nameN);
    83           val pos = Position.of_properties args;
    84           val {elapsed, ...} = Markup.parse_timing_properties args;
    85           val is_significant =
    86             Timing.is_relevant_time elapsed andalso
    87             elapsed >= Options.default_seconds "command_timing_threshold";
    88         in
    89           if is_significant then
    90             (case approximative_id name pos of
    91               SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed)
    92             | NONE => ())
    93           else ()
    94         end
    95       else if function = Markup.theory_timing then
    96         inline_message (#2 function) args
    97       else if function = (Markup.functionN, Markup.exportN) andalso
    98         not (null args) andalso #1 (hd args) = Markup.idN
    99       then
   100         inline_message (#2 function) (tl args @ [(Markup.exportN, hex_string (implode output))])
   101       else
   102         (case Markup.dest_loading_theory props of
   103           SOME name => writeln ("\floading_theory = " ^ name)
   104         | NONE => raise Output.Protocol_Message props)
   105   | [] => raise Output.Protocol_Message props);
   106 
   107 
   108 (* build theories *)
   109 
   110 fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) =
   111   let
   112     val condition = space_explode "," (Options.string options "condition");
   113     val conds = filter_out (can getenv_strict) condition;
   114   in
   115     if null conds then
   116       (if Options.bool options "checkpoint" then ML_Heap.share_common_data () else ();
   117         Options.set_default options;
   118         Isabelle_Process.init_options ();
   119         Future.fork I;
   120         (Thy_Info.use_theories {
   121           document = Present.document_enabled (Options.string options "document"),
   122           symbols = symbols,
   123           bibtex_entries = bibtex_entries,
   124           last_timing = last_timing,
   125           qualifier = qualifier,
   126           master_dir = master_dir}
   127         |>
   128           (case Options.string options "profiling" of
   129             "" => I
   130           | "time" => profile_time
   131           | "allocations" => profile_allocations
   132           | bad => error ("Bad profiling option: " ^ quote bad))
   133         |> Unsynchronized.setmp print_mode
   134             (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
   135     else
   136       Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
   137         " (undefined " ^ commas conds ^ ")\n")
   138   end;
   139 
   140 
   141 (* build session *)
   142 
   143 datatype args = Args of
   144  {symbol_codes: (string * int) list,
   145   command_timings: Properties.T list,
   146   do_output: bool,
   147   verbose: bool,
   148   browser_info: Path.T,
   149   document_files: (Path.T * Path.T) list,
   150   graph_file: Path.T,
   151   parent_name: string,
   152   chapter: string,
   153   name: string,
   154   master_dir: Path.T,
   155   theories: (Options.T * (string * Position.T) list) list,
   156   sessions: (string * Properties.T) list,
   157   doc_names: string list,
   158   global_theories: (string * string) list,
   159   loaded_theories: string list,
   160   known_theories: (string * string) list,
   161   bibtex_entries: string list};
   162 
   163 fun decode_args yxml =
   164   let
   165     open XML.Decode;
   166     val position = Position.of_properties o properties;
   167     val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
   168       (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
   169       (theories, (sessions, (doc_names, (global_theories, (loaded_theories,
   170       (known_theories, bibtex_entries))))))))))))))))) =
   171       pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
   172         (pair (list (pair string string)) (pair string (pair string (pair string (pair string
   173           (pair string
   174             (pair (((list (pair Options.decode (list (pair string position))))))
   175               (pair (list (pair string properties)) (pair (list string)
   176                 (pair (list (pair string string)) (pair (list string)
   177                   (pair (list (pair string string)) (list string)))))))))))))))))
   178       (YXML.parse_body yxml);
   179   in
   180     Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
   181       verbose = verbose, browser_info = Path.explode browser_info,
   182       document_files = map (apply2 Path.explode) document_files,
   183       graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
   184       name = name, master_dir = Path.explode master_dir, theories = theories, sessions = sessions,
   185       doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories,
   186       known_theories = known_theories, bibtex_entries = bibtex_entries}
   187   end;
   188 
   189 fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
   190     document_files, graph_file, parent_name, chapter, name, master_dir, theories, sessions,
   191     doc_names, global_theories, loaded_theories, known_theories, bibtex_entries}) =
   192   let
   193     val symbols = HTML.make_symbols symbol_codes;
   194 
   195     val _ =
   196       Resources.init_session_base
   197         {sessions = sessions,
   198          docs = doc_names,
   199          global_theories = global_theories,
   200          loaded_theories = loaded_theories,
   201          known_theories = known_theories};
   202 
   203     val _ =
   204       Session.init
   205         symbols
   206         do_output
   207         (Options.default_bool "browser_info")
   208         browser_info
   209         (Options.default_string "document")
   210         (Options.default_string "document_output")
   211         (Present.document_variants (Options.default_string "document_variants"))
   212         document_files
   213         graph_file
   214         parent_name
   215         (chapter, name)
   216         verbose;
   217 
   218     val last_timing = get_timings (fold update_timings command_timings empty_timings);
   219 
   220     val res1 =
   221       theories |>
   222         (List.app (build_theories symbols bibtex_entries last_timing name master_dir)
   223           |> session_timing name verbose
   224           |> Exn.capture);
   225     val res2 = Exn.capture Session.finish ();
   226 
   227     val _ = Resources.finish_session_base ();
   228     val _ = Par_Exn.release_all [res1, res2];
   229   in () end;
   230 
   231 (*command-line tool*)
   232 fun build args_file =
   233   let
   234     val _ = SHA1.test_samples ();
   235     val _ = Options.load_default ();
   236     val _ = Isabelle_Process.init_options ();
   237     val args = decode_args (File.read (Path.explode args_file));
   238     fun error_message msg = writeln ("\ferror_message = " ^ encode_lines (YXML.content_of msg));
   239     val _ =
   240       Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
   241         build_session args
   242       handle exn => (List.app error_message (Runtime.exn_message_list exn); Exn.reraise exn);
   243     val _ = Options.reset_default ();
   244   in () end;
   245 
   246 (*PIDE version*)
   247 val _ =
   248   Isabelle_Process.protocol_command "build_session"
   249     (fn [args_yxml] =>
   250       let
   251         val args = decode_args args_yxml;
   252         val result = (build_session args; "") handle exn =>
   253           (Runtime.exn_message exn handle _ (*sic!*) =>
   254             "Exception raised, but failed to print details!");
   255     in Output.protocol_message Markup.build_session_finished [result] end | _ => raise Match);
   256 
   257 end;