src/Pure/Tools/build.ML
author wenzelm
Sat Mar 26 13:41:14 2016 +0100 (2016-03-26)
changeset 62713 c18a68a3a1f1
parent 62666 00aff1da05ae
child 62714 63888e5f668b
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, Time.+ (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 lookup_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 
    45 
    46 (* session timing *)
    47 
    48 fun session_timing name verbose f x =
    49   let
    50     val start = Timing.start ();
    51     val y = f x;
    52     val timing = Timing.result start;
    53 
    54     val threads = string_of_int (Multithreading.max_threads_value ());
    55     val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
    56       |> Real.fmt (StringCvt.FIX (SOME 2));
    57 
    58     val timing_props =
    59       [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)];
    60     val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props));
    61     val _ =
    62       if verbose then
    63         Output.physical_stderr ("Timing " ^ name ^ " (" ^
    64           threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n")
    65       else ();
    66   in y end;
    67 
    68 
    69 (* protocol messages *)
    70 
    71 fun inline_message a args =
    72   writeln ("\f" ^ a ^ " = " ^ YXML.string_of_body (XML.Encode.properties args));
    73 
    74 fun protocol_message props output =
    75   (case props of
    76     function :: args =>
    77       if function = Markup.ML_statistics orelse function = Markup.task_statistics then
    78         inline_message (#2 function) args
    79       else if function = Markup.command_timing then
    80         let
    81           val name = the_default "" (Properties.get args Markup.nameN);
    82           val pos = Position.of_properties args;
    83           val {elapsed, ...} = Markup.parse_timing_properties args;
    84         in
    85           if Timing.is_relevant_time elapsed then
    86             (case approximative_id name pos of
    87               SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed)
    88             | NONE => ())
    89           else ()
    90         end
    91       else
    92         (case Markup.dest_loading_theory props of
    93           SOME name => writeln ("\floading_theory = " ^ name)
    94         | NONE => raise Output.Protocol_Message props)
    95   | [] => raise Output.Protocol_Message props);
    96 
    97 
    98 (* build *)
    99 
   100 fun build_theories symbols last_timing master_dir (options, thys) =
   101   let
   102     val condition = space_explode "," (Options.string options "condition");
   103     val conds = filter_out (can getenv_strict) condition;
   104   in
   105     if null conds then
   106       (Options.set_default options;
   107         (Thy_Info.use_theories {
   108           document = Present.document_enabled (Options.string options "document"),
   109           symbols = symbols,
   110           last_timing = last_timing,
   111           master_dir = master_dir}
   112         |> Unsynchronized.setmp print_mode
   113             (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
   114         |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
   115         |> Multithreading.max_threads_setmp (Options.int options "threads")
   116         |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
   117         |> Unsynchronized.setmp Future.ML_statistics true) thys)
   118     else
   119       Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
   120         " (undefined " ^ commas conds ^ ")\n")
   121   end;
   122 
   123 fun build args_file =
   124   let
   125     val _ = SHA1.test_samples ();
   126 
   127     val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
   128           (document_files, (graph_file, (parent_name, (chapter, (name, theories)))))))))) =
   129       File.read (Path.explode args_file) |> YXML.parse_body |>
   130         let open XML.Decode in
   131           pair (list (pair string int)) (pair (list properties) (pair bool
   132             (pair bool (pair string (pair (list (pair string string)) (pair string
   133               (pair string (pair string (pair string
   134               ((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))
   135         end;
   136 
   137     val symbols = HTML.make_symbols symbol_codes;
   138     val _ = Options.load_default ();
   139     val _ = Isabelle_Process.init_options ();
   140 
   141     val _ = writeln ("\fSession.name = " ^ name);
   142     val _ =
   143       Session.init
   144         symbols
   145         do_output
   146         (Options.default_bool "browser_info")
   147         (Path.explode browser_info)
   148         (Options.default_string "document")
   149         (Options.default_string "document_output")
   150         (Present.document_variants (Options.default_string "document_variants"))
   151         (map (apply2 Path.explode) document_files)
   152         (Path.explode graph_file)
   153         parent_name (chapter, name)
   154         verbose;
   155 
   156     val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
   157 
   158     val res1 =
   159       theories |>
   160         (List.app (build_theories symbols last_timing Path.current)
   161           |> session_timing name verbose
   162           |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
   163           |> Multithreading.max_threads_setmp (Options.default_int "threads")
   164           |> Exn.capture);
   165     val res2 = Exn.capture Session.finish ();
   166     val _ = Par_Exn.release_all [res1, res2];
   167 
   168     val _ = Options.reset_default ();
   169   in () end;
   170 
   171 
   172 (* PIDE protocol *)
   173 
   174 val _ =
   175   Isabelle_Process.protocol_command "build_theories"
   176     (fn [id, symbol_codes_yxml, master_dir, theories_yxml] =>
   177       let
   178         val symbols =
   179           YXML.parse_body symbol_codes_yxml
   180           |> let open XML.Decode in list (pair string int) end
   181           |> HTML.make_symbols;
   182         val theories =
   183           YXML.parse_body theories_yxml |>
   184             let open XML.Decode
   185             in list (pair Options.decode (list (string #> rpair Position.none))) end;
   186         val res1 =
   187           Exn.capture (fn () =>
   188             theories |> List.app (build_theories symbols (K NONE) (Path.explode master_dir))) ();
   189         val res2 = Exn.capture Session.shutdown ();
   190         val result =
   191           (Par_Exn.release_all [res1, res2]; "") handle exn =>
   192             (Runtime.exn_message exn handle _ (*sic!*) =>
   193               "Exception raised, but failed to print details!");
   194     in Output.protocol_message (Markup.build_theories_result id) [result] end);
   195 
   196 end;