src/Pure/Tools/build.ML
author wenzelm
Fri Apr 21 14:09:03 2017 +0200 (2017-04-21 ago)
changeset 65532 febfd9f78bd4
parent 65517 1544e61e5314
child 65934 5f202ba9f590
permissions -rw-r--r--
eliminated default_qualifier: just a constant;
     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
    96         (case Markup.dest_loading_theory props of
    97           SOME name => writeln ("\floading_theory = " ^ name)
    98         | NONE => raise Output.Protocol_Message props)
    99   | [] => raise Output.Protocol_Message props);
   100 
   101 
   102 (* build theories *)
   103 
   104 fun build_theories symbols last_timing qualifier master_dir (options, thys) =
   105   let
   106     val condition = space_explode "," (Options.string options "condition");
   107     val conds = filter_out (can getenv_strict) condition;
   108   in
   109     if null conds then
   110       (if Options.bool options "checkpoint" then ML_Heap.share_common_data () else ();
   111         Options.set_default options;
   112         Isabelle_Process.init_options ();
   113         Future.fork I;
   114         (Thy_Info.use_theories {
   115           document = Present.document_enabled (Options.string options "document"),
   116           symbols = symbols,
   117           last_timing = last_timing,
   118           qualifier = qualifier,
   119           master_dir = master_dir}
   120         |>
   121           (case Options.string options "profiling" of
   122             "" => I
   123           | "time" => profile_time
   124           | "allocations" => profile_allocations
   125           | bad => error ("Bad profiling option: " ^ quote bad))
   126         |> Unsynchronized.setmp print_mode
   127             (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
   128     else
   129       Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
   130         " (undefined " ^ commas conds ^ ")\n")
   131   end;
   132 
   133 
   134 (* build session *)
   135 
   136 datatype args = Args of
   137  {symbol_codes: (string * int) list,
   138   command_timings: Properties.T list,
   139   do_output: bool,
   140   verbose: bool,
   141   browser_info: Path.T,
   142   document_files: (Path.T * Path.T) list,
   143   graph_file: Path.T,
   144   parent_name: string,
   145   chapter: string,
   146   name: string,
   147   master_dir: Path.T,
   148   theories: (Options.T * (string * Position.T) list) list,
   149   global_theories: (string * string) list,
   150   loaded_theories: (string * string) list,
   151   known_theories: (string * string) list};
   152 
   153 fun 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, (global_theories, (loaded_theories, known_theories)))))))))))))) =
   160       pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
   161         (pair (list (pair string string)) (pair string (pair string (pair string (pair string
   162           (pair string
   163             (pair (((list (pair Options.decode (list (pair string position))))))
   164               (pair (list (pair string string))
   165                 (pair (list (pair string string)) (list (pair string string)))))))))))))))
   166       (YXML.parse_body yxml);
   167   in
   168     Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
   169       verbose = verbose, browser_info = Path.explode browser_info,
   170       document_files = map (apply2 Path.explode) document_files,
   171       graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
   172       name = name, master_dir = Path.explode master_dir, theories = theories,
   173       global_theories = global_theories, loaded_theories = loaded_theories,
   174       known_theories = known_theories}
   175   end;
   176 
   177 fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
   178     document_files, graph_file, parent_name, chapter, name, master_dir, theories,
   179     global_theories, loaded_theories, known_theories}) =
   180   let
   181     val symbols = HTML.make_symbols symbol_codes;
   182 
   183     val _ =
   184       Resources.init_session_base
   185         {global_theories = global_theories,
   186          loaded_theories = loaded_theories,
   187          known_theories = known_theories};
   188 
   189     val _ =
   190       Session.init
   191         symbols
   192         do_output
   193         (Options.default_bool "browser_info")
   194         browser_info
   195         (Options.default_string "document")
   196         (Options.default_string "document_output")
   197         (Present.document_variants (Options.default_string "document_variants"))
   198         document_files
   199         graph_file
   200         parent_name
   201         (chapter, name)
   202         verbose;
   203 
   204     val last_timing = get_timings (fold update_timings command_timings empty_timings);
   205 
   206     val res1 =
   207       theories |>
   208         (List.app (build_theories symbols last_timing name master_dir)
   209           |> session_timing name verbose
   210           |> Exn.capture);
   211     val res2 = Exn.capture Session.finish ();
   212 
   213     val _ = Resources.finish_session_base ();
   214     val _ = Par_Exn.release_all [res1, res2];
   215   in () end;
   216 
   217 (*command-line tool*)
   218 fun build args_file =
   219   let
   220     val _ = SHA1.test_samples ();
   221     val _ = Options.load_default ();
   222     val _ = Isabelle_Process.init_options ();
   223     val args = decode_args (File.read (Path.explode args_file));
   224     val _ =
   225       Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
   226         build_session args;
   227     val _ = Options.reset_default ();
   228   in () end;
   229 
   230 (*PIDE version*)
   231 val _ =
   232   Isabelle_Process.protocol_command "build_session"
   233     (fn [args_yxml] =>
   234       let
   235         val args = decode_args args_yxml;
   236         val result = (build_session args; "") handle exn =>
   237           (Runtime.exn_message exn handle _ (*sic!*) =>
   238             "Exception raised, but failed to print details!");
   239     in Output.protocol_message Markup.build_session_finished [result] end | _ => raise Match);
   240 
   241 end;