src/Pure/Tools/build.ML
author wenzelm
Sat Dec 16 21:53:07 2017 +0100 (18 months ago)
changeset 67219 81e9804b2014
parent 66873 9953ae603a23
child 67297 86a099f896fc
permissions -rw-r--r--
added document antiquotation @{session name};
renamed protocol function "Prover.session_base" to "Prover.init_session_base" according to the ML/Scala operation;
     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, 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 get_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   |> the_default Time.zeroTime;
    45 
    46 
    47 (* session timing *)
    48 
    49 fun session_timing name verbose f x =
    50   let
    51     val start = Timing.start ();
    52     val y = f x;
    53     val timing = Timing.result start;
    54 
    55     val threads = string_of_int (Multithreading.max_threads ());
    56     val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
    57       |> Real.fmt (StringCvt.FIX (SOME 2));
    58 
    59     val timing_props =
    60       [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)];
    61     val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props));
    62     val _ =
    63       if verbose then
    64         Output.physical_stderr ("Timing " ^ name ^ " (" ^
    65           threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n")
    66       else ();
    67   in y end;
    68 
    69 
    70 (* protocol messages *)
    71 
    72 fun inline_message a args =
    73   writeln ("\f" ^ a ^ " = " ^ YXML.string_of_body (XML.Encode.properties args));
    74 
    75 fun protocol_message props output =
    76   (case props of
    77     function :: args =>
    78       if function = Markup.ML_statistics orelse function = Markup.task_statistics then
    79         inline_message (#2 function) args
    80       else if function = Markup.command_timing then
    81         let
    82           val name = the_default "" (Properties.get args Markup.nameN);
    83           val pos = Position.of_properties args;
    84           val {elapsed, ...} = Markup.parse_timing_properties args;
    85           val is_significant =
    86             Timing.is_relevant_time elapsed andalso
    87             elapsed >= Options.default_seconds "command_timing_threshold";
    88         in
    89           if is_significant then
    90             (case approximative_id name pos of
    91               SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed)
    92             | NONE => ())
    93           else ()
    94         end
    95       else if function = Markup.theory_timing then
    96         inline_message (#2 function) args
    97       else
    98         (case Markup.dest_loading_theory props of
    99           SOME name => writeln ("\floading_theory = " ^ name)
   100         | NONE => raise Output.Protocol_Message props)
   101   | [] => raise Output.Protocol_Message props);
   102 
   103 
   104 (* build theories *)
   105 
   106 fun build_theories symbols last_timing qualifier master_dir (options, thys) =
   107   let
   108     val condition = space_explode "," (Options.string options "condition");
   109     val conds = filter_out (can getenv_strict) condition;
   110   in
   111     if null conds then
   112       (if Options.bool options "checkpoint" then ML_Heap.share_common_data () else ();
   113         Options.set_default options;
   114         Isabelle_Process.init_options ();
   115         Future.fork I;
   116         (Thy_Info.use_theories {
   117           document = Present.document_enabled (Options.string options "document"),
   118           symbols = symbols,
   119           last_timing = last_timing,
   120           qualifier = qualifier,
   121           master_dir = master_dir}
   122         |>
   123           (case Options.string options "profiling" of
   124             "" => I
   125           | "time" => profile_time
   126           | "allocations" => profile_allocations
   127           | bad => error ("Bad profiling option: " ^ quote bad))
   128         |> Unsynchronized.setmp print_mode
   129             (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys)
   130     else
   131       Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
   132         " (undefined " ^ commas conds ^ ")\n")
   133   end;
   134 
   135 
   136 (* build session *)
   137 
   138 datatype args = Args of
   139  {symbol_codes: (string * int) list,
   140   command_timings: Properties.T list,
   141   do_output: bool,
   142   verbose: bool,
   143   browser_info: Path.T,
   144   document_files: (Path.T * Path.T) list,
   145   graph_file: Path.T,
   146   parent_name: string,
   147   chapter: string,
   148   name: string,
   149   master_dir: Path.T,
   150   theories: (Options.T * (string * Position.T) list) list,
   151   sessions: string list,
   152   global_theories: (string * string) list,
   153   loaded_theories: string list,
   154   known_theories: (string * string) list};
   155 
   156 fun decode_args yxml =
   157   let
   158     open XML.Decode;
   159     val position = Position.of_properties o properties;
   160     val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
   161       (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
   162       (theories, (sessions, (global_theories, (loaded_theories, known_theories))))))))))))))) =
   163       pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
   164         (pair (list (pair string string)) (pair string (pair string (pair string (pair string
   165           (pair string
   166             (pair (((list (pair Options.decode (list (pair string position))))))
   167               (pair (list string) (pair (list (pair string string))
   168                 (pair (list string) (list (pair string string))))))))))))))))
   169       (YXML.parse_body yxml);
   170   in
   171     Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
   172       verbose = verbose, browser_info = Path.explode browser_info,
   173       document_files = map (apply2 Path.explode) document_files,
   174       graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
   175       name = name, master_dir = Path.explode master_dir, theories = theories, sessions = sessions,
   176       global_theories = global_theories, loaded_theories = loaded_theories,
   177       known_theories = known_theories}
   178   end;
   179 
   180 fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
   181     document_files, graph_file, parent_name, chapter, name, master_dir, theories, sessions,
   182     global_theories, loaded_theories, known_theories}) =
   183   let
   184     val symbols = HTML.make_symbols symbol_codes;
   185 
   186     val _ =
   187       Resources.init_session_base
   188         {sessions = sessions,
   189          global_theories = global_theories,
   190          loaded_theories = loaded_theories,
   191          known_theories = known_theories};
   192 
   193     val _ =
   194       Session.init
   195         symbols
   196         do_output
   197         (Options.default_bool "browser_info")
   198         browser_info
   199         (Options.default_string "document")
   200         (Options.default_string "document_output")
   201         (Present.document_variants (Options.default_string "document_variants"))
   202         document_files
   203         graph_file
   204         parent_name
   205         (chapter, name)
   206         verbose;
   207 
   208     val last_timing = get_timings (fold update_timings command_timings empty_timings);
   209 
   210     val res1 =
   211       theories |>
   212         (List.app (build_theories symbols last_timing name master_dir)
   213           |> session_timing name verbose
   214           |> Exn.capture);
   215     val res2 = Exn.capture Session.finish ();
   216 
   217     val _ = Resources.finish_session_base ();
   218     val _ = Par_Exn.release_all [res1, res2];
   219   in () end;
   220 
   221 (*command-line tool*)
   222 fun build args_file =
   223   let
   224     val _ = SHA1.test_samples ();
   225     val _ = Options.load_default ();
   226     val _ = Isabelle_Process.init_options ();
   227     val args = decode_args (File.read (Path.explode args_file));
   228     fun error_message msg = writeln ("\ferror_message = " ^ encode_lines (YXML.content_of msg));
   229     val _ =
   230       Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
   231         build_session args
   232       handle exn => (List.app error_message (Runtime.exn_message_list exn); Exn.reraise exn);
   233     val _ = Options.reset_default ();
   234   in () end;
   235 
   236 (*PIDE version*)
   237 val _ =
   238   Isabelle_Process.protocol_command "build_session"
   239     (fn [args_yxml] =>
   240       let
   241         val args = decode_args args_yxml;
   242         val result = (build_session args; "") handle exn =>
   243           (Runtime.exn_message exn handle _ (*sic!*) =>
   244             "Exception raised, but failed to print details!");
   245     in Output.protocol_message Markup.build_session_finished [result] end | _ => raise Match);
   246 
   247 end;