src/Pure/Tools/build.ML
author wenzelm
Wed Feb 20 15:22:22 2013 +0100 (2013-02-20 ago)
changeset 51228 dff3471dd8bc
parent 51220 e140c8fa485a
child 51398 c3d02b3518c2
permissions -rw-r--r--
more tight representation of command timing;
tuned signatures;
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 (* protocol messages *)
    16 
    17 local
    18 
    19 (* FIXME avoid hardwired stuff!? *)
    20 val protocol_echo = [Markup.ML_statistics, Markup.task_statistics, Markup.command_timing];
    21 
    22 fun protocol_undef () = raise Fail "Undefined Output.protocol_message";
    23 
    24 in
    25 
    26 fun protocol_message props output =
    27   (case props of
    28     function :: args =>
    29       if member (op =) protocol_echo function then
    30         writeln ("\f" ^ #2 function ^ " = " ^ YXML.string_of_body (XML.Encode.properties args))
    31       else
    32         (case Markup.dest_loading_theory props of
    33           SOME name => writeln ("\floading_theory = " ^ name)
    34         | NONE => protocol_undef ())
    35   | [] => protocol_undef ());
    36 
    37 end;
    38 
    39 
    40 (* build *)
    41 
    42 local
    43 
    44 fun no_document options =
    45   (case Options.string options "document" of "" => true | "false" => true | _ => false);
    46 
    47 fun use_theories last_timing options =
    48   Thy_Info.use_theories {last_timing = last_timing, master_dir = Path.current}
    49     |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
    50     |> Unsynchronized.setmp print_mode
    51         (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    52     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    53     |> Unsynchronized.setmp Goal.parallel_proofs_threshold
    54         (Options.int options "parallel_proofs_threshold")
    55     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    56     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    57     |> Unsynchronized.setmp Future.ML_statistics true
    58     |> no_document options ? Present.no_document
    59     |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
    60     |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs")
    61     |> Unsynchronized.setmp Printer.show_question_marks_default
    62         (Options.bool options "show_question_marks")
    63     |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
    64     |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
    65     |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
    66     |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display")
    67     |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
    68     |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
    69     |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source")
    70     |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break")
    71     |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
    72     |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
    73 
    74 fun use_theories_condition last_timing (options, thys) =
    75   let val condition = space_explode "," (Options.string options "condition") in
    76     (case filter_out (can getenv_strict) condition of
    77       [] => use_theories last_timing options (map (rpair Position.none) thys)
    78     | conds =>
    79         Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
    80           " (undefined " ^ commas conds ^ ")\n"))
    81   end;
    82 
    83 
    84 (* command timings *)
    85 
    86 type timings = ((string * Time.time) Inttab.table) Symtab.table;  (*file -> offset -> name * time *)
    87 
    88 val empty_timings: timings = Symtab.empty;
    89 
    90 fun update_timings props =
    91   (case Markup.parse_command_timing_properties props of
    92     SOME ({file, offset, name}, time) =>
    93       Symtab.map_default (file, Inttab.empty) (Inttab.update (offset, (name, time)))
    94   | NONE => I);
    95 
    96 fun lookup_timings timings tr =
    97   (case Toplevel.approximative_id tr of
    98     SOME {file, offset, name} =>
    99       (case Symtab.lookup timings file of
   100         SOME offsets =>
   101           (case Inttab.lookup offsets offset of
   102             SOME (name', time) => if name = name' then time else Time.zeroTime
   103           | NONE => Time.zeroTime)
   104       | NONE => Time.zeroTime)
   105   | NONE => Time.zeroTime);
   106 
   107 in
   108 
   109 fun build args_file = Command_Line.tool (fn () =>
   110     let
   111       val (command_timings, (do_output, (options, (verbose, (browser_info,
   112           (parent_name, (name, theories))))))) =
   113         File.read (Path.explode args_file) |> YXML.parse_body |>
   114           let open XML.Decode in
   115             pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
   116               (pair string (pair string ((list (pair Options.decode (list string))))))))))
   117           end;
   118 
   119       val document_variants =
   120         map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
   121       val _ =
   122         (case duplicates (op =) (map fst document_variants) of
   123           [] => ()
   124         | dups => error ("Duplicate document variants: " ^ commas_quote dups));
   125 
   126       val _ = writeln ("\fSession.name = " ^ name);
   127       val _ =
   128         (case Session.path () of
   129           [] => ()
   130         | path => writeln ("\fSession.parent_path = " ^ space_implode "/" path));
   131       val _ =
   132         Session.init do_output false
   133           (Options.bool options "browser_info") browser_info
   134           (Options.string options "document")
   135           (Options.bool options "document_graph")
   136           (Options.string options "document_output")
   137           document_variants
   138           parent_name name
   139           (false, "") ""
   140           verbose;
   141 
   142       val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
   143 
   144       val res1 =
   145         theories |>
   146           (List.app (use_theories_condition last_timing)
   147             |> Session.with_timing name verbose
   148             |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
   149             |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
   150             |> Exn.capture);
   151       val res2 = Exn.capture Session.finish ();
   152       val _ = Par_Exn.release_all [res1, res2];
   153 
   154       val _ = if do_output then () else exit 0;
   155     in 0 end);
   156 
   157 end;
   158 
   159 end;