author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 74822 | a1fa82431576 |
child 75626 | 4879d0021185 |
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 |
73841
95484bd7e1ec
proper profiling within command execution: messages require PIDE id;
wenzelm
parents:
73840
diff
changeset
|
49 |
val _ = ML_Profiling.check_mode (Options.string options "profiling"); |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
50 |
val condition = space_explode "," (Options.string options "condition"); |
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
51 |
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
|
52 |
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
|
53 |
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
|
54 |
(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
|
55 |
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
|
56 |
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
|
57 |
(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
|
58 |
|> 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
|
59 |
(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
|
60 |
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
|
61 |
(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
|
62 |
" (undefined " ^ commas conds ^ ")\n"); []) |
74822
a1fa82431576
clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT (see also 9ead8d9be3ab);
wenzelm
parents:
73841
diff
changeset
|
63 |
in loaded_theories end; |
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
64 |
|
65307 | 65 |
|
66 |
(* build session *) |
|
67 |
||
68 |
val _ = |
|
73225
3ab0cedaccad
clarified modules: allow early definition of protocol commands;
wenzelm
parents:
72640
diff
changeset
|
69 |
Protocol_Command.define "build_session" |
72637 | 70 |
(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
|
71 |
let |
72637 | 72 |
val _ = Resources.init_session_yxml resources_yxml; |
72640
fffad9ad660e
simplified/clarified persistent session information;
wenzelm
parents:
72638
diff
changeset
|
73 |
val (session_name, theories) = |
72103 | 74 |
YXML.parse_body args_yxml |> |
75 |
let |
|
76 |
open XML.Decode; |
|
77 |
val position = Position.of_properties o properties; |
|
72640
fffad9ad660e
simplified/clarified persistent session information;
wenzelm
parents:
72638
diff
changeset
|
78 |
in pair string (list (pair Options.decode (list (pair string position)))) end; |
fffad9ad660e
simplified/clarified persistent session information;
wenzelm
parents:
72638
diff
changeset
|
79 |
|
fffad9ad660e
simplified/clarified persistent session information;
wenzelm
parents:
72638
diff
changeset
|
80 |
val _ = Session.init session_name; |
72103 | 81 |
|
82 |
fun build () = |
|
83 |
let |
|
74822
a1fa82431576
clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT (see also 9ead8d9be3ab);
wenzelm
parents:
73841
diff
changeset
|
84 |
val res = |
72103 | 85 |
theories |> |
74822
a1fa82431576
clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT (see also 9ead8d9be3ab);
wenzelm
parents:
73841
diff
changeset
|
86 |
(map (build_theories session_name) |
72103 | 87 |
|> session_timing |
88 |
|> Exn.capture); |
|
74822
a1fa82431576
clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT (see also 9ead8d9be3ab);
wenzelm
parents:
73841
diff
changeset
|
89 |
val res1 = |
a1fa82431576
clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT (see also 9ead8d9be3ab);
wenzelm
parents:
73841
diff
changeset
|
90 |
(case res of |
a1fa82431576
clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT (see also 9ead8d9be3ab);
wenzelm
parents:
73841
diff
changeset
|
91 |
Exn.Res loaded_theories => |
a1fa82431576
clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT (see also 9ead8d9be3ab);
wenzelm
parents:
73841
diff
changeset
|
92 |
Exn.capture (apply_hooks session_name) (flat loaded_theories) |
a1fa82431576
clarified hook for Mirabelle (again): cover all 'theories' sections within ROOT (see also 9ead8d9be3ab);
wenzelm
parents:
73841
diff
changeset
|
93 |
| Exn.Exn exn => Exn.Exn exn); |
72103 | 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; |