author  wenzelm 
Tue, 08 Jan 2013 21:16:51 +0100  
changeset 50777  20126dd9772c 
parent 50707  5b2bf7611662 
child 50781  a0f22c2d60cc 
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 

4 
Session management  maintain state of logic images. 

5 
*) 

6 

7 
signature SESSION = 

8 
sig 

25840  9 
val id: unit > string list 
11509  10 
val name: unit > string 
50707
5b2bf7611662
maintain session index on Scala side, for more determistic results;
wenzelm
parents:
50430
diff
changeset

11 
val path: unit > string list 
6346  12 
val welcome: unit > string 
48457  13 
val finish: unit > unit 
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset

14 
val init: bool > bool > bool > string > string > bool > string > (string * string) list > 
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

15 
string > string > bool * string > string > bool > unit 
48457  16 
val with_timing: string > bool > ('a > 'b) > 'a > 'b 
48445  17 
val use_dir: string > string > bool > string list > bool > bool > string > 
31688  18 
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

19 
string > int > bool > bool > int > int > int > int > unit 
6346  20 
end; 
21 

22 
structure Session: SESSION = 

23 
struct 

24 

25 
(* session state *) 

26 

32738  27 
val session = Unsynchronized.ref ([Context.PureN]: string list); 
28 
val session_finished = Unsynchronized.ref false; 

48542  29 

30 
fun id () = ! session; 

31 
fun name () = "Isabelle/" ^ List.last (! session); 

9414  32 

33 

34 
(* access path *) 

6346  35 

48542  36 
val session_path = Unsynchronized.ref ([]: string list); 
37 
val remote_path = Unsynchronized.ref (NONE: Url.T option); 

6346  38 

48542  39 
fun path () = ! session_path; 
26109
c69c3559355b
more elaborate structure Distribution (filledin by makedist);
wenzelm
parents:
25840
diff
changeset

40 

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

41 

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

42 
(* welcome *) 
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

43 

26109
c69c3559355b
more elaborate structure Distribution (filledin by makedist);
wenzelm
parents:
25840
diff
changeset

44 
fun welcome () = 
26134  45 
if Distribution.is_official then 
46 
"Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")" 

48990  47 
else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")"; 
6346  48 

49 

9414  50 
(* add_path *) 
51 

52 
fun add_path reset s = 

53 
let val sess = ! session @ [s] in 

18964  54 
(case duplicates (op =) sess of 
9414  55 
[] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s])) 
48542  56 
 dups => error ("Duplicate session identifiers " ^ commas_quote dups)) 
9414  57 
end; 
58 

59 

48457  60 
(* init_name *) 
6346  61 

48457  62 
fun init_name reset parent name = 
20664  63 
if not (member (op =) (! session) parent) orelse not (! session_finished) then 
6346  64 
error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) 
65 
else (add_path reset name; session_finished := false); 

66 

67 

68 
(* finish *) 

69 

49931
85780e6f8fd2
more basic Goal.reset_futures as snapshot of implicit state;
wenzelm
parents:
49911
diff
changeset

70 
fun finish_futures () = 
85780e6f8fd2
more basic Goal.reset_futures as snapshot of implicit state;
wenzelm
parents:
49911
diff
changeset

71 
(case map_filter Task_Queue.group_status (Goal.reset_futures ()) of 
85780e6f8fd2
more basic Goal.reset_futures as snapshot of implicit state;
wenzelm
parents:
49911
diff
changeset

72 
[] => () 
85780e6f8fd2
more basic Goal.reset_futures as snapshot of implicit state;
wenzelm
parents:
49911
diff
changeset

73 
 exns => raise Par_Exn.make exns); 
85780e6f8fd2
more basic Goal.reset_futures as snapshot of implicit state;
wenzelm
parents:
49911
diff
changeset

74 

6346  75 
fun finish () = 
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

76 
(Future.shutdown (); 
49931
85780e6f8fd2
more basic Goal.reset_futures as snapshot of implicit state;
wenzelm
parents:
49911
diff
changeset

77 
finish_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

78 
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

79 
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

80 
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

81 
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

82 
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

83 
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

84 
session_finished := true); 
6346  85 

86 

87 
(* use_dir *) 

88 

50777  89 
fun with_timing name verbose f x = 
90 
let 

91 
val start = Timing.start (); 

92 
val y = f x; 

93 
val timing = Timing.result start; 

94 

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

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

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

98 

99 
val _ = 

100 
writeln ("\fTiming = " ^ ML_Syntax.print_properties 

101 
([("threads", threads)] @ Timing.properties timing @ [("factor", factor)])); 

102 
val _ = 

103 
if verbose then 

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

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

106 
else (); 

107 
in y end; 

48457  108 

48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

109 
fun get_rpath rpath = 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

110 
(if rpath = "" then () else 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

111 
if is_some (! remote_path) then 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

112 
error "Path for remote theory browsing information may only be set once" 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

113 
else 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

114 
remote_path := SOME (Url.explode rpath); 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

115 
(! remote_path, rpath <> "")); 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

116 

48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset

117 
fun init build reset info info_path doc doc_graph doc_output doc_variants 
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset

118 
parent name doc_dump rpath verbose = 
48457  119 
(init_name reset parent name; 
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset

120 
Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_output 
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset

121 
doc_variants (path ()) name doc_dump (get_rpath rpath) verbose 
48467
a4318c36a829
more precise propagation of options: build, session, theories;
wenzelm
parents:
48457
diff
changeset

122 
(map Thy_Info.get_theory (Thy_Info.get_names ()))); 
48457  123 

48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

124 
local 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

125 

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

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

127 
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

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

129 

48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

130 
in 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

131 

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

133 
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

134 
parallel_proofs parallel_proofs_threshold = 
23972  135 
((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

136 
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

137 
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

138 
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

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

140 
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

141 
init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name 
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

142 
doc_dump rpath 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

143 
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

144 
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

145 
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

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

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

148 
> 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

149 
> 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

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

151 
> Unsynchronized.setmp Multithreading.max_threads 
23979  152 
(if Multithreading.available then max_threads 
153 
else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) () 

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

156 
end; 

48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

157 

c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

158 
end; 