src/Pure/Tools/build.ML
author wenzelm
Thu Jan 24 17:18:13 2013 +0100 (2013-01-24 ago)
changeset 51045 630c0895d9d1
parent 50982 a7aa17a1f721
child 51216 e6e7685fc8f8
permissions -rw-r--r--
more efficient inlined properties, especially relevant for voluminous tasks trace;
     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 local
    18 
    19 fun ML_statistics (function :: stats) "" =
    20       if function = Markup.ML_statistics then SOME stats
    21       else NONE
    22   | ML_statistics _ _ = NONE;
    23 
    24 fun task_statistics (function :: stats) "" =
    25       if function = Markup.task_statistics then SOME stats
    26       else NONE
    27   | task_statistics _ _ = NONE;
    28 
    29 val print_properties = YXML.string_of_body o XML.Encode.properties;
    30 
    31 in
    32 
    33 fun protocol_message props output =
    34   (case ML_statistics props output of
    35     SOME stats => writeln ("\fML_statistics = " ^ print_properties stats)
    36   | NONE =>
    37       (case task_statistics props output of
    38         SOME stats => writeln ("\ftask_statistics = " ^ print_properties stats)
    39       | NONE =>
    40           (case Markup.dest_loading_theory props of
    41             SOME name => writeln ("\floading_theory = " ^ name)
    42           | NONE => raise Fail "Undefined Output.protocol_message")));
    43 
    44 end;
    45 
    46 
    47 (* build *)
    48 
    49 local
    50 
    51 fun no_document options =
    52   (case Options.string options "document" of "" => true | "false" => true | _ => false);
    53 
    54 fun use_thys options =
    55   Thy_Info.use_thys
    56     |> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
    57     |> Unsynchronized.setmp print_mode
    58         (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    59     |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    60     |> Unsynchronized.setmp Goal.parallel_proofs_threshold
    61         (Options.int options "parallel_proofs_threshold")
    62     |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    63     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    64     |> Unsynchronized.setmp Future.ML_statistics true
    65     |> no_document options ? Present.no_document
    66     |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
    67     |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs")
    68     |> Unsynchronized.setmp Printer.show_question_marks_default
    69         (Options.bool options "show_question_marks")
    70     |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
    71     |> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
    72     |> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
    73     |> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display")
    74     |> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
    75     |> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
    76     |> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source")
    77     |> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break")
    78     |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
    79     |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
    80 
    81 fun use_theories (options, thys) =
    82   let val condition = space_explode "," (Options.string options "condition") in
    83     (case filter_out (can getenv_strict) condition of
    84       [] => use_thys options (map (rpair Position.none) thys)
    85     | conds =>
    86         Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
    87           " (undefined " ^ commas conds ^ ")\n"))
    88   end;
    89 
    90 in
    91 
    92 fun build args_file = Command_Line.tool (fn () =>
    93     let
    94       val (do_output, (options, (verbose, (browser_info, (parent_name,
    95           (name, theories)))))) =
    96         File.read (Path.explode args_file) |> YXML.parse_body |>
    97           let open XML.Decode in
    98             pair bool (pair Options.decode (pair bool (pair string (pair string
    99               (pair string ((list (pair Options.decode (list string)))))))))
   100           end;
   101 
   102       val document_variants =
   103         map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
   104       val _ =
   105         (case duplicates (op =) (map fst document_variants) of
   106           [] => ()
   107         | dups => error ("Duplicate document variants: " ^ commas_quote dups));
   108 
   109       val _ = writeln ("\fSession.name = " ^ name);
   110       val _ =
   111         (case Session.path () of
   112           [] => ()
   113         | path => writeln ("\fSession.parent_path = " ^ space_implode "/" path));
   114       val _ =
   115         Session.init do_output false
   116           (Options.bool options "browser_info") browser_info
   117           (Options.string options "document")
   118           (Options.bool options "document_graph")
   119           (Options.string options "document_output")
   120           document_variants
   121           parent_name name
   122           (false, "") ""
   123           verbose;
   124 
   125       val res1 =
   126         theories |>
   127           (List.app use_theories
   128             |> Session.with_timing name verbose
   129             |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
   130             |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
   131             |> Exn.capture);
   132       val res2 = Exn.capture Session.finish ();
   133       val _ = Par_Exn.release_all [res1, res2];
   134 
   135       val _ = if do_output then () else exit 0;
   136     in 0 end);
   137 
   138 end;
   139 
   140 end;