# HG changeset patch # User wenzelm # Date 1248805599 -7200 # Node ID 99711ef9d582249ab73e9e93374fe8c0b8c3b05d # Parent b1c2110ae6810b00fa4db5338aad8a3d9d6ff9b4# Parent 8b03a3daba5da3faed6fe405553468a8cd2f57f2 merged diff -r b1c2110ae681 -r 99711ef9d582 src/HOL/Tools/atp_wrapper.ML --- 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; - diff -r b1c2110ae681 -r 99711ef9d582 src/HOL/Tools/res_axioms.ML --- 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"; diff -r b1c2110ae681 -r 99711ef9d582 src/HOL/Tools/res_reconstruct.ML --- 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 === *) diff -r b1c2110ae681 -r 99711ef9d582 src/HOL/ex/ROOT.ML --- 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"; diff -r b1c2110ae681 -r 99711ef9d582 src/Pure/Concurrent/future.ML --- 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 (); diff -r b1c2110ae681 -r 99711ef9d582 src/Pure/Concurrent/par_list.ML --- 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); diff -r b1c2110ae681 -r 99711ef9d582 src/Pure/Concurrent/synchronized.ML --- 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); diff -r b1c2110ae681 -r 99711ef9d582 src/Pure/Concurrent/task_queue.ML --- 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; diff -r b1c2110ae681 -r 99711ef9d582 src/Pure/goal.ML --- 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;