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