author | wenzelm |
Sun, 06 Jun 2021 21:17:23 +0200 | |
changeset 73822 | 1192c68ebe1c |
parent 73821 | 9ead8d9be3ab |
child 73840 | a5200fa7cb4c |
permissions | -rw-r--r-- |
50686 | 1 |
(* Title: Pure/Tools/build.ML |
48418 | 2 |
Author: Makarius |
3 |
||
4 |
Build Isabelle sessions. |
|
5 |
*) |
|
6 |
||
73821
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
7 |
signature BUILD = |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
8 |
sig |
73822
1192c68ebe1c
suppress theories from other sessions, unless explicitly specified via mirabelle_theories;
wenzelm
parents:
73821
diff
changeset
|
9 |
type hook = string -> (theory * Document_Output.segment list) list -> unit |
1192c68ebe1c
suppress theories from other sessions, unless explicitly specified via mirabelle_theories;
wenzelm
parents:
73821
diff
changeset
|
10 |
val add_hook: hook -> unit |
73821
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
11 |
end; |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
12 |
|
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
13 |
structure Build: BUILD = |
48418 | 14 |
struct |
15 |
||
52052
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
16 |
(* session timing *) |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
17 |
|
72019 | 18 |
fun session_timing f x = |
52052
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
19 |
let |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
20 |
val start = Timing.start (); |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
21 |
val y = f x; |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
22 |
val timing = Timing.result start; |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
23 |
|
62925 | 24 |
val threads = string_of_int (Multithreading.max_threads ()); |
72019 | 25 |
val props = [("threads", threads)] @ Markup.timing_properties timing; |
26 |
val _ = Output.protocol_message (Markup.session_timing :: props) []; |
|
52052
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
27 |
in y end; |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
28 |
|
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52041
diff
changeset
|
29 |
|
65307 | 30 |
(* build theories *) |
50683 | 31 |
|
73822
1192c68ebe1c
suppress theories from other sessions, unless explicitly specified via mirabelle_theories;
wenzelm
parents:
73821
diff
changeset
|
32 |
type hook = string -> (theory * Document_Output.segment list) list -> unit; |
1192c68ebe1c
suppress theories from other sessions, unless explicitly specified via mirabelle_theories;
wenzelm
parents:
73821
diff
changeset
|
33 |
|
73821
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
34 |
local |
73822
1192c68ebe1c
suppress theories from other sessions, unless explicitly specified via mirabelle_theories;
wenzelm
parents:
73821
diff
changeset
|
35 |
val hooks = Synchronized.var "Build.hooks" ([]: hook list); |
73821
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
36 |
in |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
37 |
|
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
38 |
fun add_hook hook = Synchronized.change hooks (cons hook); |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
39 |
|
73822
1192c68ebe1c
suppress theories from other sessions, unless explicitly specified via mirabelle_theories;
wenzelm
parents:
73821
diff
changeset
|
40 |
fun apply_hooks qualifier loaded_theories = |
73821
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
41 |
Synchronized.value hooks |
73822
1192c68ebe1c
suppress theories from other sessions, unless explicitly specified via mirabelle_theories;
wenzelm
parents:
73821
diff
changeset
|
42 |
|> List.app (fn hook => hook qualifier loaded_theories); |
73821
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
43 |
|
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
44 |
end; |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
45 |
|
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
46 |
|
72638
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
47 |
fun build_theories qualifier (options, thys) = |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
48 |
let |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
49 |
val condition = space_explode "," (Options.string options "condition"); |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
50 |
val conds = filter_out (can getenv_strict) condition; |
73821
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
51 |
val loaded_theories = |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
52 |
if null conds then |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
53 |
(Options.set_default options; |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
54 |
Isabelle_Process.init_options (); |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
55 |
Future.fork I; |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
56 |
(Thy_Info.use_theories options qualifier |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
57 |
|> |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
58 |
(case Options.string options "profiling" of |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
59 |
"" => I |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
60 |
| "time" => profile_time |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
61 |
| "allocations" => profile_allocations |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
62 |
| bad => error ("Bad profiling option: " ^ quote bad)) |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
63 |
|> Unsynchronized.setmp print_mode |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
64 |
(space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys) |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
65 |
else |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
66 |
(Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ |
9ead8d9be3ab
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
wenzelm
parents:
73559
diff
changeset
|
67 |
" (undefined " ^ commas conds ^ ")\n"); []) |
73822
1192c68ebe1c
suppress theories from other sessions, unless explicitly specified via mirabelle_theories;
wenzelm
parents:
73821
diff
changeset
|
68 |
in apply_hooks qualifier loaded_theories end; |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
69 |
|
65307 | 70 |
|
71 |
(* build session *) |
|
72 |
||
73 |
val _ = |
|
73225
3ab0cedaccad
clarified modules: allow early definition of protocol commands;
wenzelm
parents:
72640
diff
changeset
|
74 |
Protocol_Command.define "build_session" |
72637 | 75 |
(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
|
76 |
let |
72637 | 77 |
val _ = Resources.init_session_yxml resources_yxml; |
72640
fffad9ad660e
simplified/clarified persistent session information;
wenzelm
parents:
72638
diff
changeset
|
78 |
val (session_name, theories) = |
72103 | 79 |
YXML.parse_body args_yxml |> |
80 |
let |
|
81 |
open XML.Decode; |
|
82 |
val position = Position.of_properties o properties; |
|
72640
fffad9ad660e
simplified/clarified persistent session information;
wenzelm
parents:
72638
diff
changeset
|
83 |
in pair string (list (pair Options.decode (list (pair string position)))) end; |
fffad9ad660e
simplified/clarified persistent session information;
wenzelm
parents:
72638
diff
changeset
|
84 |
|
fffad9ad660e
simplified/clarified persistent session information;
wenzelm
parents:
72638
diff
changeset
|
85 |
val _ = Session.init session_name; |
72103 | 86 |
|
87 |
fun build () = |
|
88 |
let |
|
89 |
val res1 = |
|
90 |
theories |> |
|
72638
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
91 |
(List.app (build_theories session_name) |
72103 | 92 |
|> session_timing |
93 |
|> Exn.capture); |
|
94 |
val res2 = Exn.capture Session.finish (); |
|
95 |
||
96 |
val _ = Resources.finish_session_base (); |
|
97 |
val _ = Par_Exn.release_all [res1, res2]; |
|
98 |
val _ = |
|
99 |
if session_name = Context.PureN |
|
100 |
then Theory.install_pure (Thy_Info.get_theory Context.PureN) else (); |
|
101 |
in () end; |
|
102 |
||
71880
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
103 |
fun exec e = |
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
104 |
if can Theory.get_pure () then |
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
105 |
Isabelle_Thread.fork |
71884 | 106 |
{name = "build_session", stack_limit = Isabelle_Thread.stack_limit (), |
107 |
interrupts = false} e |
|
71880
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
108 |
|> ignore |
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
109 |
else e (); |
71667
4d2de35214c5
proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;
wenzelm
parents:
71656
diff
changeset
|
110 |
in |
71880
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
111 |
exec (fn () => |
72103 | 112 |
(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
|
113 |
((1, Runtime.exn_message_list exn) handle _ (*sic!*) => (2, ["CRASHED"]))) |
71879 | 114 |
|> let open XML.Encode in pair int (list string) end |
73559 | 115 |
|> single |
71880
0ca353521753
asynchronous build_session: notably for Scala.fulfill protocol commands during run;
wenzelm
parents:
71879
diff
changeset
|
116 |
|> 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
|
117 |
end |
70991
f9f7c34b7dd4
more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents:
70907
diff
changeset
|
118 |
| _ => raise Match); |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
119 |
|
48418 | 120 |
end; |