src/Pure/Tools/build.ML
author wenzelm
Tue Apr 09 20:16:52 2013 +0200 (2013-04-09 ago)
changeset 51662 3391a493f39a
parent 51661 92e58b76dbb1
child 51666 b97aeb018900
permissions -rw-r--r--
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
     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) (Inttab.update (offset, (name, time)))
    25   | NONE => I);
    26 
    27 fun approximative_id name pos =
    28   (case (Position.file_of pos, Position.offset_of pos) of
    29     (SOME file, SOME offset) =>
    30       if name = "" then NONE else SOME {file = file, offset = offset, name = name}
    31   | _ => NONE);
    32 
    33 fun lookup_timings timings tr =
    34   (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of
    35     SOME {file, offset, name} =>
    36       (case Symtab.lookup timings file of
    37         SOME offsets =>
    38           (case Inttab.lookup offsets offset of
    39             SOME (name', time) => if name = name' then SOME time else NONE
    40           | NONE => NONE)
    41       | NONE => NONE)
    42   | NONE => NONE);
    43 
    44 
    45 (* protocol messages *)
    46 
    47 fun inline_message a args =
    48   writeln ("\f" ^ a ^ " = " ^ YXML.string_of_body (XML.Encode.properties args));
    49 
    50 fun protocol_message props output =
    51   (case props of
    52     function :: args =>
    53       if function = Markup.ML_statistics orelse function = Markup.task_statistics then
    54         inline_message (#2 function) args
    55       else if function = Markup.command_timing then
    56         let
    57           val name = the_default "" (Properties.get args Markup.nameN);
    58           val pos = Position.of_properties args;
    59           val {elapsed, ...} = Markup.parse_timing_properties args;
    60         in
    61           (case approximative_id name pos of
    62             SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed)
    63           | NONE => ())
    64         end
    65       else
    66         (case Markup.dest_loading_theory props of
    67           SOME name => writeln ("\floading_theory = " ^ name)
    68         | NONE => raise Output.Protocol_Message props)
    69   | [] => raise Output.Protocol_Message props);
    70 
    71 
    72 (* build *)
    73 
    74 local
    75 
    76 fun no_document options =
    77   (case Options.string options "document" of "" => true | "false" => true | _ => false);
    78 
    79 fun use_theories last_timing options =
    80   Thy_Info.use_theories {last_timing = last_timing, master_dir = Path.current}
    81     |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
    82     |> Unsynchronized.setmp print_mode
    83         (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    84     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    85     |> Unsynchronized.setmp Goal.parallel_subproofs_saturation
    86         (Options.int options "parallel_subproofs_saturation")
    87     |> Unsynchronized.setmp Goal.parallel_subproofs_threshold
    88         (Options.real options "parallel_subproofs_threshold")
    89     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    90     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    91     |> Unsynchronized.setmp Future.ML_statistics true
    92     |> no_document options ? Present.no_document
    93     |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
    94     |> Unsynchronized.setmp Goal.skip_proofs (Options.bool options "skip_proofs")
    95     |> Unsynchronized.setmp Printer.show_question_marks_default
    96         (Options.bool options "show_question_marks")
    97     |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
    98     |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
    99     |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
   100     |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display")
   101     |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
   102     |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
   103     |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source")
   104     |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break")
   105     |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
   106     |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
   107 
   108 fun use_theories_condition last_timing (options, thys) =
   109   let val condition = space_explode "," (Options.string options "condition") in
   110     (case filter_out (can getenv_strict) condition of
   111       [] => use_theories last_timing options (map (rpair Position.none) thys)
   112     | conds =>
   113         Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
   114           " (undefined " ^ commas conds ^ ")\n"))
   115   end;
   116 
   117 in
   118 
   119 fun build args_file = Command_Line.tool (fn () =>
   120     let
   121       val (command_timings, (do_output, (options, (verbose, (browser_info,
   122           (parent_name, (chapter, (name, theories)))))))) =
   123         File.read (Path.explode args_file) |> YXML.parse_body |>
   124           let open XML.Decode in
   125             pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
   126               (pair string (pair string (pair string
   127                 ((list (pair Options.decode (list string)))))))))))
   128           end;
   129 
   130       val document_variants =
   131         map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
   132       val _ =
   133         (case duplicates (op =) (map fst document_variants) of
   134           [] => ()
   135         | dups => error ("Duplicate document variants: " ^ commas_quote dups));
   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           document_variants
   146           parent_name (chapter, name)
   147           (false, "")
   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 (use_theories_condition last_timing)
   155             |> Session.with_timing name verbose
   156             |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
   157             |> Unsynchronized.setmp Multithreading.max_threads (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 _ = if do_output then () else exit 0;
   163     in 0 end);
   164 
   165 end;
   166 
   167 end;