--- a/src/HOL/Tools/atp_wrapper.ML Tue Jul 28 13:38:13 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML Tue Jul 28 20:26:39 2009 +0200
@@ -59,9 +59,7 @@
val (ctxt, (chain_ths, th)) = goal
val thy = ProofContext.theory_of ctxt
val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
- val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno)
- handle THM ("assume: variables", _, _) =>
- error "Sledgehammer: Goal contains type variables (TVars)"
+ val goal_cls = #1 (ResAxioms.neg_conjecture_clauses ctxt th subgoalno)
val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm ctxt th)) goal_cls
val the_filtered_clauses =
case filtered_clauses of
@@ -71,7 +69,8 @@
case axiom_clauses of
NONE => the_filtered_clauses
| SOME axcls => axcls
- val (thm_names, clauses) = preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
+ val (thm_names, clauses) =
+ preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
(* write out problem file and call prover *)
val probfile = prob_pathname subgoalno
@@ -85,7 +84,7 @@
val _ =
if destdir' = "" then File.rm probfile
else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof
-
+
(* check for success and print out some information on failure *)
val failure = find_failure proof
val success = rc = 0 andalso is_none failure
@@ -133,7 +132,7 @@
fun vampire_opts max_new theory_const timeout = tptp_prover_opts
max_new theory_const
(Path.explode "$VAMPIRE_HOME/vampire",
- ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
+ ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
timeout;
val vampire = vampire_opts 60 false;
@@ -141,7 +140,7 @@
fun vampire_opts_full max_new theory_const timeout = full_prover_opts
max_new theory_const
(Path.explode "$VAMPIRE_HOME/vampire",
- ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
+ ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
timeout;
val vampire_full = vampire_opts_full 60 false;
@@ -173,7 +172,8 @@
(ResAtp.prepare_clauses true)
(ResHolClause.dfg_write_file (AtpManager.get_full_types()))
(Path.explode "$SPASS_HOME/SPASS",
- "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)
+ "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^
+ string_of_int timeout)
ResReconstruct.find_failure
(ResReconstruct.lemma_list true)
timeout ax_clauses fcls name n goal;
@@ -196,22 +196,23 @@
end;
fun refresh_systems () = Synchronized.change systems (fn _ =>
- get_systems());
+ get_systems ());
fun get_system prefix = Synchronized.change_result systems (fn systems =>
let val systems = if null systems then get_systems() else systems
in (find_first (String.isPrefix prefix) systems, systems) end);
fun remote_prover_opts max_new theory_const args prover_prefix timeout =
- let val sys = case get_system prover_prefix of
+ let val sys =
+ case get_system prover_prefix of
NONE => error ("No system like " ^ quote prover_prefix ^ " at SystemOnTPTP")
| SOME sys => sys
in tptp_prover_opts max_new theory_const
(Path.explode "$ISABELLE_HOME/lib/scripts/SystemOnTPTP",
- args ^ " -t " ^ string_of_int timeout ^ " -s " ^ sys) timeout end;
+ args ^ " -t " ^ string_of_int timeout ^ " -s " ^ sys) timeout
+ end;
val remote_prover = remote_prover_opts 60 false;
end;
-
--- a/src/HOL/Tools/res_axioms.ML Tue Jul 28 13:38:13 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML Tue Jul 28 20:26:39 2009 +0200
@@ -14,7 +14,7 @@
val neg_clausify: thm list -> thm list
val expand_defs_tac: thm -> tactic
val combinators: thm -> thm
- val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
+ val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list
val atpset_rules_of: Proof.context -> (string * thm) list
val suppress_endtheory: bool ref (*for emergency use where endtheory causes problems*)
val setup: theory -> theory
@@ -498,32 +498,30 @@
val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac];
-fun neg_clausify sts =
- sts |> Meson.make_clauses |> map combinators |> Meson.finish_cnf;
+val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf;
-fun neg_conjecture_clauses st0 n =
- let val st = Seq.hd (neg_skolemize_tac n st0)
- val (params,_,_) = OldGoals.strip_context (Logic.nth_prem (n, Thm.prop_of st))
- in (neg_clausify (the (OldGoals.metahyps_thms n st)), params) end
- handle Option => error "unable to Skolemize subgoal";
+fun neg_conjecture_clauses ctxt st0 n =
+ let
+ val st = Seq.hd (neg_skolemize_tac n st0)
+ val ({params, prems, ...}, _) = Subgoal.focus (Variable.set_body false ctxt) n st
+ in (neg_clausify prems, map (Term.dest_Free o Thm.term_of o #2) params) end;
(*Conversion of a subgoal to conjecture clauses. Each clause has
leading !!-bound universal variables, to express generality. *)
-val neg_clausify_tac =
+fun neg_clausify_tac ctxt =
neg_skolemize_tac THEN'
- SUBGOAL
- (fn (prop,_) =>
- let val ts = Logic.strip_assums_hyp prop
- in EVERY1
- [OldGoals.METAHYPS
- (fn hyps =>
- (Method.insert_tac
- (map forall_intr_vars (neg_clausify hyps)) 1)),
- REPEAT_DETERM_N (length ts) o (etac thin_rl)]
+ SUBGOAL (fn (prop, i) =>
+ let val ts = Logic.strip_assums_hyp prop in
+ EVERY'
+ [FOCUS
+ (fn {prems, ...} =>
+ (Method.insert_tac
+ (map forall_intr_vars (neg_clausify prems)) i)) ctxt,
+ REPEAT_DETERM_N (length ts) o etac thin_rl] i
end);
val neg_clausify_setup =
- Method.setup @{binding neg_clausify} (Scan.succeed (K (SIMPLE_METHOD' neg_clausify_tac)))
+ Method.setup @{binding neg_clausify} (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac))
"conversion of goal to conjecture clauses";
--- a/src/HOL/Tools/res_reconstruct.ML Tue Jul 28 13:38:13 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Tue Jul 28 20:26:39 2009 +0200
@@ -442,7 +442,7 @@
val _ = trace (Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n")
val (_,lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
val _ = trace (Int.toString (length lines) ^ " lines extracted\n")
- val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno
+ val (ccls,fixes) = ResAxioms.neg_conjecture_clauses ctxt th sgno
val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n")
val ccls = map forall_intr_vars ccls
val _ =
@@ -452,10 +452,7 @@
val _ = trace "\ndecode_tstp_file: finishing\n"
in
isar_header (map #1 fixes) ^ String.concat ilines ^ "qed\n"
- end
- handle e => (*FIXME: exn handler is too general!*)
- let val msg = "Translation of TSTP raised an exception: " ^ ML_Compiler.exn_message e
- in trace msg; msg end;
+ end;
(*=== EXTRACTING PROOF-TEXT === *)
--- a/src/HOL/ex/ROOT.ML Tue Jul 28 13:38:13 2009 +0200
+++ b/src/HOL/ex/ROOT.ML Tue Jul 28 20:26:39 2009 +0200
@@ -68,7 +68,9 @@
"Landau"
];
-setmp Proofterm.proofs 2 use_thy "Hilbert_Classical";
+Future.shutdown ();
+(setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy))
+ "Hilbert_Classical";
use_thy "SVC_Oracle";
--- a/src/Pure/Concurrent/future.ML Tue Jul 28 13:38:13 2009 +0200
+++ b/src/Pure/Concurrent/future.ML Tue Jul 28 20:26:39 2009 +0200
@@ -1,7 +1,8 @@
(* Title: Pure/Concurrent/future.ML
Author: Makarius
-Future values.
+Future values, see also
+http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf
Notes:
@@ -26,7 +27,6 @@
signature FUTURE =
sig
- val enabled: unit -> bool
type task = Task_Queue.task
type group = Task_Queue.group
val is_worker: unit -> bool
@@ -56,11 +56,6 @@
(** future values **)
-fun enabled () =
- Multithreading.enabled () andalso
- not (Multithreading.self_critical ());
-
-
(* identifiers *)
type task = Task_Queue.task;
@@ -83,18 +78,19 @@
datatype 'a future = Future of
{task: task,
group: group,
- result: 'a Exn.result option ref};
+ result: 'a Exn.result option Synchronized.var};
fun task_of (Future {task, ...}) = task;
fun group_of (Future {group, ...}) = group;
+fun result_of (Future {result, ...}) = result;
-fun peek (Future {result, ...}) = ! result;
+fun peek x = Synchronized.peek (result_of x);
fun is_finished x = is_some (peek x);
fun value x = Future
{task = Task_Queue.new_task 0,
group = Task_Queue.new_group NONE,
- result = ref (SOME (Exn.Result x))};
+ result = Synchronized.var "future" (SOME (Exn.Result x))};
@@ -136,31 +132,18 @@
fun broadcast cond = (*requires SYNCHRONIZED*)
ConditionVar.broadcast cond;
-fun broadcast_all () = (*requires SYNCHRONIZED*)
- (ConditionVar.broadcast scheduler_event;
- ConditionVar.broadcast work_available;
+fun broadcast_work () = (*requires SYNCHRONIZED*)
+ (ConditionVar.broadcast work_available;
ConditionVar.broadcast work_finished);
end;
-(* worker activity *)
-
-fun count_active ws =
- fold (fn (_, active) => fn i => if active then i + 1 else i) ws 0;
-
-fun change_active active = (*requires SYNCHRONIZED*)
- change workers (AList.update Thread.equal (Thread.self (), active));
-
-fun overloaded () =
- count_active (! workers) > Multithreading.max_threads_value ();
-
-
(* execute future jobs *)
fun future_job group (e: unit -> 'a) =
let
- val result = ref (NONE: 'a Exn.result option);
+ val result = Synchronized.var "future" (NONE: 'a Exn.result option);
fun job ok =
let
val res =
@@ -170,7 +153,7 @@
Multithreading.with_attributes Multithreading.restricted_interrupts
(fn _ => fn () => e ())) ()) ()
else Exn.Exn Exn.Interrupt;
- val _ = result := SOME res;
+ val _ = Synchronized.change result (K (SOME res));
in
(case res of
Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
@@ -186,7 +169,7 @@
val valid = not (Task_Queue.is_canceled group);
val ok = setmp_thread_data (name, task, group) (fn () =>
fold (fn job => fn ok => job valid andalso ok) jobs true) ();
- val _ = SYNCHRONIZED "execute" (fn () =>
+ val _ = SYNCHRONIZED "finish" (fn () =>
let
val maximal = change_result queue (Task_Queue.finish task);
val _ =
@@ -199,12 +182,19 @@
in () end;
+(* worker activity *)
+
+fun count_active () = (*requires SYNCHRONIZED*)
+ fold (fn (_, active) => fn i => if active then i + 1 else i) (! workers) 0;
+
+fun change_active active = (*requires SYNCHRONIZED*)
+ change workers (AList.update Thread.equal (Thread.self (), active));
+
+
(* worker threads *)
fun worker_wait cond = (*requires SYNCHRONIZED*)
- (change_active false; broadcast scheduler_event;
- wait cond;
- change_active true; broadcast scheduler_event);
+ (change_active false; wait cond; change_active true);
fun worker_next () = (*requires SYNCHRONIZED*)
if ! excessive > 0 then
@@ -212,9 +202,10 @@
change workers (filter_out (fn (thread, _) => Thread.equal (thread, Thread.self ())));
broadcast scheduler_event;
NONE)
- else if overloaded () then (worker_wait scheduler_event; worker_next ())
+ else if count_active () > Multithreading.max_threads_value () then
+ (worker_wait scheduler_event; worker_next ())
else
- (case change_result queue Task_Queue.dequeue of
+ (case change_result queue (Task_Queue.dequeue (Thread.self ())) of
NONE => (worker_wait work_available; worker_next ())
| some => some);
@@ -224,13 +215,15 @@
| SOME work => (execute name work; worker_loop name));
fun worker_start name = (*requires SYNCHRONIZED*)
- change workers (cons (SimpleThread.fork false (fn () => worker_loop name), true));
+ change workers (cons (SimpleThread.fork false (fn () =>
+ (broadcast scheduler_event; worker_loop name)), true));
(* scheduler *)
val last_status = ref Time.zeroTime;
-val next_status = Time.fromMilliseconds 450;
+val next_status = Time.fromMilliseconds 500;
+val next_round = Time.fromMilliseconds 50;
fun scheduler_next () = (*requires SYNCHRONIZED*)
let
@@ -243,7 +236,7 @@
let
val {ready, pending, running} = Task_Queue.status (! queue);
val total = length (! workers);
- val active = count_active (! workers);
+ val active = count_active ();
in
"SCHEDULE: " ^
string_of_int ready ^ " ready, " ^
@@ -270,19 +263,16 @@
val _ = excessive := l - mm;
val _ =
if mm > l then
- (funpow (mm - l) (fn () => worker_start ("worker " ^ string_of_int (inc next))) ();
- broadcast scheduler_event)
+ funpow (mm - l) (fn () => worker_start ("worker " ^ string_of_int (inc next))) ()
else ();
(*canceled groups*)
val _ =
if null (! canceled) then ()
- else (change canceled (filter_out (Task_Queue.cancel (! queue))); broadcast_all ());
+ else (change canceled (filter_out (Task_Queue.cancel (! queue))); broadcast_work ());
(*delay loop*)
- val delay =
- Time.fromMilliseconds (if not (! do_shutdown) andalso null (! canceled) then 500 else 50);
- val _ = wait_interruptible scheduler_event delay
+ val _ = wait_interruptible scheduler_event next_round
handle Exn.Interrupt =>
(Multithreading.tracing 1 (fn () => "Interrupt");
List.app do_cancel (Task_Queue.cancel_all (! queue)));
@@ -302,9 +292,8 @@
fun scheduler_check () = (*requires SYNCHRONIZED*)
(do_shutdown := false;
- if not (scheduler_active ()) then
- (scheduler := SOME (SimpleThread.fork false scheduler_loop); broadcast scheduler_event)
- else ());
+ if scheduler_active () then ()
+ else scheduler := SOME (SimpleThread.fork false scheduler_loop));
@@ -319,7 +308,7 @@
SOME group => group
| NONE => Task_Queue.new_group (worker_group ()));
val (result, job) = future_job group e;
- val task = SYNCHRONIZED "future" (fn () =>
+ val task = SYNCHRONIZED "enqueue" (fn () =>
let
val (task, minimal) = change_result queue (Task_Queue.enqueue group deps pri job);
val _ = if minimal then signal work_available else ();
@@ -345,14 +334,12 @@
| SOME res => res);
fun join_wait x =
- if SYNCHRONIZED "join_wait" (fn () =>
- is_finished x orelse (wait work_finished; false))
- then () else join_wait x;
+ Synchronized.guarded_access (result_of x) (fn NONE => NONE | some => SOME ((), some));
fun join_next deps = (*requires SYNCHRONIZED*)
if null deps then NONE
else
- (case change_result queue (Task_Queue.dequeue_towards deps) of
+ (case change_result queue (Task_Queue.dequeue_towards (Thread.self ()) deps) of
(NONE, []) => NONE
| (NONE, deps') => (worker_wait work_finished; join_next deps')
| (SOME work, deps') => SOME (work, deps'));
@@ -366,14 +353,13 @@
fun join_results xs =
if forall is_finished xs then map get_result xs
+ else if Multithreading.self_critical () then
+ error "Cannot join future values within critical section"
else uninterruptible (fn _ => fn () =>
- let
- val _ = Multithreading.self_critical () andalso
- error "Cannot join future values within critical section";
- val _ =
- if is_worker () then join_work (map task_of xs)
- else List.app join_wait xs;
- in map get_result xs end) ();
+ (if is_worker ()
+ then join_work (map task_of xs)
+ else List.app join_wait xs;
+ map get_result xs)) ();
end;
@@ -389,7 +375,7 @@
val group = Task_Queue.new_group (SOME (group_of x));
val (result, job) = future_job group (fn () => f (join x));
- val extended = SYNCHRONIZED "map_future" (fn () =>
+ val extended = SYNCHRONIZED "extend" (fn () =>
(case Task_Queue.extend task job (! queue) of
SOME queue' => (queue := queue'; true)
| NONE => false));
@@ -403,11 +389,12 @@
fun interruptible_task f x =
if Multithreading.available then
+ (Thread.testInterrupt ();
Multithreading.with_attributes
(if is_worker ()
then Multithreading.restricted_interrupts
else Multithreading.regular_interrupts)
- (fn _ => f) x
+ (fn _ => fn x => f x) x)
else interruptible f x;
(*cancel: present and future group members will be interrupted eventually*)
@@ -421,7 +408,7 @@
if Multithreading.available then
SYNCHRONIZED "shutdown" (fn () =>
while scheduler_active () do
- (wait scheduler_event; broadcast_all ()))
+ (wait scheduler_event; broadcast_work ()))
else ();
--- a/src/Pure/Concurrent/par_list.ML Tue Jul 28 13:38:13 2009 +0200
+++ b/src/Pure/Concurrent/par_list.ML Tue Jul 28 20:26:39 2009 +0200
@@ -27,10 +27,8 @@
struct
fun raw_map f xs =
- if Future.enabled () then
- let val group = Task_Queue.new_group (Future.worker_group ())
- in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end
- else map (Exn.capture f) xs;
+ let val group = Task_Queue.new_group (Future.worker_group ())
+ in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end;
fun map f xs = Exn.release_first (raw_map f xs);
--- a/src/Pure/Concurrent/synchronized.ML Tue Jul 28 13:38:13 2009 +0200
+++ b/src/Pure/Concurrent/synchronized.ML Tue Jul 28 20:26:39 2009 +0200
@@ -8,6 +8,7 @@
sig
type 'a var
val var: string -> 'a -> 'a var
+ val peek: 'a var -> 'a
val value: 'a var -> 'a
val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
@@ -32,6 +33,8 @@
cond = ConditionVar.conditionVar (),
var = ref x};
+fun peek (Var {var, ...}) = ! var; (*unsynchronized!*)
+
fun value (Var {name, lock, cond, var}) = SimpleThread.synchronized name lock (fn () => ! var);
--- a/src/Pure/Concurrent/task_queue.ML Tue Jul 28 13:38:13 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Tue Jul 28 20:26:39 2009 +0200
@@ -26,8 +26,8 @@
val cancel_all: queue -> group list
val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> (task * bool) * queue
val extend: task -> (bool -> bool) -> queue -> queue option
- val dequeue: queue -> (task * group * (bool -> bool) list) option * queue
- val dequeue_towards: task list -> queue ->
+ val dequeue: Thread.thread -> queue -> (task * group * (bool -> bool) list) option * queue
+ val dequeue_towards: Thread.thread -> task list -> queue ->
(((task * group * (bool -> bool) list) option * task list) * queue)
val finish: task -> queue -> bool * queue
end;
@@ -52,11 +52,11 @@
datatype group = Group of
{parent: group option,
id: serial,
- status: exn list ref};
+ status: exn list Synchronized.var};
fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status};
-fun new_group parent = make_group (parent, serial (), ref []);
+fun new_group parent = make_group (parent, serial (), Synchronized.var "group" []);
fun group_id (Group {id, ...}) = id;
fun eq_group (group1, group2) = group_id group1 = group_id group2;
@@ -67,16 +67,20 @@
(* group status *)
-fun cancel_group (Group {status, ...}) exn = CRITICAL (fn () =>
- (case exn of
- Exn.Interrupt => if null (! status) then status := [exn] else ()
- | _ => change status (cons exn)));
+fun cancel_group (Group {status, ...}) exn =
+ Synchronized.change status
+ (fn exns =>
+ (case exn of
+ Exn.Interrupt => if null exns then [exn] else exns
+ | _ => exn :: exns));
-fun is_canceled (Group {parent, status, ...}) = (*non-critical*)
- not (null (! status)) orelse (case parent of NONE => false | SOME group => is_canceled group);
+fun is_canceled (Group {parent, status, ...}) =
+ not (null (Synchronized.value status)) orelse
+ (case parent of NONE => false | SOME group => is_canceled group);
-fun group_status (Group {parent, status, ...}) = (*non-critical*)
- ! status @ (case parent of NONE => [] | SOME group => group_status group);
+fun group_status (Group {parent, status, ...}) =
+ Synchronized.value status @
+ (case parent of NONE => [] | SOME group => group_status group);
fun str_of_group group =
(is_canceled group ? enclose "(" ")") (string_of_int (group_id group));
@@ -94,6 +98,12 @@
fun get_job (jobs: jobs) task = #2 (Task_Graph.get_node jobs task);
fun set_job task job (jobs: jobs) = Task_Graph.map_node task (fn (group, _) => (group, job)) jobs;
+fun add_job task dep (jobs: jobs) =
+ Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
+
+fun get_deps (jobs: jobs) task =
+ Task_Graph.imm_preds jobs task handle Task_Graph.UNDEF _ => [];
+
(* queue of grouped jobs *)
@@ -147,12 +157,6 @@
(* enqueue *)
-fun add_job task dep (jobs: jobs) =
- Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
-
-fun get_deps (jobs: jobs) task =
- Task_Graph.imm_preds jobs task handle Task_Graph.UNDEF _ => [];
-
fun enqueue group deps pri job (Queue {groups, jobs, cache}) =
let
val task = new_task pri;
@@ -179,7 +183,7 @@
(* dequeue *)
-fun dequeue (queue as Queue {groups, jobs, cache}) =
+fun dequeue thread (queue as Queue {groups, jobs, cache}) =
let
fun ready (task, ((group, Job list), ([], _))) = SOME (task, group, rev list)
| ready _ = NONE;
@@ -188,7 +192,7 @@
NONE => (NONE, make_queue groups jobs No_Result)
| SOME (result as (task, _, _)) =>
let
- val jobs' = set_job task (Running (Thread.self ())) jobs;
+ val jobs' = set_job task (Running thread) jobs;
val cache' = Result task;
in (SOME result, make_queue groups jobs' cache') end);
in
@@ -201,26 +205,26 @@
(* dequeue_towards -- adhoc dependencies *)
-fun dequeue_towards deps (queue as Queue {groups, jobs, ...}) =
+fun dequeue_towards thread deps (queue as Queue {groups, jobs, ...}) =
let
fun ready task =
(case Task_Graph.get_node jobs task of
(group, Job list) =>
- if null (Task_Graph.imm_preds jobs task)
+ if null (get_deps jobs task)
then SOME (task, group, rev list)
else NONE
| _ => NONE);
val tasks = filter (can (Task_Graph.get_node jobs)) deps;
fun result (res as (task, _, _)) =
let
- val jobs' = set_job task (Running (Thread.self ())) jobs;
+ val jobs' = set_job task (Running thread) jobs;
val cache' = Unknown;
in ((SOME res, tasks), make_queue groups jobs' cache') end;
in
(case get_first ready tasks of
SOME res => result res
| NONE =>
- (case get_first (get_first ready o Task_Graph.imm_preds jobs) tasks of
+ (case get_first (get_first ready o get_deps jobs) tasks of
SOME res => result res
| NONE => ((NONE, tasks), queue)))
end;
--- a/src/Pure/goal.ML Tue Jul 28 13:38:13 2009 +0200
+++ b/src/Pure/goal.ML Tue Jul 28 20:26:39 2009 +0200
@@ -103,7 +103,7 @@
val parallel_proofs = ref 1;
fun future_enabled () =
- Future.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
+ Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2;