author  wenzelm 
Tue, 12 Mar 2013 16:47:24 +0100  
changeset 51399  6ac3c29a300e 
parent 51398  c3d02b3518c2 
child 51423  e5f9a6d9ca82 
permissions  rwrr 
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 (filledin 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 doublesure 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 (); 
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

63 
session_finished := true); 
6346  64 

65 

51399
6ac3c29a300e
discontinued "isabelle usedir" option r (reset session path);
wenzelm
parents:
51398
diff
changeset

66 
(* timing within ML *) 
6346  67 

50777  68 
fun with_timing name verbose f x = 
69 
let 

70 
val start = Timing.start (); 

71 
val y = f x; 

72 
val timing = Timing.result start; 

73 

74 
val threads = string_of_int (Multithreading.max_threads_value ()); 

75 
val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) 

76 
> Real.fmt (StringCvt.FIX (SOME 2)); 

77 

51045
630c0895d9d1
more efficient inlined properties, especially relevant for voluminous tasks trace;
wenzelm
parents:
50781
diff
changeset

78 
val timing_props = 
630c0895d9d1
more efficient inlined properties, especially relevant for voluminous tasks trace;
wenzelm
parents:
50781
diff
changeset

79 
[("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)]; 
630c0895d9d1
more efficient inlined properties, especially relevant for voluminous tasks trace;
wenzelm
parents:
50781
diff
changeset

80 
val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props)); 
50777  81 
val _ = 
82 
if verbose then 

83 
Output.physical_stderr ("Timing " ^ name ^ " (" ^ 

84 
threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n") 

85 
else (); 

86 
in y end; 

48457  87 

88 

51399
6ac3c29a300e
discontinued "isabelle usedir" option r (reset session path);
wenzelm
parents:
51398
diff
changeset

89 
(* use_dir *) 
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

90 

48804
6348e5fca42e
more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents:
48709
diff
changeset

91 
fun read_variants strs = 
6348e5fca42e
more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents:
48709
diff
changeset

92 
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

93 
> filter_out (fn (_, s) => s = ""); 
6348e5fca42e
more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents:
48709
diff
changeset

94 

48445  95 
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

96 
name doc_dump rpath level timing verbose max_threads trace_threads 
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
39733
diff
changeset

97 
parallel_proofs parallel_proofs_threshold = 
23972  98 
((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

99 
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

100 
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

101 
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

102 
"### 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

103 
val _ = 
51399
6ac3c29a300e
discontinued "isabelle usedir" option r (reset session path);
wenzelm
parents:
51398
diff
changeset

104 
if not reset then () 
6ac3c29a300e
discontinued "isabelle usedir" option r (reset session path);
wenzelm
parents:
51398
diff
changeset

105 
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

106 
val _ = 
51398
c3d02b3518c2
discontinued "isabelle usedir" option P (remote path);
wenzelm
parents:
51276
diff
changeset

107 
if rpath = "" then () 
51399
6ac3c29a300e
discontinued "isabelle usedir" option r (reset session path);
wenzelm
parents:
51398
diff
changeset

108 
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

109 

c3d02b3518c2
discontinued "isabelle usedir" option P (remote path);
wenzelm
parents:
51276
diff
changeset

110 
val _ = 
51399
6ac3c29a300e
discontinued "isabelle usedir" option r (reset session path);
wenzelm
parents:
51398
diff
changeset

111 
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

112 
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

113 
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

114 
val res2 = Exn.capture 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

115 
in ignore (Par_Exn.release_all [res1, res2]) end) 
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
37216
diff
changeset

116 
> Unsynchronized.setmp Proofterm.proofs level 
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
37216
diff
changeset

117 
> Unsynchronized.setmp print_mode (modes @ print_mode_value ()) 
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
37216
diff
changeset

118 
> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs 
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
39733
diff
changeset

119 
> Unsynchronized.setmp Goal.parallel_proofs_threshold parallel_proofs_threshold 
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
37216
diff
changeset

120 
> Unsynchronized.setmp Multithreading.trace trace_threads 
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
37216
diff
changeset

121 
> Unsynchronized.setmp Multithreading.max_threads 
23979  122 
(if Multithreading.available then max_threads 
123 
else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) () 

31478  124 
handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1); 
6346  125 

126 
end; 