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