author  wenzelm 
Mon, 22 Dec 2014 18:10:54 +0100  
changeset 59178  e819a6683f87 
parent 59177  f96ff29aa00c 
child 59180  c0fa3b3bdabd 
permissions  rwrr 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

1 
(* Title: Pure/Thy/thy_info.ML 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

2 
Author: Markus Wenzel, TU Muenchen 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

3 

37978
548f3f165d05
simplified Thy_Header.read  include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset

4 
Global theory info database, with autoloading according to theory and 
15801  5 
file dependencies. 
3976  6 
*) 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

7 

6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

8 
signature THY_INFO = 
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

9 
sig 
26614  10 
val get_names: unit > string list 
7288  11 
val lookup_theory: string > theory option 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

12 
val get_theory: string > theory 
26983  13 
val master_directory: string > Path.T 
29421
db532e37cda2
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in posthoc fashion;
wenzelm
parents:
29118
diff
changeset

14 
val remove_thy: string > unit 
54458
96ccc8972fc7
prefer explicit "document" flag  eliminated stateful Present.no_document;
wenzelm
parents:
54446
diff
changeset

15 
val use_theories: 
96ccc8972fc7
prefer explicit "document" flag  eliminated stateful Present.no_document;
wenzelm
parents:
54446
diff
changeset

16 
{document: bool, last_timing: Toplevel.transition > Time.time option, master_dir: Path.T} > 
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
50862
diff
changeset

17 
(string * Position.T) list > unit 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48898
diff
changeset

18 
val use_thys: (string * Position.T) list > unit 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48898
diff
changeset

19 
val use_thy: string * Position.T > unit 
58856  20 
val script_thy: Position.T > string > theory > theory 
37954
a2e73df0b1e0
simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
wenzelm
parents:
37953
diff
changeset

21 
val register_thy: theory > unit 
24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

22 
val finish: unit > unit 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

23 
end; 
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

24 

37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset

25 
structure Thy_Info: THY_INFO = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

26 
struct 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

27 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

28 
(** thy database **) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

29 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

30 
(* messages *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

31 

55797  32 
val show_path = space_implode " via " o map quote; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

33 

55797  34 
fun cycle_msg names = "Cyclic dependency of " ^ show_path names; 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

35 

6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

36 

6666  37 
(* derived graph operations *) 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

38 

50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

39 
fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G 
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

40 
handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess)); 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

41 

37984
f26352bd82cf
clarified register_thy: clean slate via kill_thy, more precise CRITICAL section;
wenzelm
parents:
37981
diff
changeset

42 
fun new_entry name parents entry = 
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

43 
String_Graph.new_node (name, entry) #> add_deps name parents; 
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

44 

3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

45 

59178  46 
(* global thys *) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

47 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

48 
type deps = 
41955
703ea96b13c6
files are identified via SHA1 digests  discontinued ISABELLE_FILE_IDENT;
wenzelm
parents:
41678
diff
changeset

49 
{master: (Path.T * SHA1.digest), (*master dependencies for thy file*) 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48898
diff
changeset

50 
imports: (string * Position.T) list}; (*source specification of imports (partially qualified)*) 
23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

51 

38148
d2f3c8d4a89f
uniform naming of imports (source specification) vs. parents (thy node names) vs. parent_thys (theory values);
wenzelm
parents:
38147
diff
changeset

52 
fun make_deps master imports : deps = {master = master, imports = imports}; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

53 

