src/Pure/Tools/build.ML
author wenzelm
Sun May 24 14:47:28 2020 +0200 (2 months ago)
changeset 71880 0ca353521753
parent 71879 fe7ee970c425
child 71884 2bf0283fc975
permissions -rw-r--r--
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
     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 session_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 _ = Protocol_Message.marker "Timing" timing_props;
    62     val _ =
    63       if verbose then
    64         Output.physical_stderr ("Timing " ^ session_name ^ " (" ^
    65           threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n")
    66       else ();
    67   in y end;
    68 
    69 
    70 (* protocol messages *)
    71 
    72 fun 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.marker (#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.marker (#2 function)
    90                   (Markup.command_timing_properties id elapsed)
    91             | NONE => ())
    92           else ()
    93         end
    94       else if function = Markup.theory_timing then
    95         Protocol_Message.marker (#2 function) args
    96       else
    97         (case Markup.dest_loading_theory props of
    98           SOME name => Protocol_Message.marker_text "loading_theory" name
    99         | NONE => Export.protocol_message props output)
   100   | [] => raise Output.Protocol_Message props);
   101 
   102 
   103 (* build theories *)
   104 
   105 fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) =
   106   let
   107     val context =
   108       {options = options, symbols = symbols, bibtex_entries = bibtex_entries,
   109         last_timing = last_timing};
   110     val condition = space_explode "," (Options.string options "condition");
   111     val conds = filter_out (can getenv_strict) condition;
   112   in
   113     if null conds then
   114       (Options.set_default options;
   115         Isabelle_Process.init_options ();
   116         Future.fork I;
   117         (Thy_Info.use_theories context qualifier master_dir
   118         |>
   119           (case Options.string options "profiling" of
   120             "" => I
   121           | "time" => profile_time
   122           | "allocations" => profile_allocations
   123           | bad => error ("Bad profiling option: " ^ quote bad))
   124         |> Unsynchronized.setmp print_mode
   125             (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
   126     else
   127       Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
   128         " (undefined " ^ commas conds ^ ")\n")
   129   end;
   130 
   131 
   132 (* build session *)
   133 
   134 datatype args = Args of
   135  {pide: bool,
   136   symbol_codes: (string * int) list,
   137   command_timings: Properties.T list,
   138   verbose: bool,
   139   browser_info: Path.T,
   140   document_files: (Path.T * Path.T) list,
   141   graph_file: Path.T,
   142   parent_name: string,
   143   chapter: string,
   144   session_name: string,
   145   master_dir: Path.T,
   146   theories: (Options.T * (string * Position.T) list) list,
   147   session_positions: (string * Properties.T) list,
   148   session_directories: (string * string) list,
   149   doc_names: string list,
   150   global_theories: (string * string) list,
   151   loaded_theories: string list,
   152   bibtex_entries: string list};
   153 
   154 fun decode_args pide yxml =
   155   let
   156     open XML.Decode;
   157     val position = Position.of_properties o properties;
   158     val (symbol_codes, (command_timings, (verbose, (browser_info,
   159       (document_files, (graph_file, (parent_name, (chapter, (session_name, (master_dir,
   160       (theories, (session_positions, (session_directories, (doc_names, (global_theories,
   161       (loaded_theories, bibtex_entries)))))))))))))))) =
   162       pair (list (pair string int)) (pair (list properties) (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 properties))
   167                 (pair (list (pair string string)) (pair (list string)
   168                   (pair (list (pair string string)) (pair (list string) (list string))))))))))))))))
   169       (YXML.parse_body yxml);
   170   in
   171     Args {pide = pide, symbol_codes = symbol_codes, command_timings = command_timings,
   172       verbose = verbose, browser_info = Path.explode browser_info,
   173       document_files = map (apply2 Path.explode) document_files,
   174       graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
   175       session_name = session_name, master_dir = Path.explode master_dir, theories = theories,
   176       session_positions = session_positions, session_directories = session_directories,
   177       doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories,
   178       bibtex_entries = bibtex_entries}
   179   end;
   180 
   181 fun build_session (Args {pide, symbol_codes, command_timings, verbose, browser_info, document_files,
   182     graph_file, parent_name, chapter, session_name, master_dir, theories, session_positions,
   183     session_directories, doc_names, global_theories, loaded_theories, bibtex_entries}) =
   184   let
   185     val symbols = HTML.make_symbols symbol_codes;
   186 
   187     val _ =
   188       Resources.init_session
   189         {pide = pide,
   190          session_positions = session_positions,
   191          session_directories = session_directories,
   192          docs = doc_names,
   193          global_theories = global_theories,
   194          loaded_theories = loaded_theories};
   195 
   196     val _ =
   197       Session.init
   198         symbols
   199         (Options.default_bool "browser_info")
   200         browser_info
   201         (Options.default_string "document")
   202         (Options.default_string "document_output")
   203         (Present.document_variants (Options.default ()))
   204         document_files
   205         graph_file
   206         parent_name
   207         (chapter, session_name)
   208         verbose;
   209 
   210     val last_timing = get_timings (fold update_timings command_timings empty_timings);
   211 
   212     val res1 =
   213       theories |>
   214         (List.app (build_theories symbols bibtex_entries last_timing session_name master_dir)
   215           |> session_timing session_name verbose
   216           |> Exn.capture);
   217     val res2 = Exn.capture Session.finish ();
   218 
   219     val _ = Resources.finish_session_base ();
   220     val _ = Par_Exn.release_all [res1, res2];
   221     val _ =
   222       if session_name = Context.PureN
   223       then Theory.install_pure (Thy_Info.get_theory Context.PureN) else ();
   224   in () end;
   225 
   226 
   227 (* command-line tool *)
   228 
   229 fun inline_errors exn =
   230   Runtime.exn_message_list exn
   231   |> List.app (fn msg => Protocol_Message.marker_text "error_message" (YXML.content_of msg));
   232 
   233 fun build args_file =
   234   let
   235     val _ = SHA1.test_samples ();
   236     val _ = Options.load_default ();
   237     val _ = Isabelle_Process.init_options ();
   238     val args = decode_args false (File.read (Path.explode args_file));
   239     val _ =
   240       Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
   241         build_session args
   242       handle exn => (inline_errors exn; Exn.reraise exn);
   243     val _ = Private_Output.protocol_message_fn := Output.protocol_message_undefined;
   244     val _ = Options.reset_default ();
   245   in () end;
   246 
   247 
   248 (* PIDE version *)
   249 
   250 val _ =
   251   Isabelle_Process.protocol_command "build_session"
   252     (fn [args_yxml] =>
   253         let
   254           val args = decode_args true args_yxml;
   255           fun exec e =
   256             if can Theory.get_pure () then
   257               Isabelle_Thread.fork
   258                 {name = "build_session", stack_limit = NONE, interrupts = false} e
   259               |> ignore
   260             else e ();
   261         in
   262           exec (fn () =>
   263             (Future.interruptible_task (fn () => (build_session args; (0, []))) () handle exn =>
   264               ((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"])))
   265           |> let open XML.Encode in pair int (list string) end
   266           |> Output.protocol_message Markup.build_session_finished)
   267         end
   268       | _ => raise Match);
   269 
   270 end;