src/Pure/Tools/build.ML
author wenzelm
Wed Jan 14 16:27:19 2015 +0100 (2015-01-14 ago)
changeset 59366 e94df7f6b608
parent 59364 3b5da177ae6b
child 59368 100db5cf5be5
permissions -rw-r--r--
clarified build_theories: proper protocol handler;
     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 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           last_timing = last_timing,
   110           master_dir = master_dir}
   111         |> Unsynchronized.setmp print_mode
   112             (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
   113         |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
   114         |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
   115         |> Multithreading.max_threads_setmp (Options.int options "threads")
   116         |> Unsynchronized.setmp Future.ML_statistics true) thys)
   117     else
   118       Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
   119         " (undefined " ^ commas conds ^ ")\n")
   120   end;
   121 
   122 fun build args_file = Command_Line.tool0 (fn () =>
   123     let
   124       val _ = SHA1_Samples.test ();
   125 
   126       val (command_timings, (do_output, (options, (verbose, (browser_info,
   127           (document_files, (parent_name, (chapter, (name, theories))))))))) =
   128         File.read (Path.explode args_file) |> YXML.parse_body |>
   129           let open XML.Decode in
   130             pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
   131               (pair (list (pair string string)) (pair string (pair string (pair string
   132                 ((list (pair Options.decode (list (string #> rpair Position.none)))))))))))))
   133           end;
   134 
   135       val _ = Options.set_default options;
   136 
   137       val _ = writeln ("\fSession.name = " ^ name);
   138       val _ =
   139         Session.init do_output
   140           (Options.bool options "browser_info")
   141           (Path.explode browser_info)
   142           (Options.string options "document")
   143           (Options.bool options "document_graph")
   144           (Options.string options "document_output")
   145           (Present.document_variants (Options.string options "document_variants"))
   146           (map (apply2 Path.explode) document_files)
   147           parent_name (chapter, name)
   148           verbose;
   149 
   150       val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
   151 
   152       val res1 =
   153         theories |>
   154           (List.app (build_theories last_timing Path.current)
   155             |> session_timing name verbose
   156             |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
   157             |> Multithreading.max_threads_setmp (Options.int options "threads")
   158             |> Exn.capture);
   159       val res2 = Exn.capture Session.finish ();
   160       val _ = Par_Exn.release_all [res1, res2];
   161 
   162       val _ = Options.reset_default ();
   163       val _ = if do_output then () else exit 0;
   164     in () end);
   165 
   166 
   167 (* PIDE protocol *)
   168 
   169 val _ =
   170   Isabelle_Process.protocol_command "build_theories"
   171     (fn [id, master_dir, theories_yxml] =>
   172       let
   173         val theories =
   174           YXML.parse_body theories_yxml |>
   175             let open XML.Decode
   176             in list (pair Options.decode (list (string #> rpair Position.none))) end;
   177         val result =
   178           Exn.capture (fn () =>
   179             theories |> List.app (build_theories (K NONE) (Path.explode master_dir))) ();
   180         val ok =
   181           (case result of
   182             Exn.Res _ => true
   183           | Exn.Exn exn => (Runtime.exn_error_message exn; false));
   184     in Output.protocol_message (Markup.build_theories_result id ok) [] end);
   185 
   186 end;