author | wenzelm |
Tue, 17 Nov 2020 22:57:56 +0100 | |
changeset 72638 | 2a7fc87495e0 |
parent 72637 | fd68c9c1b90b |
child 72640 | fffad9ad660e |
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 |
||
52052
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
10 |
(* session timing *) |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
11 |
|
72019 | 12 |
fun session_timing f x = |
52052
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
13 |
let |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
14 |
val start = Timing.start (); |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
15 |
val y = f x; |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
16 |
val timing = Timing.result start; |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
17 |
|
62925 | 18 |
val threads = string_of_int (Multithreading.max_threads ()); |
72019 | 19 |
val props = [("threads", threads)] @ Markup.timing_properties timing; |
20 |
val _ = Output.protocol_message (Markup.session_timing :: props) []; |
|
52052
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
21 |
in y end; |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
22 |
|
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
23 |
|
65307 | 24 |
(* build theories *) |
50683 | 25 |
|
72638
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
26 |
fun build_theories qualifier (options, thys) = |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
27 |
let |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
28 |
val condition = space_explode "," (Options.string options "condition"); |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
29 |
val conds = filter_out (can getenv_strict) condition; |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
30 |
in |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
31 |
if null conds then |
69755 | 32 |
(Options.set_default options; |
62714 | 33 |
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
|
34 |
Future.fork I; |
72638
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
35 |
(Thy_Info.use_theories options qualifier |
64308 | 36 |
|> |
37 |
(case Options.string options "profiling" of |
|
38 |
"" => I |
|
39 |
| "time" => profile_time |
|
40 |
| "allocations" => profile_allocations |
|
41 |
| bad => error ("Bad profiling option: " ^ quote bad)) |
|
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
42 |
|> Unsynchronized.setmp print_mode |
62714 | 43 |
(space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys) |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
44 |
else |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
45 |
Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
46 |
" (undefined " ^ commas conds ^ ")\n") |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
47 |
end; |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
48 |
|
65307 | 49 |
|
50 |
(* build session *) |
|
51 |
||
52 |
val _ = |
|
53 |
Isabelle_Process.protocol_command "build_session" |
|
72637 | 54 |
(fn [resources_yxml, args_yxml] => |
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
55 |
let |
72637 | 56 |
val _ = Resources.init_session_yxml resources_yxml; |
72638
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
57 |
val (parent_name, (chapter, (session_name, theories))) = |
72103 | 58 |
YXML.parse_body args_yxml |> |
59 |
let |
|
60 |
open XML.Decode; |
|
61 |
val position = Position.of_properties o properties; |
|
62 |
in |
|
72638
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
63 |
pair string (pair string (pair string |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
64 |
(list (pair Options.decode (list (pair string position)))))) |
72103 | 65 |
end; |
66 |
||
67 |
fun build () = |
|
68 |
let |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
69 |
val _ = Session.init parent_name (chapter, session_name); |
72103 | 70 |
|
71 |
val res1 = |
|
72 |
theories |> |
|
72638
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
73 |
(List.app (build_theories session_name) |
72103 | 74 |
|> session_timing |
75 |
|> Exn.capture); |
|
76 |
val res2 = Exn.capture Session.finish (); |
|
77 |
||
78 |
val _ = Resources.finish_session_base (); |
|
79 |
val _ = Par_Exn.release_all [res1, res2]; |
|
80 |
val _ = |
|
81 |
if session_name = Context.PureN |
|
82 |
then Theory.install_pure (Thy_Info.get_theory Context.PureN) else (); |
|
83 |
in () end; |
|
84 |
||
71880
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
85 |
fun exec e = |
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
86 |
if can Theory.get_pure () then |
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
87 |
Isabelle_Thread.fork |
71884 | 88 |
{name = "build_session", stack_limit = Isabelle_Thread.stack_limit (), |
89 |
interrupts = false} e |
|
71880
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
90 |
|> ignore |
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
91 |
else e (); |
71667
4d2de35214c5
proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents:
71656
diff
changeset
|
92 |
in |
71880
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
93 |
exec (fn () => |
72103 | 94 |
(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
|
95 |
((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"]))) |
71879 | 96 |
|> 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
|
97 |
|> 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
|
98 |
end |
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
99 |
| _ => raise Match); |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
100 |
|
48418 | 101 |
end; |