src/Pure/Tools/build.ML
author wenzelm
Tue Jan 23 19:25:39 2018 +0100 (22 months ago ago)
changeset 67493 c4e9e0c50487
parent 67472 bddfa23a4ea9
child 68090 0763d4eb3ebc
permissions -rw-r--r--
treat sessions as entities with defining position;
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 bibtex_entries 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           bibtex_entries = bibtex_entries,
   120           last_timing = last_timing,
   121           qualifier = qualifier,
   122           master_dir = master_dir}
   123         |>
   124           (case Options.string options "profiling" of
   125             "" => I
   126           | "time" => profile_time
   127           | "allocations" => profile_allocations
   128           | bad => error ("Bad profiling option: " ^ quote bad))
   129         |> Unsynchronized.setmp print_mode
   130             (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
   131     else
   132       Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
   133         " (undefined " ^ commas conds ^ ")\n")
   134   end;
   135 
   136 
   137 (* build session *)
   138 
   139 datatype args = Args of
   140  {symbol_codes: (string * int) list,
   141   command_timings: Properties.T list,
   142   do_output: bool,
   143   verbose: bool,
   144   browser_info: Path.T,
   145   document_files: (Path.T * Path.T) list,
   146   graph_file: Path.T,
   147   parent_name: string,
   148   chapter: string,
   149   name: string,
   150   master_dir: Path.T,
   151   theories: (Options.T * (string * Position.T) list) list,
   152   sessions: (string * Properties.T) list,
   153   doc_names: string list,
   154   global_theories: (string * string) list,
   155   loaded_theories: string list,
   156   known_theories: (string * string) list,
   157   bibtex_entries: string list};
   158 
   159 fun decode_args yxml =
   160   let
   161     open XML.Decode;
   162     val position = Position.of_properties o properties;
   163     val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
   164       (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
   165       (theories, (sessions, (doc_names, (global_theories, (loaded_theories,
   166       (known_theories, bibtex_entries))))))))))))))))) =
   167       pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
   168         (pair (list (pair string string)) (pair string (pair string (pair string (pair string
   169           (pair string
   170             (pair (((list (pair Options.decode (list (pair string position))))))
   171               (pair (list (pair string properties)) (pair (list string)
   172                 (pair (list (pair string string)) (pair (list string)
   173                   (pair (list (pair string string)) (list string)))))))))))))))))
   174       (YXML.parse_body yxml);
   175   in
   176     Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
   177       verbose = verbose, browser_info = Path.explode browser_info,
   178       document_files = map (apply2 Path.explode) document_files,
   179       graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
   180       name = name, master_dir = Path.explode master_dir, theories = theories, sessions = sessions,
   181       doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories,
   182       known_theories = known_theories, bibtex_entries = bibtex_entries}
   183   end;
   184 
   185 fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
   186     document_files, graph_file, parent_name, chapter, name, master_dir, theories, sessions,
   187     doc_names, global_theories, loaded_theories, known_theories, bibtex_entries}) =
   188   let
   189     val symbols = HTML.make_symbols symbol_codes;
   190 
   191     val _ =
   192       Resources.init_session_base
   193         {sessions = sessions,
   194          docs = doc_names,
   195          global_theories = global_theories,
   196          loaded_theories = loaded_theories,
   197          known_theories = known_theories};
   198 
   199     val _ =
   200       Session.init
   201         symbols
   202         do_output
   203         (Options.default_bool "browser_info")
   204         browser_info
   205         (Options.default_string "document")
   206         (Options.default_string "document_output")
   207         (Present.document_variants (Options.default_string "document_variants"))
   208         document_files
   209         graph_file
   210         parent_name
   211         (chapter, name)
   212         verbose;
   213 
   214     val last_timing = get_timings (fold update_timings command_timings empty_timings);
   215 
   216     val res1 =
   217       theories |>
   218         (List.app (build_theories symbols bibtex_entries last_timing name master_dir)
   219           |> session_timing name verbose
   220           |> Exn.capture);
   221     val res2 = Exn.capture Session.finish ();
   222 
   223     val _ = Resources.finish_session_base ();
   224     val _ = Par_Exn.release_all [res1, res2];
   225   in () end;
   226 
   227 (*command-line tool*)
   228 fun build args_file =
   229   let
   230     val _ = SHA1.test_samples ();
   231     val _ = Options.load_default ();
   232     val _ = Isabelle_Process.init_options ();
   233     val args = decode_args (File.read (Path.explode args_file));
   234     fun error_message msg = writeln ("\ferror_message = " ^ encode_lines (YXML.content_of msg));
   235     val _ =
   236       Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
   237         build_session args
   238       handle exn => (List.app error_message (Runtime.exn_message_list exn); Exn.reraise exn);
   239     val _ = Options.reset_default ();
   240   in () end;
   241 
   242 (*PIDE version*)
   243 val _ =
   244   Isabelle_Process.protocol_command "build_session"
   245     (fn [args_yxml] =>
   246       let
   247         val args = decode_args args_yxml;
   248         val result = (build_session args; "") handle exn =>
   249           (Runtime.exn_message exn handle _ (*sic!*) =>
   250             "Exception raised, but failed to print details!");
   251     in Output.protocol_message Markup.build_session_finished [result] end | _ => raise Match);
   252 
   253 end;