59178  54 
fun master_dir (d: deps option) = 
55 
the_default Path.current (Option.map (Path.dir o #1 o #master) d); 

56 

44225
a8f921e6484f
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents:
44222
diff
changeset

57 
fun base_name s = Path.implode (Path.base (Path.explode s)); 
23967  58 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

59 
local 
59178  60 
val global_thys = 
61 
Synchronized.var "Thy_Info.thys" 

62 
(String_Graph.empty: (deps option * theory option) String_Graph.T); 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

63 
in 
59178  64 
fun get_thys () = Synchronized.value global_thys; 
65 
fun change_thys f = Synchronized.change global_thys f; 

3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

66 
end; 
5209  67 

50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

68 
fun get_names () = String_Graph.topological_order (get_thys ()); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

69 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

70 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

71 
(* access thy *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

72 

59178  73 
fun lookup thys name = try (String_Graph.get_node thys) name; 
74 
fun lookup_thy name = lookup (get_thys ()) name; 

7935  75 

59178  76 
fun get thys name = 
77 
(case lookup thys name of 

15531  78 
SOME thy => thy 
55797  79 
 NONE => error ("Theory loader: nothing known about theory " ^ quote name)); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

80 

59178  81 
fun get_thy name = get (get_thys ()) name; 
82 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

83 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

84 
(* access deps *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

85 

15570  86 
val lookup_deps = Option.map #1 o lookup_thy; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

87 

59178  88 
val master_directory = master_dir o #1 o get_thy; 
7191  89 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

90 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

91 
(* access theory *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

92 

7687  93 
fun lookup_theory name = 
94 
(case lookup_thy name of 

38142  95 
SOME (_, SOME theory) => SOME theory 
15531  96 
 _ => NONE); 
7288  97 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

98 
fun get_theory name = 
7288  99 
(case lookup_theory name of 
23871  100 
SOME theory => theory 
55797  101 
 _ => error ("Theory loader: undefined entry for theory " ^ quote name)); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

102 

56208  103 
val get_imports = Resources.imports_of o get_theory; 
44337
d453faed4815
clarified get_imports  should not rely on accidental order within graph;
wenzelm
parents:
44302
diff
changeset

104 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

105 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

106 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

107 
(** thy operations **) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

108 

59178  109 
(* remove *) 
29421
db532e37cda2
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in posthoc fashion;
wenzelm
parents:
29118
diff
changeset

110 

59178  111 
fun remove name thys = 
112 
(case lookup thys name of 

113 
NONE => thys 

114 
 SOME (NONE, _) => error ("Cannot update finished theory " ^ quote name) 

115 
 SOME _ => 

116 
let 

117 
val succs = String_Graph.all_succs thys [name]; 

118 
val _ = writeln ("Theory loader: removing " ^ commas_quote succs); 

119 
in fold String_Graph.del_node succs thys end); 

29421
db532e37cda2
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in posthoc fashion;
wenzelm
parents:
29118
diff
changeset

120 

59178  121 
val remove_thy = change_thys o remove; 
122 

7099  123 

59178  124 
(* update *) 
125 

126 
fun update deps theory thys = 

43640  127 
let 
128 
val name = Context.theory_name theory; 

129 
val parents = map Context.theory_name (Theory.parents_of theory); 

59178  130 

131 
val thys' = remove name thys; 

132 
val _ = map (get thys') parents; 

133 
in new_entry name parents (SOME deps, SOME theory) thys' end; 

134 

135 
fun update_thy deps theory = change_thys (update deps theory); 

43640  136 

7099  137 

24209  138 
(* scheduling loader tasks *) 
139 

51330  140 
datatype result = 
53375
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

141 
Result of {theory: theory, exec_id: Document_ID.exec, 
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

142 
present: unit > unit, commit: unit > unit, weight: int}; 
51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

143 

53375
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

144 
fun theory_result theory = 
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

145 
Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0}; 
51330  146 

147 
fun result_theory (Result {theory, ...}) = theory; 

51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

148 
fun result_present (Result {present, ...}) = present; 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

149 
fun result_commit (Result {commit, ...}) = commit; 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

150 
fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i); 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

151 

53375
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

152 
fun join_theory (Result {theory, exec_id, ...}) = 
54370
39ac1a02c60c
join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
wenzelm
parents:
53375
diff
changeset

153 
let 
39ac1a02c60c
join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
wenzelm
parents:
53375
diff
changeset

154 
(*toplevel proofs and diags*) 
39ac1a02c60c
join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
wenzelm
parents:
53375
diff
changeset

155 
val _ = Future.join_tasks (maps Future.group_snapshot (Execution.peek exec_id)); 
39ac1a02c60c
join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
wenzelm
parents:
53375
diff
changeset

156 
(*fully nested proofs*) 
39ac1a02c60c
join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
wenzelm
parents:
53375
diff
changeset

157 
val res = Exn.capture Thm.join_theory_proofs theory; 
39ac1a02c60c
join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
wenzelm
parents:
53375
diff
changeset

158 
in res :: map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id)) end; 
43641
081e009549dc
uniform finish_thy  always Global_Theory.join_proofs, even with sequential scheduling;
wenzelm
parents:
43640
diff
changeset

159 

37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

160 
datatype task = 
55461
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

161 
Task of Path.T * string list * (theory list > result)  
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

162 
Finished of theory; 
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

163 

3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

164 
fun task_finished (Task _) = false 
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

165 
 task_finished (Finished _) = true; 
24209  166 

44162  167 
fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents; 
168 

29118  169 
local 
170 

44162  171 
val schedule_seq = 
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

172 
String_Graph.schedule (fn deps => fn (_, task) => 
44162  173 
(case task of 
55461
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

174 
Task (_, parents, body) => 
51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

175 
let 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

176 
val result = body (task_parents deps parents); 
53190
5d92649a310e
simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML);
wenzelm
parents:
51661
diff
changeset

177 
val _ = Par_Exn.release_all (join_theory result); 
51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

178 
val _ = result_present result (); 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

179 
val _ = result_commit result (); 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

180 
in result_theory result end 
44162  181 
 Finished thy => thy)) #> ignore; 
29000
5e03bc760355
improved future_schedule: more robust handling of failed parents (explicit join), final join of all futures, including Exn.release_all;
wenzelm
parents:
28980
diff
changeset

182 

51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

183 
val schedule_futures = uninterruptible (fn _ => fn tasks => 
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

184 
let 
51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

185 
val futures = tasks 
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

186 
> String_Graph.schedule (fn deps => fn (name, task) => 
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

187 
(case task of 
55461
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

188 
Task (_, parents, body) => 
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

189 
(singleton o Future.forks) 
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

190 
{name = "theory:" ^ name, group = NONE, 
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

191 
deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true} 
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

192 
(fn () => 
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

193 
(case filter (not o can Future.join o #2) deps of 
51330  194 
[] => body (map (result_theory o Future.join) (task_parents deps parents)) 
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

195 
 bad => 
55797  196 
error 
197 
("Failed to load theory " ^ quote name ^ 

198 
" (unresolved " ^ commas_quote (map #1 bad) ^ ")"))) 

51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

199 
 Finished theory => Future.value (theory_result theory))); 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

200 

e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

201 
val results1 = futures 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

202 
> maps (fn future => 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

203 
(case Future.join_result future of 
53190
5d92649a310e
simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML);
wenzelm
parents:
51661
diff
changeset

204 
Exn.Res result => join_theory result 
51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

205 
 Exn.Exn exn => [Exn.Exn exn])); 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

206 

e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

207 
val results2 = futures 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

208 
> map_filter (Exn.get_res o Future.join_result) 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

209 
> sort result_ord 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

210 
> Par_List.map (fn result => Exn.capture (result_present result) ()); 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

211 

e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

212 
(* FIXME more precise commit order (!?) *) 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

213 
val results3 = futures 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

214 
> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ()); 
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

215 

54370
39ac1a02c60c
join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
wenzelm
parents:
53375
diff
changeset

216 
(* FIXME avoid global Execution.reset (!??) *) 
53192  217 
val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ())); 
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

218 

51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

219 
val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4); 
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

220 
in () end); 
29429
a6c641f08af7
schedule_futures: tuned final consolidation, explicit after_load phase;
wenzelm
parents:
29421
diff
changeset

221 

24209  222 
in 
223 

32794  224 
fun schedule_tasks tasks = 
29118  225 
if not (Multithreading.enabled ()) then schedule_seq tasks 
226 
else if Multithreading.self_critical () then 

55797  227 
(warning "Theory loader: no multithreading within critical section"; 
24209  228 
schedule_seq tasks) 
29118  229 
else schedule_futures tasks; 
24209  230 

231 
end; 

232 

233 

23967  234 
(* require_thy  checking database entries wrt. the filesystem *) 
15065  235 

7211  236 
local 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

237 

37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

238 
fun required_by _ [] = "" 
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

239 
 required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; 
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

240 

54458
96ccc8972fc7
prefer explicit "document" flag  eliminated stateful Present.no_document;
wenzelm
parents:
54446
diff
changeset

241 
fun load_thy document last_timing initiators update_time deps text (name, pos) keywords parents = 
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

242 
let 
59178  243 
val _ = remove_thy name; 
58843  244 
val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators); 
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56208
diff
changeset

