src/Pure/Tools/build.ML
author wenzelm
Sun May 12 20:25:45 2013 +0200 (2013-05-12 ago)
changeset 51949 f6858bb224c9
parent 51941 ead4248aef3b
child 52041 80e001b85332
permissions -rw-r--r--
some system options as context-sensitive config options;
     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 Thy_Output.display_default (Options.bool options "thy_output_display")
    97     |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
    98     |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
    99     |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source")
   100     |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break")
   101     |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
   102     |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
   103 
   104 fun use_theories_condition last_timing (options, thys) =
   105   let val condition = space_explode "," (Options.string options "condition") in
   106     (case filter_out (can getenv_strict) condition of
   107       [] =>
   108         (Options.set_default options;
   109          use_theories last_timing options (map (rpair Position.none) thys))
   110     | conds =>
   111         Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
   112           " (undefined " ^ commas conds ^ ")\n"))
   113   end;
   114 
   115 in
   116 
   117 fun build args_file = Command_Line.tool (fn () =>
   118     let
   119       val (command_timings, (do_output, (options, (verbose, (browser_info,
   120           (parent_name, (chapter, (name, theories)))))))) =
   121         File.read (Path.explode args_file) |> YXML.parse_body |>
   122           let open XML.Decode in
   123             pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
   124               (pair string (pair string (pair string
   125                 ((list (pair Options.decode (list string)))))))))))
   126           end;
   127 
   128       val _ = Options.set_default options;
   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 _ = Options.reset_default ();
   163       val _ = if do_output then () else exit 0;
   164     in 0 end);
   165 
   166 end;
   167 
   168 end;