src/Pure/Tools/build.ML
author wenzelm
Sun May 12 15:05:15 2013 +0200 (2013-05-12 ago)
changeset 51941 ead4248aef3b
parent 51666 b97aeb018900
child 51949 f6858bb224c9
permissions -rw-r--r--
full default options for Isabelle_Process and 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)
    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       [] =>
   113         (Options.set_default options;
   114          use_theories last_timing options (map (rpair Position.none) thys))
   115     | conds =>
   116         Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
   117           " (undefined " ^ commas conds ^ ")\n"))
   118   end;
   119 
   120 in
   121 
   122 fun build args_file = Command_Line.tool (fn () =>
   123     let
   124       val (command_timings, (do_output, (options, (verbose, (browser_info,
   125           (parent_name, (chapter, (name, theories)))))))) =
   126         File.read (Path.explode args_file) |> YXML.parse_body |>
   127           let open XML.Decode in
   128             pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
   129               (pair string (pair string (pair string
   130                 ((list (pair Options.decode (list string)))))))))))
   131           end;
   132 
   133       val _ = Options.set_default options;
   134 
   135       val document_variants =
   136         map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
   137       val _ =
   138         (case duplicates (op =) (map fst document_variants) of
   139           [] => ()
   140         | dups => error ("Duplicate document variants: " ^ commas_quote dups));
   141 
   142       val _ = writeln ("\fSession.name = " ^ name);
   143       val _ =
   144         Session.init do_output
   145           (Options.bool options "browser_info")
   146           (Path.explode browser_info)
   147           (Options.string options "document")
   148           (Options.bool options "document_graph")
   149           (Options.string options "document_output")
   150           document_variants
   151           parent_name (chapter, name)
   152           (false, "")
   153           verbose;
   154 
   155       val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
   156 
   157       val res1 =
   158         theories |>
   159           (List.app (use_theories_condition last_timing)
   160             |> Session.with_timing name verbose
   161             |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
   162             |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
   163             |> Exn.capture);
   164       val res2 = Exn.capture Session.finish ();
   165       val _ = Par_Exn.release_all [res1, res2];
   166 
   167       val _ = Options.reset_default ();
   168       val _ = if do_output then () else exit 0;
   169     in 0 end);
   170 
   171 end;
   172 
   173 end;