245 
val _ = Output.try_protocol_message (Markup.loading_theory name) []; 
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

246 

41548
bd0bebf93fa6
Thy_Load.begin_theory: maintain source specification of imports;
wenzelm
parents:
41536
diff
changeset

247 
val {master = (thy_path, _), imports} = deps; 
38134
3de75ca6f166
load_thy: refer to physical master directory (not accumulated source import directory) and enable loading files relatively to that;
wenzelm
parents:
37985
diff
changeset

248 
val dir = Path.dir thy_path; 
51294
0850d43cb355
discontinued obsolete header "files"  these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset

249 
val header = Thy_Header.make (name, pos) imports keywords; 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48898
diff
changeset

250 

ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48898
diff
changeset

251 
val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents); 
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

252 

53375
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

253 
val exec_id = Document_ID.make (); 
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

254 
val _ = 
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

255 
Execution.running Document_ID.none exec_id [] orelse 
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

256 
raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id); 
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

257 

78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

258 
val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path); 
51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

259 
val (theory, present, weight) = 
56208  260 
Resources.load_thy document last_timing update_time dir header text_pos text 
48638  261 
(if name = Context.PureN then [ML_Context.the_global_context ()] else parents); 
43640  262 
fun commit () = update_thy deps theory; 
53375
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

