author | wenzelm |
Sat, 28 Mar 2020 19:11:59 +0100 | |
changeset 71611 | fb6953e77000 |
parent 70991 | f9f7c34b7dd4 |
child 71613 | 6bce25f9d0ab |
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 |
||
72 |
fun protocol_message props output = |
|
51216 | 73 |
(case props of |
74 |
function :: args => |
|
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
75 |
if function = Markup.ML_statistics orelse function = Markup.task_statistics then |
70907 | 76 |
Protocol_Message.inline (#2 function) args |
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
77 |
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
|
78 |
let |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
79 |
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
|
80 |
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
|
81 |
val {elapsed, ...} = Markup.parse_timing_properties args; |
62793
f235646b1b73
less bulky timing information, e.g. HOL 56913 ~> 672;
wenzelm
parents:
62715
diff
changeset
|
82 |
val is_significant = |
f235646b1b73
less bulky timing information, e.g. HOL 56913 ~> 672;
wenzelm
parents:
62715
diff
changeset
|
83 |
Timing.is_relevant_time elapsed andalso |
62826 | 84 |
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
|
85 |
in |
62793
f235646b1b73
less bulky timing information, e.g. HOL 56913 ~> 672;
wenzelm
parents:
62715
diff
changeset
|
86 |
if is_significant then |
59149
0070053570c4
suppress irrelevant timing messages (the majority);
wenzelm
parents:
59058
diff
changeset
|
87 |
(case approximative_id name pos of |
70907 | 88 |
SOME id => |
89 |
Protocol_Message.inline (#2 function) (Markup.command_timing_properties id elapsed) |
|
59149
0070053570c4
suppress irrelevant timing messages (the majority);
wenzelm
parents:
59058
diff
changeset
|
90 |
| NONE => ()) |
0070053570c4
suppress irrelevant timing messages (the majority);
wenzelm
parents:
59058
diff
changeset
|
91 |
else () |
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
92 |
end |
66873
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66712
diff
changeset
|
93 |
else if function = Markup.theory_timing then |
70907 | 94 |
Protocol_Message.inline (#2 function) args |
51216 | 95 |
else |
96 |
(case Markup.dest_loading_theory props of |
|
97 |
SOME name => writeln ("\floading_theory = " ^ name) |
|
70907 | 98 |
| NONE => Export.protocol_message props output) |
51661 | 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 |
|
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67219
diff
changeset
|
104 |
fun build_theories symbols bibtex_entries last_timing qualifier master_dir (options, thys) = |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
105 |
let |
68179
da70c9e91135
clarified signature: more explicit type "context" with full options;
wenzelm
parents:
68148
diff
changeset
|
106 |
val context = |
da70c9e91135
clarified signature: more explicit type "context" with full options;
wenzelm
parents:
68148
diff
changeset
|
107 |
{options = options, symbols = symbols, bibtex_entries = bibtex_entries, |
da70c9e91135
clarified signature: more explicit type "context" with full options;
wenzelm
parents:
68148
diff
changeset
|
108 |
last_timing = last_timing}; |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
109 |
val condition = space_explode "," (Options.string options "condition"); |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
110 |
val conds = filter_out (can getenv_strict) condition; |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
111 |
in |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
112 |
if null conds then |
69755 | 113 |
(Options.set_default options; |
62714 | 114 |
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
|
115 |
Future.fork I; |
68179
da70c9e91135
clarified signature: more explicit type "context" with full options;
wenzelm
parents:
68148
diff
changeset
|
116 |
(Thy_Info.use_theories context qualifier master_dir |
64308 | 117 |
|> |
118 |
(case Options.string options "profiling" of |
|
119 |
"" => I |
|
120 |
| "time" => profile_time |
|
121 |
| "allocations" => profile_allocations |
|
122 |
| bad => error ("Bad profiling option: " ^ quote bad)) |
|
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
123 |
|> Unsynchronized.setmp print_mode |
62714 | 124 |
(space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys) |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
125 |
else |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
126 |
Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
127 |
" (undefined " ^ commas conds ^ ")\n") |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
128 |
end; |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
129 |
|
65307 | 130 |
|
131 |
(* build session *) |
|
132 |
||
133 |
datatype args = Args of |
|
134 |
{symbol_codes: (string * int) list, |
|
135 |
command_timings: Properties.T list, |
|
136 |
verbose: bool, |
|
137 |
browser_info: Path.T, |
|
138 |
document_files: (Path.T * Path.T) list, |
|
139 |
graph_file: Path.T, |
|
140 |
parent_name: string, |
|
141 |
chapter: string, |
|
142 |
name: string, |
|
143 |
master_dir: Path.T, |
|
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65318
diff
changeset
|
144 |
theories: (Options.T * (string * Position.T) list) list, |
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
69755
diff
changeset
|
145 |
session_positions: (string * Properties.T) list, |
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
69755
diff
changeset
|
146 |
session_directories: (string * string) list, |
67471 | 147 |
doc_names: string list, |
65457 | 148 |
global_theories: (string * string) list, |
66712 | 149 |
loaded_theories: string list, |
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67219
diff
changeset
|
150 |
bibtex_entries: string list}; |
65307 | 151 |
|
152 |
fun decode_args yxml = |
|
62630 | 153 |
let |
65307 | 154 |
open XML.Decode; |
65517 | 155 |
val position = Position.of_properties o properties; |
71611
fb6953e77000
eliminated pointless flag (see also 6533ceee4cd7);
wenzelm
parents:
70991
diff
changeset
|
156 |
val (symbol_codes, (command_timings, (verbose, (browser_info, |
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65318
diff
changeset
|
157 |
(document_files, (graph_file, (parent_name, (chapter, (name, (master_dir, |
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
69755
diff
changeset
|
158 |
(theories, (session_positions, (session_directories, (doc_names, (global_theories, |
71611
fb6953e77000
eliminated pointless flag (see also 6533ceee4cd7);
wenzelm
parents:
70991
diff
changeset
|
159 |
(loaded_theories, bibtex_entries)))))))))))))))) = |
fb6953e77000
eliminated pointless flag (see also 6533ceee4cd7);
wenzelm
parents:
70991
diff
changeset
|
160 |
pair (list (pair string int)) (pair (list properties) (pair bool (pair string |
65307 | 161 |
(pair (list (pair string string)) (pair string (pair string (pair string (pair string |
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65318
diff
changeset
|
162 |
(pair string |
65517 | 163 |
(pair (((list (pair Options.decode (list (pair string position)))))) |
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
69755
diff
changeset
|
164 |
(pair (list (pair string properties)) |
67493
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67471
diff
changeset
|
165 |
(pair (list (pair string string)) (pair (list string) |
71611
fb6953e77000
eliminated pointless flag (see also 6533ceee4cd7);
wenzelm
parents:
70991
diff
changeset
|
166 |
(pair (list (pair string string)) (pair (list string) (list string)))))))))))))))) |
65307 | 167 |
(YXML.parse_body yxml); |
168 |
in |
|
71611
fb6953e77000
eliminated pointless flag (see also 6533ceee4cd7);
wenzelm
parents:
70991
diff
changeset
|
169 |
Args {symbol_codes = symbol_codes, command_timings = command_timings, |
65307 | 170 |
verbose = verbose, browser_info = Path.explode browser_info, |
171 |
document_files = map (apply2 Path.explode) document_files, |
|
172 |
graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter, |
|
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
69755
diff
changeset
|
173 |
name = name, master_dir = Path.explode master_dir, theories = theories, |
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
69755
diff
changeset
|
174 |
session_positions = session_positions, session_directories = session_directories, |
67471 | 175 |
doc_names = doc_names, global_theories = global_theories, loaded_theories = loaded_theories, |
70712
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
176 |
bibtex_entries = bibtex_entries} |
65307 | 177 |
end; |
48418 | 178 |
|
71611
fb6953e77000
eliminated pointless flag (see also 6533ceee4cd7);
wenzelm
parents:
70991
diff
changeset
|
179 |
fun build_session (Args {symbol_codes, command_timings, verbose, browser_info, |
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
69755
diff
changeset
|
180 |
document_files, graph_file, parent_name, chapter, name, master_dir, theories, session_positions, |
70712
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
181 |
session_directories, doc_names, global_theories, loaded_theories, bibtex_entries}) = |
65307 | 182 |
let |
62630 | 183 |
val symbols = HTML.make_symbols symbol_codes; |
51941
ead4248aef3b
full default options for Isabelle_Process and Build;
wenzelm
parents:
51666
diff
changeset
|
184 |
|
65441 | 185 |
val _ = |
65478
7c40477e0a87
clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
wenzelm
parents:
65457
diff
changeset
|
186 |
Resources.init_session_base |
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
69755
diff
changeset
|
187 |
{session_positions = session_positions, |
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
69755
diff
changeset
|
188 |
session_directories = session_directories, |
67493
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67471
diff
changeset
|
189 |
docs = doc_names, |
67219 | 190 |
global_theories = global_theories, |
70712
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
191 |
loaded_theories = loaded_theories}; |
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65318
diff
changeset
|
192 |
|
62630 | 193 |
val _ = |
194 |
Session.init |
|
195 |
symbols |
|
196 |
(Options.default_bool "browser_info") |
|
65307 | 197 |
browser_info |
62630 | 198 |
(Options.default_string "document") |
199 |
(Options.default_string "document_output") |
|
68511 | 200 |
(Present.document_variants (Options.default ())) |
65307 | 201 |
document_files |
202 |
graph_file |
|
203 |
parent_name |
|
204 |
(chapter, name) |
|
62630 | 205 |
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
|
206 |
|
65058
3e9f382fb67e
absent timing information means zero, according to 0070053570c4, f235646b1b73;
wenzelm
parents:
64599
diff
changeset
|
207 |
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
|
208 |
|
62630 | 209 |
val res1 = |
210 |
theories |> |
|
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67219
diff
changeset
|
211 |
(List.app (build_theories symbols bibtex_entries last_timing name master_dir) |
62630 | 212 |
|> session_timing name verbose |
213 |
|> Exn.capture); |
|
214 |
val res2 = Exn.capture Session.finish (); |
|
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65318
diff
changeset
|
215 |
|
65478
7c40477e0a87
clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
wenzelm
parents:
65457
diff
changeset
|
216 |
val _ = Resources.finish_session_base (); |
62630 | 217 |
val _ = Par_Exn.release_all [res1, res2]; |
65307 | 218 |
in () end; |
48673
b2b09970c571
let with_timing report overall number of threads;
wenzelm
parents:
48672
diff
changeset
|
219 |
|
65307 | 220 |
(*command-line tool*) |
221 |
fun build args_file = |
|
222 |
let |
|
223 |
val _ = SHA1.test_samples (); |
|
224 |
val _ = Options.load_default (); |
|
225 |
val _ = Isabelle_Process.init_options (); |
|
65936 | 226 |
val args = decode_args (File.read (Path.explode args_file)); |
66048
d244a895da50
avoid markup, for the sake of Build_Log.Log_File.parse_props;
wenzelm
parents:
65948
diff
changeset
|
227 |
fun error_message msg = writeln ("\ferror_message = " ^ encode_lines (YXML.content_of msg)); |
65307 | 228 |
val _ = |
229 |
Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message |
|
65934 | 230 |
build_session args |
65948 | 231 |
handle exn => (List.app error_message (Runtime.exn_message_list exn); Exn.reraise exn); |
70907 | 232 |
val _ = Private_Output.protocol_message_fn := Output.protocol_message_undefined; |
62630 | 233 |
val _ = Options.reset_default (); |
234 |
in () end; |
|
48418 | 235 |
|
65307 | 236 |
(*PIDE version*) |
237 |
val _ = |
|
238 |
Isabelle_Process.protocol_command "build_session" |
|
65313 | 239 |
(fn [args_yxml] => |
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
240 |
let |
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
241 |
val args = decode_args args_yxml; |
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
242 |
val result = (build_session args; "") handle exn => |
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
243 |
(Runtime.exn_message exn handle _ (*sic!*) => |
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
244 |
"Exception raised, but failed to print details!"); |
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
245 |
in Output.protocol_message Markup.build_session_finished [XML.Text result] end |
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
246 |
| _ => raise Match); |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
247 |
|
48418 | 248 |
end; |