author  wenzelm 
Wed, 19 Aug 2015 16:21:10 +0200  
changeset 60975  5f3d6e16ea78 
parent 60937  51425cbe8ce9 
child 61381  ddca85598c65 
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 
60937  13 
val pure_theory: unit > theory 
26983  14 
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

15 
val remove_thy: string > unit 
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset

16 
val use_theories: 
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset

17 
{document: bool, last_timing: Toplevel.transition > Time.time option, master_dir: Path.T} > 
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset

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

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

20 
val use_thy: string * Position.T > unit 
58856  21 
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

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

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

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

25 

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

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

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

28 

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

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

30 

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

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

32 

55797  33 
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

34 

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

36 

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

37 

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

39 

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

40 
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

41 
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

42 

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

43 
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

44 
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

45 

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

46 

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

48 

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

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

50 
{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

51 
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

52 

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

53 
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

54 

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

57 

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

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

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

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

63 
(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

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

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

67 
end; 
5209  68 

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

69 
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

70 

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

71 

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

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

73 

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

7935  76 

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

15531  79 
SOME thy => thy 
55797  80 
 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

81 

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

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

84 

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

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

86 

15570  87 
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

88 

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

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

91 

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

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

93 

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

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

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

99 
fun get_theory name = 
7288  100 
(case lookup_theory name of 
23871  101 
SOME theory => theory 
55797  102 
 _ => 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

103 

60937  104 
fun pure_theory () = get_theory "Pure"; 
105 

56208  106 
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

107 

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

108 

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

109 

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

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

111 

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

113 

59178  114 
fun remove name thys = 
115 
(case lookup thys name of 

116 
NONE => thys 

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

118 
 SOME _ => 

119 
let 

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

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

122 
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

123 

59178  124 
val remove_thy = change_thys o remove; 
125 

7099  126 

59178  127 
(* update *) 
128 

129 
fun update deps theory thys = 

43640  130 
let 
131 
val name = Context.theory_name theory; 

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

59178  133 

134 
val thys' = remove name thys; 

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

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

137 

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

43640  139 

7099  140 

24209  141 
(* scheduling loader tasks *) 
142 

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

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

145 
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

146 

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

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

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

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

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

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

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

153 
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

154 

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

155 
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

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

157 
(*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

158 
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

159 
(*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

160 
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

161 
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

162 

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

163 
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

164 
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

165 
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

166 

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

167 
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

168 
 task_finished (Finished _) = true; 
24209  169 

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

29118  172 
local 
173 

44162  174 
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

175 
String_Graph.schedule (fn deps => fn (_, task) => 
44162  176 
(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

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

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

179 
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

180 
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

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

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

183 
in result_theory result end 
44162  184 
 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

185 

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

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

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

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

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

190 
(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

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

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

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

194 
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

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

196 
(case filter (not o can Future.join o #2) deps of 
51330  197 
[] => 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

198 
 bad => 
55797  199 
error 
200 
("Failed to load theory " ^ quote name ^ 

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

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

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

203 

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

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

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

206 
(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

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

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

209 

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

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

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

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

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

214 

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

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

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

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

218 

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

219 
(* FIXME avoid global Execution.reset (!??) *) 
53192  220 
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

221 

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

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

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

224 

24209  225 
in 
226 

32794  227 
fun schedule_tasks tasks = 
59180
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59178
diff
changeset

228 
if Multithreading.enabled () then schedule_futures tasks else schedule_seq tasks; 
24209  229 

230 
end; 

231 

232 

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

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

236 

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

237 
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

238 
 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

239 

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

240 
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

241 
let 
59178  242 
val _ = remove_thy name; 
58843  243 
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

244 
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

245 

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

246 
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

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

248 
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

249 

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

250 
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

251 

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

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

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

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

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

256 

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

257 
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

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

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

263 
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

264 
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

265 

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

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

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

268 
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

269 
 NONE => 
56208  270 
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

271 
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

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

273 
let 
48928  274 
val {master = master', text = text', theory_pos = theory_pos', imports = imports', 
56208  275 
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

276 
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

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

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

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

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

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

283 

23967  284 
in 
285 

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

286 
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

287 
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

288 
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

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

290 
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

291 
val name = Path.implode (Path.base path); 
56208  292 
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

293 
fun check_entry (Task (node_name', _, _)) = 
60975
5f3d6e16ea78
avoid ambiguities on native Windows, such as / vs. /cygdrive/c/cygwin;
wenzelm
parents:
60937
diff
changeset

294 
if op = (apply2 File.platform_path (node_name, node_name')) 
5f3d6e16ea78
avoid ambiguities on native Windows, such as / vs. /cygdrive/c/cygwin;
wenzelm
parents:
60937
diff
changeset

295 
then () 
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

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 

59364  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; 