263 
in 
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

264 
Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight} 
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

265 
end; 
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

266 

48898
9fc880720663
simplified Thy_Load.check_thy (again)  no need to pass keywords nor find files in body text;
wenzelm
parents:
48888
diff
changeset

267 
fun check_deps dir name = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

268 
(case lookup_deps name of 
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51284
diff
changeset

269 
SOME NONE => (true, NONE, Position.none, get_imports name, []) 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

270 
 NONE => 
56208  271 
let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name 
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51284
diff
changeset

272 
in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end 
42129
c17508a61f49
present theory content as future, depending on intermediate proof state futures  potential to reduce memory requirements and improve parallelization;
wenzelm
parents:
42003
diff
changeset

273 
 SOME (SOME {master, ...}) => 
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41955
diff
changeset

274 
let 
48928  275 
val {master = master', text = text', theory_pos = theory_pos', imports = imports', 
56208  276 
keywords = keywords'} = Resources.check_thy dir name; 
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41955
diff
changeset

277 
val deps' = SOME (make_deps master' imports', text'); 
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41955
diff
changeset

278 
val current = 
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41955
diff
changeset

279 
#2 master = #2 master' andalso 
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41955
diff
changeset

280 
(case lookup_theory name of 
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41955
diff
changeset

281 
NONE => false 
56208  282 
 SOME theory => Resources.loaded_files_current theory); 
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51284
diff
changeset

283 
in (current, deps', theory_pos', imports', keywords') end); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

284 

23967  285 
in 
286 

54458
96ccc8972fc7
prefer explicit "document" flag  eliminated stateful Present.no_document;
wenzelm
parents:
54446
diff
changeset

287 
fun require_thys document last_timing initiators dir strs tasks = 
96ccc8972fc7
prefer explicit "document" flag  eliminated stateful Present.no_document;
wenzelm
parents:
54446
diff
changeset

288 
fold_map (require_thy document last_timing initiators dir) strs tasks >> forall I 
96ccc8972fc7
prefer explicit "document" flag  eliminated stateful Present.no_document;
wenzelm
parents:
54446
diff
changeset

289 
and require_thy document last_timing initiators dir (str, require_pos) tasks = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

290 
let 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
20664
diff
changeset

291 
val path = Path.expand (Path.explode str); 
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
20664
diff
changeset

292 
val name = Path.implode (Path.base path); 
56208  293 
val node_name = File.full_path dir (Resources.thy_path path); 
55461
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

