src/Pure/Tools/build.ML
author wenzelm
Tue Jan 13 21:46:09 2015 +0100 (2015-01-13 ago)
changeset 59362 41f1645a4f63
parent 59175 bf465f335e85
child 59364 3b5da177ae6b
permissions -rw-r--r--
some support for PIDE batch session;
clarified Thy_Info.use_thys_options and corresponding protocol command;
     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 use_theories last_timing master_dir (options, thys) =
   101   let val condition = space_explode "," (Options.string options "condition") in
   102     (case filter_out (can getenv_strict) condition of
   103       [] =>
   104         Thy_Info.use_thys_options last_timing master_dir options
   105           (map (rpair Position.none) thys)
   106     | conds =>
   107         Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
   108           " (undefined " ^ commas conds ^ ")\n"))
   109   end;
   110 
   111 fun build args_file = Command_Line.tool0 (fn () =>
   112     let
   113       val _ = SHA1_Samples.test ();
   114 
   115       val (command_timings, (do_output, (options, (verbose, (browser_info,
   116           (document_files, (parent_name, (chapter, (name, theories))))))))) =
   117         File.read (Path.explode args_file) |> YXML.parse_body |>
   118           let open XML.Decode in
   119             pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
   120               (pair (list (pair string string)) (pair string (pair string (pair string
   121                 ((list (pair Options.decode (list string))))))))))))
   122           end;
   123 
   124       val _ = Options.set_default options;
   125 
   126       val _ = writeln ("\fSession.name = " ^ name);
   127       val _ =
   128         Session.init do_output
   129           (Options.bool options "browser_info")
   130           (Path.explode browser_info)
   131           (Options.string options "document")
   132           (Options.bool options "document_graph")
   133           (Options.string options "document_output")
   134           (Present.document_variants (Options.string options "document_variants"))
   135           (map (apply2 Path.explode) document_files)
   136           parent_name (chapter, name)
   137           verbose;
   138 
   139       val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
   140 
   141       val res1 =
   142         theories |>
   143           (List.app (use_theories last_timing Path.current)
   144             |> session_timing name verbose
   145             |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
   146             |> Multithreading.max_threads_setmp (Options.int options "threads")
   147             |> Exn.capture);
   148       val res2 = Exn.capture Session.finish ();
   149       val _ = Par_Exn.release_all [res1, res2];
   150 
   151       val _ = Options.reset_default ();
   152       val _ = if do_output then () else exit 0;
   153     in () end);
   154 
   155 end;