src/Pure/Tools/build.ML
author wenzelm
Tue Apr 09 21:22:15 2013 +0200 (2013-04-09 ago)
changeset 51666 b97aeb018900
parent 51662 3391a493f39a
child 51941 ead4248aef3b
permissions -rw-r--r--
add command timings (like document command status);
     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 (* protocol messages *)
    47 
    48 fun inline_message a args =
    49   writeln ("\f" ^ a ^ " = " ^ YXML.string_of_body (XML.Encode.properties args));
    50 
    51 fun protocol_message props output =
    52   (case props of
    53     function :: args =>
    54       if function = Markup.ML_statistics orelse function = Markup.task_statistics then
    55         inline_message (#2 function) args
    56       else if function = Markup.command_timing then
    57         let
    58           val name = the_default "" (Properties.get args Markup.nameN);
    59           val pos = Position.of_properties args;
    60           val {elapsed, ...} = Markup.parse_timing_properties args;
    61         in
    62           (case approximative_id name pos of
    63             SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed)
    64           | NONE => ())
    65         end
    66       else
    67         (case Markup.dest_loading_theory props of
    68           SOME name => writeln ("\floading_theory = " ^ name)
    69         | NONE => raise Output.Protocol_Message props)
    70   | [] => raise Output.Protocol_Message props);
    71 
    72 
    73 (* build *)
    74 
    75 local
    76 
    77 fun no_document options =
    78   (case Options.string options "document" of "" => true | "false" => true | _ => false);
    79 
    80 fun use_theories last_timing options =
    81   Thy_Info.use_theories {last_timing = last_timing, master_dir = Path.current}
    82     |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
    83     |> Unsynchronized.setmp print_mode
    84         (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    85     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    86     |> Unsynchronized.setmp Goal.parallel_subproofs_saturation
    87         (Options.int options "parallel_subproofs_saturation")
    88     |> Unsynchronized.setmp Goal.parallel_subproofs_threshold
    89         (Options.real options "parallel_subproofs_threshold")
    90     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    91     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    92     |> Unsynchronized.setmp Future.ML_statistics true
    93     |> no_document options ? Present.no_document
    94     |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
    95     |> Unsynchronized.setmp Goal.skip_proofs (Options.bool options "skip_proofs")
    96     |> Unsynchronized.setmp Printer.show_question_marks_default
    97         (Options.bool options "show_question_marks")
    98     |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
    99     |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
   100     |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
   101     |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display")
   102     |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
   103     |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
   104     |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source")
   105     |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break")
   106     |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
   107     |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
   108 
   109 fun use_theories_condition last_timing (options, thys) =
   110   let val condition = space_explode "," (Options.string options "condition") in
   111     (case filter_out (can getenv_strict) condition of
   112       [] => use_theories last_timing options (map (rpair Position.none) thys)
   113     | conds =>
   114         Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
   115           " (undefined " ^ commas conds ^ ")\n"))
   116   end;
   117 
   118 in
   119 
   120 fun build args_file = Command_Line.tool (fn () =>
   121     let
   122       val (command_timings, (do_output, (options, (verbose, (browser_info,
   123           (parent_name, (chapter, (name, theories)))))))) =
   124         File.read (Path.explode args_file) |> YXML.parse_body |>
   125           let open XML.Decode in
   126             pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
   127               (pair string (pair string (pair string
   128                 ((list (pair Options.decode (list string)))))))))))
   129           end;
   130 
   131       val document_variants =
   132         map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
   133       val _ =
   134         (case duplicates (op =) (map fst document_variants) of
   135           [] => ()
   136         | dups => error ("Duplicate document variants: " ^ commas_quote dups));
   137 
   138       val _ = writeln ("\fSession.name = " ^ name);
   139       val _ =
   140         Session.init do_output
   141           (Options.bool options "browser_info")
   142           (Path.explode browser_info)
   143           (Options.string options "document")
   144           (Options.bool options "document_graph")
   145           (Options.string options "document_output")
   146           document_variants
   147           parent_name (chapter, name)
   148           (false, "")
   149           verbose;
   150 
   151       val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
   152 
   153       val res1 =
   154         theories |>
   155           (List.app (use_theories_condition last_timing)
   156             |> Session.with_timing name verbose
   157             |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
   158             |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
   159             |> Exn.capture);
   160       val res2 = Exn.capture Session.finish ();
   161       val _ = Par_Exn.release_all [res1, res2];
   162 
   163       val _ = if do_output then () else exit 0;
   164     in 0 end);
   165 
   166 end;
   167 
   168 end;