294 
fun check_entry (Task (node_name', _, _)) = 
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

295 
if node_name = node_name' then () 
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

296 
else 
55797  297 
error ("Incoherent imports for theory " ^ quote name ^ 
55461
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

298 
Position.here require_pos ^ ":\n" ^ 
55488
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
55461
diff
changeset

299 
" " ^ Path.print node_name ^ "\n" ^ 
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
55461
diff
changeset

300 
" " ^ Path.print node_name') 
55461
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

301 
 check_entry _ = (); 
7066  302 
in 
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

303 
(case try (String_Graph.get_node tasks) name of 
55461
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

304 
SOME task => (check_entry task; (task_finished task, tasks)) 
23967  305 
 NONE => 
306 
let 

43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
43641
diff
changeset

307 
val dir' = Path.append dir (Path.dir path); 
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
43641
diff
changeset

308 
val _ = member (op =) initiators name andalso error (cycle_msg initiators); 
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
43641
diff
changeset

309 

51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51284
diff
changeset

310 
val (current, deps, theory_pos, imports, keywords) = check_deps dir' name 
55797  311 
handle ERROR msg => 
312 
cat_error msg 

313 
("The error(s) above occurred for theory " ^ quote name ^ 

314 
Position.here require_pos ^ required_by "\n" initiators); 

37981
9a15982f41fe
theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);
wenzelm
parents:
37980
diff
changeset

315 

48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48898
diff
changeset

316 
val parents = map (base_name o #1) imports; 
48898
9fc880720663
simplified Thy_Load.check_thy (again)  no need to pass keywords nor find files in body text;
wenzelm
parents:
48888
diff
changeset

317 
val (parents_current, tasks') = 
54458
96ccc8972fc7
prefer explicit "document" flag  eliminated stateful Present.no_document;
wenzelm
parents:
54446
diff
changeset

318 
require_thys document last_timing (name :: initiators) 
48898
9fc880720663
simplified Thy_Load.check_thy (again)  no need to pass keywords nor find files in body text;
wenzelm
parents:
48888
diff
changeset

319 
(Path.append dir (master_dir (Option.map #1 deps))) imports tasks; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

320 

23967  321 
val all_current = current andalso parents_current; 
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

322 
val task = 
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

323 
if all_current then Finished (get_theory name) 
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

324 
else 
37980
b8c3d4dc1e3e
avoid repeated File.read for theory text (as before);
wenzelm
parents:
37979
diff
changeset

325 
(case deps of 
b8c3d4dc1e3e
avoid repeated File.read for theory text (as before);
wenzelm
parents:
37979
diff
changeset

326 
NONE => raise Fail "Malformed deps" 
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41955
diff
changeset

327 
 SOME (dep, text) => 
48876
157dd47032e0
more standard Thy_Load.check_thy for Pure.thy, relying on its header;
wenzelm
parents:
48874
diff
changeset

328 
let 
157dd47032e0
more standard Thy_Load.check_thy for Pure.thy, relying on its header;
wenzelm
parents:
48874
diff
changeset

329 
val update_time = serial (); 
48928  330 
val load = 
54458
96ccc8972fc7
prefer explicit "document" flag  eliminated stateful Present.no_document;
wenzelm
parents:
54446
diff
changeset

331 
load_thy document last_timing initiators update_time dep 
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51284
diff
changeset

332 
text (name, theory_pos) keywords; 
55461
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

333 
in Task (node_name, parents, load) end); 
48874
ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48710
diff
changeset

334 

ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48710
diff
changeset

335 
val tasks'' = new_entry name parents task tasks'; 
48898
9fc880720663
simplified Thy_Load.check_thy (again)  no need to pass keywords nor find files in body text;
wenzelm
parents:
48888
diff
changeset

336 
in (all_current, tasks'') end) 
7066  337 
end; 
6484
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

338 

23967  339 
end; 
340 

341 

37979  342 
(* use_thy *) 
23967  343 

54458
96ccc8972fc7
prefer explicit "document" flag  eliminated stateful Present.no_document;
wenzelm
parents:
54446
diff
changeset

344 
fun use_theories {document, last_timing, master_dir} imports = 
96ccc8972fc7
prefer explicit "document" flag  eliminated stateful Present.no_document;
wenzelm
parents:
54446
diff
changeset

345 
schedule_tasks (snd (require_thys document last_timing [] master_dir imports String_Graph.empty)); 
23967  346 

54458
96ccc8972fc7
prefer explicit "document" flag  eliminated stateful Present.no_document;
wenzelm
parents:
54446
diff
changeset

347 
val use_thys = use_theories {document = false, last_timing = K NONE, master_dir = Path.current}; 
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load  as theory data instead of accidental loader state;
wenzelm
parents:
37942
diff
changeset

348 
val use_thy = use_thys o single; 
7211  349 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

350 

57626  351 
(* toplevel scripting  without maintaining database *) 
352 

58856  353 
fun script_thy pos txt thy = 
57626  354 
let 
58856  355 
val trs = 
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58856
diff
changeset

356 
Outer_Syntax.parse thy pos txt 
58856  357 
> map (Toplevel.modify_init (K thy)); 
57626  358 
val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs); 
359 
val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel; 

360 
in Toplevel.end_theory end_pos end_state end; 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

361 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

362 

37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

363 
(* register theory *) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

364 

37954
a2e73df0b1e0
simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
wenzelm
parents:
37953
diff
changeset

365 
fun register_thy theory = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

366 
let 
16454  367 
val name = Context.theory_name theory; 
56208  368 
val {master, ...} = Resources.check_thy (Resources.master_directory theory) name; 
369 
val imports = Resources.imports_of theory; 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

370 
in 
59178  371 
change_thys (fn thys => 
372 
let 

373 
val thys' = remove name thys; 

374 
val _ = writeln ("Registering theory " ^ quote name); 

375 
in update (make_deps master imports) theory thys' end) 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

376 
end; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

377 

24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

378 

8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

379 
(* finish all theories *) 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

380 

50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

381 
fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry))); 
24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

382 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

383 
end; 