src/Pure/Tools/build.ML
author wenzelm
Thu Apr 17 11:29:15 2014 +0200 (2014-04-17 ago)
changeset 56612 74851ff86180
parent 56533 cd8b6d849b6a
child 56614 d80f43dab30e
permissions -rw-r--r--
tuned;
     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           (case approximative_id name pos of
    86             SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed)
    87           | NONE => ())
    88         end
    89       else
    90         (case Markup.dest_loading_theory props of
    91           SOME name => writeln ("\floading_theory = " ^ name)
    92         | NONE => raise Output.Protocol_Message props)
    93   | [] => raise Output.Protocol_Message props);
    94 
    95 
    96 (* build *)
    97 
    98 local
    99 
   100 fun use_theories last_timing options =
   101   Thy_Info.use_theories {
   102       document =
   103         (case Options.string options "document" of "" => false | "false" => false | _ => true),
   104       last_timing = last_timing,
   105       master_dir = Path.current}
   106     |> Unsynchronized.setmp print_mode
   107         (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
   108     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
   109     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
   110     |> Multithreading.max_threads_setmp (Options.int options "threads")
   111     |> Unsynchronized.setmp Future.ML_statistics true
   112     |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
   113     |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
   114 
   115 fun use_theories_condition last_timing (options, thys) =
   116   let val condition = space_explode "," (Options.string options "condition") in
   117     (case filter_out (can getenv_strict) condition of
   118       [] =>
   119         (Options.set_default options;
   120          use_theories last_timing options (map (rpair Position.none) thys))
   121     | conds =>
   122         Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
   123           " (undefined " ^ commas conds ^ ")\n"))
   124   end;
   125 
   126 in
   127 
   128 fun build args_file = Command_Line.tool (fn () =>
   129     let
   130       val _ = SHA1_Samples.test ();
   131 
   132       val (command_timings, (do_output, (options, (verbose, (browser_info,
   133           (document_files, (parent_name, (chapter, (name, theories))))))))) =
   134         File.read (Path.explode args_file) |> YXML.parse_body |>
   135           let open XML.Decode in
   136             pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
   137               (pair (list (pair string string)) (pair string (pair string (pair string
   138                 ((list (pair Options.decode (list string))))))))))))
   139           end;
   140 
   141       val _ = Options.set_default options;
   142 
   143       val _ = writeln ("\fSession.name = " ^ name);
   144       val _ =
   145         Session.init do_output
   146           (Options.bool options "browser_info")
   147           (Path.explode browser_info)
   148           (Options.string options "document")
   149           (Options.bool options "document_graph")
   150           (Options.string options "document_output")
   151           (Present.document_variants (Options.string options "document_variants"))
   152           (map (pairself Path.explode) document_files)
   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 (use_theories_condition last_timing)
   161             |> session_timing name verbose
   162             |> Unsynchronized.setmp Outer_Syntax.batch_mode true
   163             |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
   164             |> Multithreading.max_threads_setmp (Options.int options "threads")
   165             |> Exn.capture);
   166       val res2 = Exn.capture Session.finish ();
   167       val _ = Par_Exn.release_all [res1, res2];
   168 
   169       val _ = Options.reset_default ();
   170       val _ = if do_output then () else exit 0;
   171     in 0 end);
   172 
   173 end;
   174 
   175 end;