wenzelm@51701
|
1 |
(* Title: Pure/Tools/build.ML
|
wenzelm@49433
|
2 |
Author: Makarius
|
wenzelm@49433
|
3 |
|
wenzelm@49433
|
4 |
Build Isabelle sessions.
|
wenzelm@49433
|
5 |
*)
|
wenzelm@49433
|
6 |
|
wenzelm@49433
|
7 |
signature BUILD =
|
wenzelm@49433
|
8 |
sig
|
wenzelm@49746
|
9 |
val build: string -> unit
|
wenzelm@49433
|
10 |
end;
|
wenzelm@49433
|
11 |
|
wenzelm@49433
|
12 |
structure Build: BUILD =
|
wenzelm@49433
|
13 |
struct
|
wenzelm@49433
|
14 |
|
wenzelm@51698
|
15 |
(* protocol messages *)
|
wenzelm@51698
|
16 |
|
wenzelm@52013
|
17 |
local
|
wenzelm@52013
|
18 |
|
wenzelm@51698
|
19 |
fun ML_statistics (function :: stats) "" =
|
wenzelm@51698
|
20 |
if function = Markup.ML_statistics then SOME stats
|
wenzelm@51698
|
21 |
else NONE
|
wenzelm@51698
|
22 |
| ML_statistics _ _ = NONE;
|
wenzelm@51698
|
23 |
|
wenzelm@51990
|
24 |
fun task_statistics (function :: stats) "" =
|
wenzelm@51990
|
25 |
if function = Markup.task_statistics then SOME stats
|
wenzelm@51990
|
26 |
else NONE
|
wenzelm@51990
|
27 |
| task_statistics _ _ = NONE;
|
wenzelm@51990
|
28 |
|
wenzelm@52013
|
29 |
val print_properties = YXML.string_of_body o XML.Encode.properties;
|
wenzelm@52013
|
30 |
|
wenzelm@52013
|
31 |
in
|
wenzelm@52013
|
32 |
|
wenzelm@51698
|
33 |
fun protocol_message props output =
|
wenzelm@51698
|
34 |
(case ML_statistics props output of
|
wenzelm@52013
|
35 |
SOME stats => writeln ("\fML_statistics = " ^ print_properties stats)
|
wenzelm@51860
|
36 |
| NONE =>
|
wenzelm@51990
|
37 |
(case task_statistics props output of
|
wenzelm@52013
|
38 |
SOME stats => writeln ("\ftask_statistics = " ^ print_properties stats)
|
wenzelm@51990
|
39 |
| NONE =>
|
wenzelm@51990
|
40 |
(case Markup.dest_loading_theory props of
|
wenzelm@51990
|
41 |
SOME name => writeln ("\floading_theory = " ^ name)
|
wenzelm@51990
|
42 |
| NONE => raise Fail "Undefined Output.protocol_message")));
|
wenzelm@51698
|
43 |
|
wenzelm@52013
|
44 |
end;
|
wenzelm@52013
|
45 |
|
wenzelm@51698
|
46 |
|
wenzelm@51698
|
47 |
(* build *)
|
wenzelm@51698
|
48 |
|
wenzelm@49480
|
49 |
local
|
wenzelm@49480
|
50 |
|
wenzelm@49515
|
51 |
fun no_document options =
|
wenzelm@51136
|
52 |
(case Options.string options "document" of "" => true | "false" => true | _ => false);
|
wenzelm@49515
|
53 |
|
wenzelm@49480
|
54 |
fun use_thys options =
|
wenzelm@49472
|
55 |
Thy_Info.use_thys
|
wenzelm@49472
|
56 |
|> Unsynchronized.setmp Proofterm.proofs (Options.int options "proofs")
|
wenzelm@49472
|
57 |
|> Unsynchronized.setmp print_mode
|
wenzelm@49472
|
58 |
(space_explode "," (Options.string options "print_mode") @ print_mode_value ())
|
wenzelm@49472
|
59 |
|> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
|
wenzelm@49472
|
60 |
|> Unsynchronized.setmp Goal.parallel_proofs_threshold
|
wenzelm@49472
|
61 |
(Options.int options "parallel_proofs_threshold")
|
wenzelm@49472
|
62 |
|> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
|
wenzelm@49475
|
63 |
|> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
|
wenzelm@51713
|
64 |
|> Unsynchronized.setmp Future.ML_statistics true
|
wenzelm@49515
|
65 |
|> no_document options ? Present.no_document
|
wenzelm@49501
|
66 |
|> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
|
wenzelm@49649
|
67 |
|> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs")
|
wenzelm@49501
|
68 |
|> Unsynchronized.setmp Printer.show_question_marks_default
|
wenzelm@49501
|
69 |
(Options.bool options "show_question_marks")
|
wenzelm@49501
|
70 |
|> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")
|
wenzelm@49501
|
71 |
|> Unsynchronized.setmp Name_Space.names_short_default (Options.bool options "names_short")
|
wenzelm@49507
|
72 |
|> Unsynchronized.setmp Name_Space.names_unique_default (Options.bool options "names_unique")
|
wenzelm@49535
|
73 |
|> Unsynchronized.setmp Thy_Output.display_default (Options.bool options "thy_output_display")
|
wenzelm@49535
|
74 |
|> Unsynchronized.setmp Thy_Output.quotes_default (Options.bool options "thy_output_quotes")
|
wenzelm@49535
|
75 |
|> Unsynchronized.setmp Thy_Output.indent_default (Options.int options "thy_output_indent")
|
wenzelm@49535
|
76 |
|> Unsynchronized.setmp Thy_Output.source_default (Options.bool options "thy_output_source")
|
wenzelm@49535
|
77 |
|> Unsynchronized.setmp Thy_Output.break_default (Options.bool options "thy_output_break")
|
wenzelm@49542
|
78 |
|> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
|
wenzelm@49507
|
79 |
|> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
|
wenzelm@49472
|
80 |
|
wenzelm@49480
|
81 |
fun use_theories (options, thys) =
|
wenzelm@49480
|
82 |
let val condition = space_explode "," (Options.string options "condition") in
|
wenzelm@49480
|
83 |
(case filter_out (can getenv_strict) condition of
|
wenzelm@49942
|
84 |
[] => use_thys options (map (rpair Position.none) thys)
|
wenzelm@49480
|
85 |
| conds =>
|
wenzelm@49527
|
86 |
Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
|
wenzelm@49492
|
87 |
" (undefined " ^ commas conds ^ ")\n"))
|
wenzelm@49480
|
88 |
end;
|
wenzelm@49480
|
89 |
|
wenzelm@49480
|
90 |
in
|
wenzelm@49480
|
91 |
|
wenzelm@49696
|
92 |
fun build args_file = Command_Line.tool (fn () =>
|
wenzelm@49687
|
93 |
let
|
wenzelm@49687
|
94 |
val (do_output, (options, (verbose, (browser_info, (parent_name,
|
wenzelm@49687
|
95 |
(name, theories)))))) =
|
wenzelm@49687
|
96 |
File.read (Path.explode args_file) |> YXML.parse_body |>
|
wenzelm@49687
|
97 |
let open XML.Decode in
|
wenzelm@49687
|
98 |
pair bool (pair Options.decode (pair bool (pair string (pair string
|
wenzelm@49687
|
99 |
(pair string ((list (pair Options.decode (list string)))))))))
|
wenzelm@49687
|
100 |
end;
|
wenzelm@49433
|
101 |
|
wenzelm@49819
|
102 |
val document_variants =
|
wenzelm@49819
|
103 |
map Present.read_variant (space_explode ":" (Options.string options "document_variants"));
|
wenzelm@49687
|
104 |
val _ =
|
wenzelm@49820
|
105 |
(case duplicates (op =) (map fst document_variants) of
|
wenzelm@49820
|
106 |
[] => ()
|
wenzelm@49820
|
107 |
| dups => error ("Duplicate document variants: " ^ commas_quote dups));
|
wenzelm@50257
|
108 |
|
wenzelm@51997
|
109 |
val _ = writeln ("\fSession.name = " ^ name);
|
wenzelm@50257
|
110 |
val _ =
|
wenzelm@51722
|
111 |
(case Session.path () of
|
wenzelm@51722
|
112 |
[] => ()
|
wenzelm@51722
|
113 |
| path => writeln ("\fSession.parent_path = " ^ space_implode "/" path));
|
wenzelm@51722
|
114 |
val _ =
|
wenzelm@49687
|
115 |
Session.init do_output false
|
wenzelm@49687
|
116 |
(Options.bool options "browser_info") browser_info
|
wenzelm@49687
|
117 |
(Options.string options "document")
|
wenzelm@49687
|
118 |
(Options.bool options "document_graph")
|
wenzelm@49820
|
119 |
(Options.string options "document_output")
|
wenzelm@49819
|
120 |
document_variants
|
wenzelm@49687
|
121 |
parent_name name
|
wenzelm@51136
|
122 |
(false, "") ""
|
wenzelm@51136
|
123 |
verbose;
|
wenzelm@50926
|
124 |
|
wenzelm@50926
|
125 |
val res1 =
|
wenzelm@49688
|
126 |
theories |>
|
wenzelm@49688
|
127 |
(List.app use_theories
|
wenzelm@49688
|
128 |
|> Session.with_timing name verbose
|
wenzelm@51698
|
129 |
|> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
|
wenzelm@50926
|
130 |
|> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
|
wenzelm@50926
|
131 |
|> Exn.capture);
|
wenzelm@50926
|
132 |
val res2 = Exn.capture Session.finish ();
|
wenzelm@50926
|
133 |
val _ = Par_Exn.release_all [res1, res2];
|
wenzelm@49688
|
134 |
|
wenzelm@49749
|
135 |
val _ = if do_output then () else exit 0;
|
wenzelm@49696
|
136 |
in 0 end);
|
wenzelm@49433
|
137 |
|
wenzelm@49433
|
138 |
end;
|
wenzelm@49480
|
139 |
|
wenzelm@49480
|
140 |
end;
|