author | wenzelm |
Mon, 16 Nov 2020 22:23:04 +0100 | |
changeset 72622 | 830222403681 |
parent 72620 | 429afd0d1a79 |
child 72624 | 35524fade6a4 |
permissions | -rw-r--r-- |
50686 | 1 |
(* Title: Pure/Tools/build.ML |
48418 | 2 |
Author: Makarius |
3 |
||
4 |
Build Isabelle sessions. |
|
5 |
*) |
|
6 |
||
72103 | 7 |
structure Build: sig end = |
48418 | 8 |
struct |
9 |
||
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
10 |
(* command timings *) |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
11 |
|
56615 | 12 |
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
|
13 |
|
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
14 |
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
|
15 |
|
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
16 |
fun update_timings props = |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
17 |
(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
|
18 |
SOME ({file, offset, name}, time) => |
51666
b97aeb018900
add command timings (like document command status);
wenzelm
parents:
51662
diff
changeset
|
19 |
Symtab.map_default (file, Inttab.empty) |
62826 | 20 |
(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
|
21 |
| NONE => I); |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
22 |
|
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
23 |
fun approximative_id name pos = |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
24 |
(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
|
25 |
(SOME file, SOME offset) => |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
26 |
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
|
27 |
| _ => NONE); |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
28 |
|
65058
3e9f382fb67e
absent timing information means zero, according to 0070053570c4, f235646b1b73;
wenzelm
parents:
64599
diff
changeset
|
29 |
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
|
30 |
(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
|
31 |
SOME {file, offset, name} => |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
32 |
(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
|
33 |
SOME offsets => |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
34 |
(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
|
35 |
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
|
36 |
| NONE => NONE) |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
37 |
| NONE => NONE) |
65058
3e9f382fb67e
absent timing information means zero, according to 0070053570c4, f235646b1b73;
wenzelm
parents:
64599
diff
changeset
|
38 |
| NONE => NONE) |
3e9f382fb67e
absent timing information means zero, according to 0070053570c4, f235646b1b73;
wenzelm
parents:
64599
diff
changeset
|
39 |
|> the_default Time.zeroTime; |
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
40 |
|
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset
|
41 |
|
52052
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
42 |
(* session timing *) |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
43 |
|
72019 | 44 |
fun session_timing f x = |
52052
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
45 |
let |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
46 |
val start = Timing.start (); |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
47 |
val y = f x; |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
48 |
val timing = Timing.result start; |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
49 |
|
62925 | 50 |
val threads = string_of_int (Multithreading.max_threads ()); |
72019 | 51 |
val props = [("threads", threads)] @ Markup.timing_properties timing; |
52 |
val _ = Output.protocol_message (Markup.session_timing :: props) []; |
|
52052
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
53 |
in y end; |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
54 |
|
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
55 |
|
65307 | 56 |
(* build theories *) |
50683 | 57 |
|
72620 | 58 |
fun build_theories last_timing qualifier master_dir (options, thys) = |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
59 |
let |
72620 | 60 |
val context = {options = options, last_timing = last_timing}; |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
61 |
val condition = space_explode "," (Options.string options "condition"); |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
62 |
val conds = filter_out (can getenv_strict) condition; |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
63 |
in |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
64 |
if null conds then |
69755 | 65 |
(Options.set_default options; |
62714 | 66 |
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
|
67 |
Future.fork I; |
68179
da70c9e91135
clarified signature: more explicit type "context" with full options;
wenzelm
parents:
68148
diff
changeset
|
68 |
(Thy_Info.use_theories context qualifier master_dir |
64308 | 69 |
|> |
70 |
(case Options.string options "profiling" of |
|
71 |
"" => I |
|
72 |
| "time" => profile_time |
|
73 |
| "allocations" => profile_allocations |
|
74 |
| bad => error ("Bad profiling option: " ^ quote bad)) |
|
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
75 |
|> Unsynchronized.setmp print_mode |
62714 | 76 |
(space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys) |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
77 |
else |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
78 |
Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
79 |
" (undefined " ^ commas conds ^ ")\n") |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
80 |
end; |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
81 |
|
65307 | 82 |
|
83 |
(* build session *) |
|
84 |
||
85 |
val _ = |
|
86 |
Isabelle_Process.protocol_command "build_session" |
|
65313 | 87 |
(fn [args_yxml] => |
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
88 |
let |
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
89 |
val (html_symbols, (command_timings, (parent_name, (chapter, |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
90 |
(session_name, (master_dir, (theories, (session_positions, (session_directories, |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
91 |
(session_chapters, (doc_names, |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
92 |
(global_theories, (loaded_theories, bibtex_entries))))))))))))) = |
72103 | 93 |
YXML.parse_body args_yxml |> |
94 |
let |
|
95 |
open XML.Decode; |
|
96 |
val position = Position.of_properties o properties; |
|
97 |
val path = Path.explode o string; |
|
98 |
in |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
99 |
pair (list (pair string int)) (pair (list properties) (pair string (pair string |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
100 |
(pair string (pair path |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
101 |
(pair (((list (pair Options.decode (list (pair string position)))))) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
102 |
(pair (list (pair string properties)) (pair (list (pair string string)) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
103 |
(pair (list (pair string string)) (pair (list string) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
104 |
(pair (list (pair string string)) (pair (list string) |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
105 |
(list (pair string (list string))))))))))))))) |
72103 | 106 |
end; |
107 |
||
108 |
fun build () = |
|
109 |
let |
|
110 |
val _ = |
|
111 |
Resources.init_session |
|
72620 | 112 |
{html_symbols = html_symbols, |
113 |
session_positions = session_positions, |
|
72103 | 114 |
session_directories = session_directories, |
72616 | 115 |
session_chapters = session_chapters, |
72613
d01ea9e3bd2d
clarified bibtex_entries: refer to overall session structure;
wenzelm
parents:
72574
diff
changeset
|
116 |
bibtex_entries = bibtex_entries, |
72103 | 117 |
docs = doc_names, |
118 |
global_theories = global_theories, |
|
119 |
loaded_theories = loaded_theories}; |
|
120 |
||
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
121 |
val _ = Session.init parent_name (chapter, session_name); |
72103 | 122 |
|
123 |
val last_timing = get_timings (fold update_timings command_timings empty_timings); |
|
124 |
||
125 |
val res1 = |
|
126 |
theories |> |
|
72620 | 127 |
(List.app (build_theories last_timing session_name master_dir) |
72103 | 128 |
|> session_timing |
129 |
|> Exn.capture); |
|
130 |
val res2 = Exn.capture Session.finish (); |
|
131 |
||
132 |
val _ = Resources.finish_session_base (); |
|
133 |
val _ = Par_Exn.release_all [res1, res2]; |
|
134 |
val _ = |
|
135 |
if session_name = Context.PureN |
|
136 |
then Theory.install_pure (Thy_Info.get_theory Context.PureN) else (); |
|
137 |
in () end; |
|
138 |
||
71880
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
139 |
fun exec e = |
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
140 |
if can Theory.get_pure () then |
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
141 |
Isabelle_Thread.fork |
71884 | 142 |
{name = "build_session", stack_limit = Isabelle_Thread.stack_limit (), |
143 |
interrupts = false} e |
|
71880
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
144 |
|> ignore |
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
145 |
else e (); |
71667
4d2de35214c5
proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents:
71656
diff
changeset
|
146 |
in |
71880
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
147 |
exec (fn () => |
72103 | 148 |
(Future.interruptible_task (fn () => (build (); (0, []))) () handle exn => |
71880
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
149 |
((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"]))) |
71879 | 150 |
|> let open XML.Encode in pair int (list string) end |
71880
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
151 |
|> Output.protocol_message Markup.build_session_finished) |
71667
4d2de35214c5
proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents:
71656
diff
changeset
|
152 |
end |
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
153 |
| _ => raise Match); |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
154 |
|
48418 | 155 |
end; |