author | wenzelm |
Fri, 17 May 2013 17:11:06 +0200 | |
changeset 52050 | b40ed9dcf903 |
parent 51948 | cb5dbc9a06f9 |
child 52052 | 892061142ba6 |
permissions | -rw-r--r-- |
30173
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
29435
diff
changeset
|
1 |
(* Title: Pure/System/session.ML |
6346 | 2 |
Author: Markus Wenzel, TU Muenchen |
3 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
4 |
Session management -- internal state of logic images. |
6346 | 5 |
*) |
6 |
||
7 |
signature SESSION = |
|
8 |
sig |
|
11509 | 9 |
val name: unit -> string |
6346 | 10 |
val welcome: unit -> string |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
11 |
val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list -> |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
12 |
string -> string * string -> bool * string -> bool -> unit |
48457 | 13 |
val finish: unit -> unit |
14 |
val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b |
|
48445 | 15 |
val use_dir: string -> string -> bool -> string list -> bool -> bool -> string -> |
31688 | 16 |
string -> bool -> string list -> string -> string -> bool * string -> |
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
39733
diff
changeset
|
17 |
string -> int -> bool -> bool -> int -> int -> int -> int -> unit |
6346 | 18 |
end; |
19 |
||
20 |
structure Session: SESSION = |
|
21 |
struct |
|
22 |
||
23 |
(* session state *) |
|
24 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
25 |
val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"}; |
32738 | 26 |
val session_finished = Unsynchronized.ref false; |
48542 | 27 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
28 |
fun name () = "Isabelle/" ^ #name (! session); |
30173
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
29435
diff
changeset
|
29 |
|
26109
c69c3559355b
more elaborate structure Distribution (filled-in by makedist);
wenzelm
parents:
25840
diff
changeset
|
30 |
fun welcome () = |
26134 | 31 |
if Distribution.is_official then |
32 |
"Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")" |
|
48990 | 33 |
else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")"; |
6346 | 34 |
|
35 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
36 |
(* init *) |
9414 | 37 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
38 |
fun init build info info_path doc doc_graph doc_output doc_variants |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
39 |
parent (chapter, name) doc_dump verbose = |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
40 |
if #name (! session) <> parent orelse not (! session_finished) then |
6346 | 41 |
error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
42 |
else |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
43 |
let |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
44 |
val _ = session := {chapter = chapter, name = name}; |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
45 |
val _ = session_finished := false; |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
46 |
in |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
47 |
Present.init build info info_path (if doc = "false" then "" else doc) |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
48 |
doc_graph doc_output doc_variants (chapter, name) |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
49 |
doc_dump verbose (map Thy_Info.get_theory (Thy_Info.get_names ())) |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
50 |
end; |
6346 | 51 |
|
52 |
||
53 |
(* finish *) |
|
54 |
||
55 |
fun finish () = |
|
51276 | 56 |
(Goal.shutdown_futures (); |
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:
49895
diff
changeset
|
57 |
Thy_Info.finish (); |
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:
49895
diff
changeset
|
58 |
Present.finish (); |
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:
49895
diff
changeset
|
59 |
Keyword.status (); |
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:
49895
diff
changeset
|
60 |
Outer_Syntax.check_syntax (); |
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:
49895
diff
changeset
|
61 |
Options.reset_default (); |
50430
702278df3b57
make double-sure that the future scheduler is properly shutdown, otherwise its threads are made persistent and will deadlock with the fresh instance after reloading the image (NB: Present.finish involves another Par_List.map over document_variants and thus might fork again);
wenzelm
parents:
50121
diff
changeset
|
62 |
Future.shutdown (); |
52050 | 63 |
Event_Timer.shutdown (); |
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:
49895
diff
changeset
|
64 |
session_finished := true); |
6346 | 65 |
|
66 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
67 |
(* timing within ML *) |
6346 | 68 |
|
50777 | 69 |
fun with_timing name verbose f x = |
70 |
let |
|
71 |
val start = Timing.start (); |
|
72 |
val y = f x; |
|
73 |
val timing = Timing.result start; |
|
74 |
||
75 |
val threads = string_of_int (Multithreading.max_threads_value ()); |
|
76 |
val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) |
|
77 |
|> Real.fmt (StringCvt.FIX (SOME 2)); |
|
78 |
||
51045
630c0895d9d1
more efficient inlined properties, especially relevant for voluminous tasks trace;
wenzelm
parents:
50781
diff
changeset
|
79 |
val timing_props = |
630c0895d9d1
more efficient inlined properties, especially relevant for voluminous tasks trace;
wenzelm
parents:
50781
diff
changeset
|
80 |
[("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)]; |
630c0895d9d1
more efficient inlined properties, especially relevant for voluminous tasks trace;
wenzelm
parents:
50781
diff
changeset
|
81 |
val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props)); |
50777 | 82 |
val _ = |
83 |
if verbose then |
|
84 |
Output.physical_stderr ("Timing " ^ name ^ " (" ^ |
|
85 |
threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n") |
|
86 |
else (); |
|
87 |
in y end; |
|
48457 | 88 |
|
89 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
90 |
(* use_dir *) |
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset
|
91 |
|
48804
6348e5fca42e
more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents:
48709
diff
changeset
|
92 |
fun read_variants strs = |
6348e5fca42e
more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents:
48709
diff
changeset
|
93 |
rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs))) |
6348e5fca42e
more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents:
48709
diff
changeset
|
94 |
|> filter_out (fn (_, s) => s = "-"); |
6348e5fca42e
more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents:
48709
diff
changeset
|
95 |
|
48445 | 96 |
fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent |
50121
97d2b77313a0
isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
wenzelm
parents:
49931
diff
changeset
|
97 |
name doc_dump rpath level timing verbose max_threads trace_threads |
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51399
diff
changeset
|
98 |
parallel_proofs parallel_subproofs_saturation = |
23972 | 99 |
((fn () => |
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:
49895
diff
changeset
|
100 |
let |
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:
49895
diff
changeset
|
101 |
val _ = |
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:
49895
diff
changeset
|
102 |
Output.physical_stderr |
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:
49895
diff
changeset
|
103 |
"### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n"; |
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:
49895
diff
changeset
|
104 |
val _ = |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
105 |
if not reset then () |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
106 |
else Output.physical_stderr "### Ignoring reset (historic usedir option -r)\n"; |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
107 |
val _ = |
51398
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51276
diff
changeset
|
108 |
if rpath = "" then () |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
109 |
else Output.physical_stderr "### Ignoring remote path (historic usedir option -P)\n"; |
51398
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51276
diff
changeset
|
110 |
|
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51276
diff
changeset
|
111 |
val _ = |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
112 |
init build info (Path.explode info_path) doc doc_graph "" (read_variants doc_variants) |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
113 |
parent ("Unsorted", name) doc_dump 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:
49895
diff
changeset
|
114 |
val res1 = (use |> with_timing item timing |> Exn.capture) root; |
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:
49895
diff
changeset
|
115 |
val res2 = Exn.capture finish (); |
51948
cb5dbc9a06f9
load options for regular isabelle-process, not just for Isar loop (relevant for numerous low-level tools) -- NB: Isabelle_Process manages options via protocol message;
wenzelm
parents:
51423
diff
changeset
|
116 |
val _ = ignore (Par_Exn.release_all [res1, res2]); |
cb5dbc9a06f9
load options for regular isabelle-process, not just for Isar loop (relevant for numerous low-level tools) -- NB: Isabelle_Process manages options via protocol message;
wenzelm
parents:
51423
diff
changeset
|
117 |
val _ = Options.reset_default (); |
cb5dbc9a06f9
load options for regular isabelle-process, not just for Isar loop (relevant for numerous low-level tools) -- NB: Isabelle_Process manages options via protocol message;
wenzelm
parents:
51423
diff
changeset
|
118 |
in () end) |
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
37216
diff
changeset
|
119 |
|> Unsynchronized.setmp Proofterm.proofs level |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
37216
diff
changeset
|
120 |
|> Unsynchronized.setmp print_mode (modes @ print_mode_value ()) |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
37216
diff
changeset
|
121 |
|> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs |
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51399
diff
changeset
|
122 |
|> Unsynchronized.setmp Goal.parallel_subproofs_saturation parallel_subproofs_saturation |
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
37216
diff
changeset
|
123 |
|> Unsynchronized.setmp Multithreading.trace trace_threads |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
37216
diff
changeset
|
124 |
|> Unsynchronized.setmp Multithreading.max_threads |
23979 | 125 |
(if Multithreading.available then max_threads |
126 |
else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) () |
|
31478 | 127 |
handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1); |
6346 | 128 |
|
129 |
end; |