src/Pure/Tools/build.ML
author wenzelm
Fri May 17 18:19:42 2013 +0200 (2013-05-17 ago)
changeset 52052 892061142ba6
parent 52041 80e001b85332
child 52059 2f970c7f722b
permissions -rw-r--r--
discontinued obsolete isabelle usedir, mkdir, make;
     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 (* session timing *)
    47 
    48 fun session_timing name verbose f x =
    49   let
    50     val start = Timing.start ();
    51     val y = f x;
    52     val timing = Timing.result start;
    53 
    54     val threads = string_of_int (Multithreading.max_threads_value ());
    55     val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
    56       |> Real.fmt (StringCvt.FIX (SOME 2));
    57 
    58     val timing_props =
    59       [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)];
    60     val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props));
    61     val _ =
    62       if verbose then
    63         Output.physical_stderr ("Timing " ^ name ^ " (" ^
    64           threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n")
    65       else ();
    66   in y end;
    67 
    68 
    69 (* protocol messages *)
    70 
    71 fun inline_message a args =
    72   writeln ("\f" ^ a ^ " = " ^ YXML.string_of_body (XML.Encode.properties args));
    73 
    74 fun protocol_message props output =
    75   (case props of
    76     function :: args =>
    77       if function = Markup.ML_statistics orelse function = Markup.task_statistics then
    78         inline_message (#2 function) args
    79       else if function = Markup.command_timing then
    80         let
    81           val name = the_default "" (Properties.get args Markup.nameN);
    82           val pos = Position.of_properties args;
    83           val {elapsed, ...} = Markup.parse_timing_properties args;
    84         in
    85           (case approximative_id name pos of
    86             SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed)
    87           | NONE => ())
    88         end
    89       else
    90         (case Markup.dest_loading_theory props of
    91           SOME name => writeln ("\floading_theory = " ^ name)
    92         | NONE => raise Output.Protocol_Message props)
    93   | [] => raise Output.Protocol_Message props);
    94 
    95 
    96 (* build *)
    97 
    98 local
    99 
   100 fun no_document options =
   101   (case Options.string options "document" of "" => true | "false" => true | _ => false);
   102 
   103 fun use_theories last_timing options =
   104   Thy_Info.use_theories {last_timing = last_timing, master_dir = Path.current}
   105     |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
   106     |> Unsynchronized.setmp print_mode
   107         (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
   108     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
   109     |> Unsynchronized.setmp Goal.parallel_subproofs_saturation
   110         (Options.int options "parallel_subproofs_saturation")
   111     |> Unsynchronized.setmp Goal.parallel_subproofs_threshold
   112         (Options.real options "parallel_subproofs_threshold")
   113     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
   114     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
   115     |> Unsynchronized.setmp Future.ML_statistics true
   116     |> no_document options ? Present.no_document
   117     |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
   118     |> Unsynchronized.setmp Goal.skip_proofs (Options.bool options "skip_proofs")
   119     |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
   120     |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
   121 
   122 fun use_theories_condition last_timing (options, thys) =
   123   let val condition = space_explode "," (Options.string options "condition") in
   124     (case filter_out (can getenv_strict) condition of
   125       [] =>
   126         (Options.set_default options;
   127          use_theories last_timing options (map (rpair Position.none) thys))
   128     | conds =>
   129         Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
   130           " (undefined " ^ commas conds ^ ")\n"))
   131   end;
   132 
   133 in
   134 
   135 fun build args_file = Command_Line.tool (fn () =>
   136     let
   137       val (command_timings, (do_output, (options, (verbose, (browser_info,
   138           (parent_name, (chapter, (name, theories)))))))) =
   139         File.read (Path.explode args_file) |> YXML.parse_body |>
   140           let open XML.Decode in
   141             pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
   142               (pair string (pair string (pair string
   143                 ((list (pair Options.decode (list string)))))))))))
   144           end;
   145 
   146       val _ = Options.set_default options;
   147 
   148       val document_variants =
   149         map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
   150       val _ =
   151         (case duplicates (op =) (map fst document_variants) of
   152           [] => ()
   153         | dups => error ("Duplicate document variants: " ^ commas_quote dups));
   154 
   155       val _ = writeln ("\fSession.name = " ^ name);
   156       val _ =
   157         Session.init do_output
   158           (Options.bool options "browser_info")
   159           (Path.explode browser_info)
   160           (Options.string options "document")
   161           (Options.bool options "document_graph")
   162           (Options.string options "document_output")
   163           document_variants
   164           parent_name (chapter, name)
   165           (false, "")
   166           verbose;
   167 
   168       val last_timing = lookup_timings (fold update_timings command_timings empty_timings);
   169 
   170       val res1 =
   171         theories |>
   172           (List.app (use_theories_condition last_timing)
   173             |> session_timing name verbose
   174             |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
   175             |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
   176             |> Exn.capture);
   177       val res2 = Exn.capture Session.finish ();
   178       val _ = Par_Exn.release_all [res1, res2];
   179 
   180       val _ = Options.reset_default ();
   181       val _ = if do_output then () else exit 0;
   182     in 0 end);
   183 
   184 end;
   185 
   186 end;