author | wenzelm |
Sat, 18 Mar 2017 20:51:42 +0100 | |
changeset 65313 | 347ed6219dab |
parent 65307 | c1ba192b4f96 |
child 65318 | 342efc382558 |
permissions | -rw-r--r-- |
50686 | 1 |
(* Title: Pure/Tools/build.ML |
48418 | 2 |
Author: Makarius |
3 |
||
4 |
Build Isabelle sessions. |
|
5 |
*) |
|
6 |
||
7 |
signature BUILD = |
|
8 |
sig |
|
48731
a45ba78abcc1
more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
wenzelm
parents:
48681
diff
changeset
|
9 |
val build: string -> unit |
48418 | 10 |
end; |
11 |
||
12 |
structure Build: BUILD = |
|
13 |
struct |
|
14 |
||
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
15 |
(* command timings *) |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
16 |
|
56615 | 17 |
type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name, time*) |
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
18 |
|
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
19 |
val empty_timings: timings = Symtab.empty; |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
20 |
|
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
21 |
fun update_timings props = |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
22 |
(case Markup.parse_command_timing_properties props of |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
23 |
SOME ({file, offset, name}, time) => |
51666
b97aeb018900
add command timings (like document command status);
wenzelm
parents:
51662
diff
changeset
|
24 |
Symtab.map_default (file, Inttab.empty) |
62826 | 25 |
(Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time))) |
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
26 |
| NONE => I); |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
27 |
|
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
28 |
fun approximative_id name pos = |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
29 |
(case (Position.file_of pos, Position.offset_of pos) of |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
30 |
(SOME file, SOME offset) => |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
31 |
if name = "" then NONE else SOME {file = file, offset = offset, name = name} |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
32 |
| _ => NONE); |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
33 |
|
65058
3e9f382fb67e
absent timing information means zero, according to 0070053570c4, f235646b1b73;
wenzelm
parents:
64599
diff
changeset
|
34 |
fun get_timings timings tr = |
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
35 |
(case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
36 |
SOME {file, offset, name} => |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
37 |
(case Symtab.lookup timings file of |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
38 |
SOME offsets => |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
39 |
(case Inttab.lookup offsets offset of |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
40 |
SOME (name', time) => if name = name' then SOME time else NONE |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
41 |
| NONE => NONE) |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
42 |
| NONE => NONE) |
65058
3e9f382fb67e
absent timing information means zero, according to 0070053570c4, f235646b1b73;
wenzelm
parents:
64599
diff
changeset
|
43 |
| NONE => NONE) |
3e9f382fb67e
absent timing information means zero, according to 0070053570c4, f235646b1b73;
wenzelm
parents:
64599
diff
changeset
|
44 |
|> the_default Time.zeroTime; |
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
45 |
|
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
46 |
|
52052
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
47 |
(* session timing *) |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
48 |
|
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
49 |
fun session_timing name verbose f x = |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
50 |
let |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
51 |
val start = Timing.start (); |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
52 |
val y = f x; |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
53 |
val timing = Timing.result start; |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
54 |
|
62925 | 55 |
val threads = string_of_int (Multithreading.max_threads ()); |
52052
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
56 |
val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
57 |
|> Real.fmt (StringCvt.FIX (SOME 2)); |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
58 |
|
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
59 |
val timing_props = |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
60 |
[("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)]; |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
61 |
val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props)); |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
62 |
val _ = |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
63 |
if verbose then |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
64 |
Output.physical_stderr ("Timing " ^ name ^ " (" ^ |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
65 |
threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n") |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
66 |
else (); |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
67 |
in y end; |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
68 |
|
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
69 |
|
50683 | 70 |
(* protocol messages *) |
71 |
||
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
72 |
fun inline_message a args = |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
73 |
writeln ("\f" ^ a ^ " = " ^ YXML.string_of_body (XML.Encode.properties args)); |
50683 | 74 |
|
75 |
fun protocol_message props output = |
|
51216 | 76 |
(case props of |
77 |
function :: args => |
|
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
78 |
if function = Markup.ML_statistics orelse function = Markup.task_statistics then |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
79 |
inline_message (#2 function) args |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
80 |
else if function = Markup.command_timing then |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
81 |
let |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
82 |
val name = the_default "" (Properties.get args Markup.nameN); |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
83 |
val pos = Position.of_properties args; |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
84 |
val {elapsed, ...} = Markup.parse_timing_properties args; |
62793
f235646b1b73
less bulky timing information, e.g. HOL 56913 ~> 672;
wenzelm
parents:
62715
diff
changeset
|
85 |
val is_significant = |
f235646b1b73
less bulky timing information, e.g. HOL 56913 ~> 672;
wenzelm
parents:
62715
diff
changeset
|
86 |
Timing.is_relevant_time elapsed andalso |
62826 | 87 |
elapsed >= Options.default_seconds "command_timing_threshold"; |
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
88 |
in |
62793
f235646b1b73
less bulky timing information, e.g. HOL 56913 ~> 672;
wenzelm
parents:
62715
diff
changeset
|
89 |
if is_significant then |
59149
0070053570c4
suppress irrelevant timing messages (the majority);
wenzelm
parents:
59058
diff
changeset
|
90 |
(case approximative_id name pos of |
0070053570c4
suppress irrelevant timing messages (the majority);
wenzelm
parents:
59058
diff
changeset
|
91 |
SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed) |
0070053570c4
suppress irrelevant timing messages (the majority);
wenzelm
parents:
59058
diff
changeset
|
92 |
| NONE => ()) |
0070053570c4
suppress irrelevant timing messages (the majority);
wenzelm
parents:
59058
diff
changeset
|
93 |
else () |
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
94 |
end |
51216 | 95 |
else |
96 |
(case Markup.dest_loading_theory props of |
|
97 |
SOME name => writeln ("\floading_theory = " ^ name) |
|
51661 | 98 |
| NONE => raise Output.Protocol_Message props) |
99 |
| [] => raise Output.Protocol_Message props); |
|
51045
630c0895d9d1
more efficient inlined properties, especially relevant for voluminous tasks trace;
wenzelm
parents:
50982
diff
changeset
|
100 |
|
50683 | 101 |
|
65307 | 102 |
(* build theories *) |
50683 | 103 |
|
61381 | 104 |
fun build_theories symbols last_timing master_dir (options, thys) = |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
105 |
let |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
106 |
val condition = space_explode "," (Options.string options "condition"); |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
107 |
val conds = filter_out (can getenv_strict) condition; |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
108 |
in |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
109 |
if null conds then |
63827
b24d0e53dd03
option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents:
62930
diff
changeset
|
110 |
(if Options.bool options "checkpoint" then ML_Heap.share_common_data () else (); |
b24d0e53dd03
option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents:
62930
diff
changeset
|
111 |
Options.set_default options; |
62714 | 112 |
Isabelle_Process.init_options (); |
64599
80ef54198f44
dummy fork to produce ML_statistics even in sequential mode (e.g. for heap size);
wenzelm
parents:
64308
diff
changeset
|
113 |
Future.fork I; |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
114 |
(Thy_Info.use_theories { |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
115 |
document = Present.document_enabled (Options.string options "document"), |
61381 | 116 |
symbols = symbols, |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
117 |
last_timing = last_timing, |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
118 |
master_dir = master_dir} |
64308 | 119 |
|> |
120 |
(case Options.string options "profiling" of |
|
121 |
"" => I |
|
122 |
| "time" => profile_time |
|
123 |
| "allocations" => profile_allocations |
|
124 |
| bad => error ("Bad profiling option: " ^ quote bad)) |
|
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
125 |
|> Unsynchronized.setmp print_mode |
62714 | 126 |
(space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys) |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
127 |
else |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
128 |
Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
129 |
" (undefined " ^ commas conds ^ ")\n") |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
130 |
end; |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
131 |
|
65307 | 132 |
|
133 |
(* build session *) |
|
134 |
||
135 |
datatype args = Args of |
|
136 |
{symbol_codes: (string * int) list, |
|
137 |
command_timings: Properties.T list, |
|
138 |
do_output: bool, |
|
139 |
verbose: bool, |
|
140 |
browser_info: Path.T, |
|
141 |
document_files: (Path.T * Path.T) list, |
|
142 |
graph_file: Path.T, |
|
143 |
parent_name: string, |
|
144 |
chapter: string, |
|
145 |
name: string, |
|
146 |
master_dir: Path.T, |
|
147 |
theories: (Options.T * (string * Position.T) list) list}; |
|
148 |
||
149 |
fun decode_args yxml = |
|
62630 | 150 |
let |
65307 | 151 |
open XML.Decode; |
62630 | 152 |
val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info, |
65307 | 153 |
(document_files, (graph_file, (parent_name, (chapter, (name, (master_dir, theories))))))))))) = |
154 |
pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string |
|
155 |
(pair (list (pair string string)) (pair string (pair string (pair string (pair string |
|
156 |
(pair string (((list (pair Options.decode (list (string #> rpair Position.none)))))))))))))))) |
|
157 |
(YXML.parse_body yxml); |
|
158 |
in |
|
159 |
Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output, |
|
160 |
verbose = verbose, browser_info = Path.explode browser_info, |
|
161 |
document_files = map (apply2 Path.explode) document_files, |
|
162 |
graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter, |
|
163 |
name = name, master_dir = Path.explode master_dir, theories = theories} |
|
164 |
end; |
|
48418 | 165 |
|
65307 | 166 |
fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info, |
167 |
document_files, graph_file, parent_name, chapter, name, master_dir, theories}) = |
|
168 |
let |
|
62630 | 169 |
val symbols = HTML.make_symbols symbol_codes; |
51941
ead4248aef3b
full default options for Isabelle_Process and Build;
wenzelm
parents:
51666
diff
changeset
|
170 |
|
62630 | 171 |
val _ = writeln ("\fSession.name = " ^ name); |
172 |
val _ = |
|
173 |
Session.init |
|
174 |
symbols |
|
175 |
do_output |
|
176 |
(Options.default_bool "browser_info") |
|
65307 | 177 |
browser_info |
62630 | 178 |
(Options.default_string "document") |
179 |
(Options.default_string "document_output") |
|
180 |
(Present.document_variants (Options.default_string "document_variants")) |
|
65307 | 181 |
document_files |
182 |
graph_file |
|
183 |
parent_name |
|
184 |
(chapter, name) |
|
62630 | 185 |
verbose; |
49911
262c36fd5f26
collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);
wenzelm
parents:
49242
diff
changeset
|
186 |
|
65058
3e9f382fb67e
absent timing information means zero, according to 0070053570c4, f235646b1b73;
wenzelm
parents:
64599
diff
changeset
|
187 |
val last_timing = get_timings (fold update_timings command_timings empty_timings); |
51218
6425a0d3b7ac
support for build passing timings from Scala to ML;
wenzelm
parents:
51217
diff
changeset
|
188 |
|
62630 | 189 |
val res1 = |
190 |
theories |> |
|
65307 | 191 |
(List.app (build_theories symbols last_timing master_dir) |
62630 | 192 |
|> session_timing name verbose |
193 |
|> Exn.capture); |
|
194 |
val res2 = Exn.capture Session.finish (); |
|
195 |
val _ = Par_Exn.release_all [res1, res2]; |
|
65307 | 196 |
in () end; |
48673
b2b09970c571
let with_timing report overall number of threads;
wenzelm
parents:
48672
diff
changeset
|
197 |
|
65307 | 198 |
(*command-line tool*) |
199 |
fun build args_file = |
|
200 |
let |
|
201 |
val _ = SHA1.test_samples (); |
|
202 |
val _ = Options.load_default (); |
|
203 |
val _ = Isabelle_Process.init_options (); |
|
204 |
val args = decode_args (File.read (Path.explode args_file)); |
|
205 |
val _ = |
|
206 |
Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message |
|
207 |
build_session args; |
|
62630 | 208 |
val _ = Options.reset_default (); |
209 |
in () end; |
|
48418 | 210 |
|
65307 | 211 |
(*PIDE version*) |
212 |
val _ = |
|
213 |
Isabelle_Process.protocol_command "build_session" |
|
65313 | 214 |
(fn [args_yxml] => |
65307 | 215 |
let |
65313 | 216 |
val args = decode_args args_yxml; |
65307 | 217 |
val result = (build_session args; "") handle exn => |
218 |
(Runtime.exn_message exn handle _ (*sic!*) => |
|
219 |
"Exception raised, but failed to print details!"); |
|
65313 | 220 |
in Output.protocol_message Markup.build_session_finished [result] end | _ => raise Match); |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
221 |
|
48418 | 222 |
end; |