author | wenzelm |
Fri, 03 Oct 2008 16:37:09 +0200 | |
changeset 28477 | 9339d4dcec8b |
child 28478 | 855ca2dcc03d |
permissions | -rw-r--r-- |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/atp_manager.ML |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
3 |
Author: Fabian Immler, TU Muenchen |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
4 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
5 |
ATP threads have to be registered here. Threads with the same |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
6 |
birth-time are seen as one group. All threads of a group are killed |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
7 |
when one thread of it has been successful, or after a certain time, or |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
8 |
when the maximum number of threads exceeds; then the oldest thread is |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
9 |
killed. |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
10 |
*) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
11 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
12 |
signature PROVERS = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
13 |
sig |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
14 |
type T |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
15 |
val get : Context.theory -> T |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
16 |
val init : Context.theory -> Context.theory |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
17 |
val map : |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
18 |
(T -> T) -> |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
19 |
Context.theory -> Context.theory |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
20 |
val put : T -> Context.theory -> Context.theory |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
21 |
end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
22 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
23 |
signature ATP_MANAGER = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
24 |
sig |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
25 |
val kill_all: unit -> unit |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
26 |
val info: unit -> unit |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
27 |
val set_atps: string -> unit |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
28 |
val set_max_atp: int -> unit |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
29 |
val set_timeout: int -> unit |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
30 |
val set_groupkilling: bool -> unit |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
31 |
val start: unit -> unit |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
32 |
val register: Time.time -> Time.time -> (Thread.thread * string) -> unit |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
33 |
val unregister: bool -> unit |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
34 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
35 |
structure Provers : PROVERS |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
36 |
val sledgehammer: Toplevel.state -> unit |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
37 |
end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
38 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
39 |
structure AtpManager : ATP_MANAGER = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
40 |
struct |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
41 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
42 |
structure ThreadHeap = HeapFun ( |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
43 |
struct |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
44 |
type elem = (Time.time * Thread.thread); |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
45 |
fun ord ((a,_),(b,_)) = Time.compare (a, b); |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
46 |
end); |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
47 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
48 |
(* create global state of threadmanager *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
49 |
val timeout_heap = ref ThreadHeap.empty |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
50 |
val oldest_heap = ref ThreadHeap.empty |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
51 |
(* managed threads *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
52 |
val active = ref ([] : (Thread.thread * Time.time * Time.time * string) list) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
53 |
val cancelling = ref ([] : (Thread.thread * Time.time * Time.time * string) list) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
54 |
(* settings *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
55 |
val atps = ref "e,spass" |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
56 |
val maximum_atps = ref 5 (* ~1 means infinite number of atps*) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
57 |
val timeout = ref 60 |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
58 |
val groupkilling = ref true |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
59 |
(* synchronizing *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
60 |
val lock = Mutex.mutex () (* to be aquired for changing state *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
61 |
val state_change = ConditionVar.conditionVar () (* signal when state changes *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
62 |
(* watches over running threads and interrupts them if required *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
63 |
val managing_thread = ref (Thread.fork (fn () => (), [])) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
64 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
65 |
(* move a thread from active to cancelling |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
66 |
managing_thread trys to interrupt all threads in cancelling |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
67 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
68 |
call from an environment where a lock has already been aquired *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
69 |
fun unregister_locked thread = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
70 |
let val entrys = (filter (fn (t,_,_,_) => Thread.equal (t, thread))) (! active) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
71 |
val entrys_update = map (fn (th, tb, _, desc) => (th, tb, Time.now(), desc)) entrys |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
72 |
val _ = change cancelling (append entrys_update) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
73 |
val _ = change active (filter_out (fn (t,_,_,_) => Thread.equal (t, thread))) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
74 |
in () end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
75 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
76 |
(* start a watching thread which runs forever *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
77 |
(* must *not* be called more than once!! => problem with locks *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
78 |
fun start () = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
79 |
let |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
80 |
val new_thread = Thread.fork (fn () => |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
81 |
let |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
82 |
(* never give up lock except for waiting *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
83 |
val _ = Mutex.lock lock |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
84 |
fun wait_for_next_event time = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
85 |
let |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
86 |
(* wait for signal or next timeout, give up lock meanwhile *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
87 |
val _ = ConditionVar.waitUntil (state_change, lock, time) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
88 |
(* move threads with priority less than Time.now() to cancelling *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
89 |
fun cancelolder heap = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
90 |
if ThreadHeap.is_empty heap then heap else |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
91 |
let val (mintime, minthread) = ThreadHeap.min heap |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
92 |
in |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
93 |
if mintime > Time.now() then heap |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
94 |
else (unregister_locked minthread; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
95 |
cancelolder (ThreadHeap.delete_min heap)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
96 |
end |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
97 |
val _ = change timeout_heap cancelolder |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
98 |
(* try to interrupt threads that are to cancel*) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
99 |
fun interrupt t = Thread.interrupt t handle Thread _ => () |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
100 |
val _ = change cancelling (filter (fn (t,_,_,_) => Thread.isActive t)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
101 |
val _ = map (fn (t, _, _, _) => interrupt t) (! cancelling) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
102 |
(* if there are threads to cancel, send periodic interrupts *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
103 |
(* TODO: find out what realtime-values are appropriate *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
104 |
val next_time = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
105 |
if length (! cancelling) > 0 then |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
106 |
Time.now() + Time.fromMilliseconds 300 |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
107 |
else if ThreadHeap.is_empty (! timeout_heap) then |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
108 |
Time.now() + Time.fromSeconds 10 |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
109 |
else |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
110 |
#1 (ThreadHeap.min (! timeout_heap)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
111 |
in |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
112 |
wait_for_next_event next_time |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
113 |
end |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
114 |
in wait_for_next_event Time.zeroTime end, |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
115 |
[Thread.InterruptState Thread.InterruptDefer]) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
116 |
in managing_thread := new_thread end |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
117 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
118 |
(* calling thread registers itself to be managed here with a relative timeout *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
119 |
fun register birthtime deadtime (thread, name) = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
120 |
let |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
121 |
val _ = Mutex.lock lock |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
122 |
(* create the atp-managing-thread if this is the first call to register *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
123 |
val _ = if Thread.isActive (! managing_thread) then () else start () |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
124 |
(* insertion *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
125 |
val _ = change timeout_heap (ThreadHeap.insert (deadtime, thread)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
126 |
val _ = change oldest_heap (ThreadHeap.insert (birthtime, thread)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
127 |
val _ = change active (cons (thread, birthtime, deadtime, name)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
128 |
(*maximum number of atps must not exceed*) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
129 |
val _ = let |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
130 |
fun kill_oldest () = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
131 |
let val (_, oldest_thread) = ThreadHeap.min (!oldest_heap) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
132 |
val _ = change oldest_heap (ThreadHeap.delete_min) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
133 |
in unregister_locked oldest_thread end |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
134 |
in |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
135 |
while ! maximum_atps > ~1 andalso length (! active) > ! maximum_atps |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
136 |
do kill_oldest () |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
137 |
end |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
138 |
(* state of threadmanager changed => signal *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
139 |
val _ = ConditionVar.signal state_change |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
140 |
val _ = Mutex.unlock lock |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
141 |
in () end |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
142 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
143 |
(* calling Thread unregisters itself from Threadmanager; thread is responsible |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
144 |
to terminate after calling this method *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
145 |
fun unregister success = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
146 |
let val _ = Mutex.lock lock |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
147 |
val thread = Thread.self () |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
148 |
(* get birthtime of unregistering thread - for group-killing*) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
149 |
fun get_birthtime [] = Time.zeroTime |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
150 |
| get_birthtime ((t,tb,td,desc)::actives) = if Thread.equal (thread, t) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
151 |
then tb |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
152 |
else get_birthtime actives |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
153 |
val birthtime = get_birthtime (! active) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
154 |
(* remove unregistering thread *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
155 |
val _ = change active (filter_out (fn (t,_,_,_) => Thread.equal (t, thread))) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
156 |
val _ = if (! groupkilling) andalso success |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
157 |
then (* remove all threads of the same group *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
158 |
let |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
159 |
val group_threads = filter (fn (_, tb, _, _) => tb = birthtime) (! active) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
160 |
val _ = change cancelling (append group_threads) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
161 |
val _ = change active (filter_out (fn (_, tb, _, _) => tb = birthtime)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
162 |
in () end |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
163 |
else () |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
164 |
val _ = ConditionVar.signal state_change |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
165 |
val _ = Mutex.unlock lock |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
166 |
in () end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
167 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
168 |
(* Move all threads to cancelling *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
169 |
fun kill_all () = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
170 |
let |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
171 |
val _ = Mutex.lock lock |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
172 |
val _ = change active (map (fn (th, tb, _, desc) => (th, tb, Time.now(), desc))) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
173 |
val _ = change cancelling (append (! active)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
174 |
val _ = change active (fn _ => []) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
175 |
val _ = ConditionVar.signal state_change |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
176 |
val _ = Mutex.unlock lock |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
177 |
in () end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
178 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
179 |
fun info () = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
180 |
let |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
181 |
val _ = Mutex.lock lock |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
182 |
fun running_info (_, birth_time, dead_time, desc) = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
183 |
priority ("Running: " |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
184 |
^ ((Int.toString o Time.toSeconds) (Time.now() - birth_time)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
185 |
^ " s -- " |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
186 |
^ ((Int.toString o Time.toSeconds) (dead_time - Time.now())) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
187 |
^ " s to live:\n" ^ desc) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
188 |
fun cancelling_info (_, _, dead_time, desc) = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
189 |
priority ("Trying to interrupt thread since " |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
190 |
^ (Int.toString o Time.toSeconds) (Time.now() - dead_time) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
191 |
^ " s:\n" ^ desc ) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
192 |
val _ = if length (! active) = 0 then [priority "No ATPs running."] |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
193 |
else (priority "--- RUNNING ATPs ---"; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
194 |
map (fn entry => running_info entry) (! active)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
195 |
val _ = if length (! cancelling) = 0 then [] |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
196 |
else (priority "--- TRYING TO INTERRUPT FOLLOWING ATPs ---"; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
197 |
map (fn entry => cancelling_info entry) (! cancelling)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
198 |
val _ = Mutex.unlock lock |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
199 |
in () end; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
200 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
201 |
(* integration into ProofGeneral *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
202 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
203 |
fun set_max_atp number = CRITICAL (fn () => maximum_atps := number); |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
204 |
fun set_atps str = CRITICAL (fn () => atps := str); |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
205 |
fun set_timeout time = CRITICAL (fn () => timeout := time); |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
206 |
fun set_groupkilling boolean = CRITICAL (fn () => groupkilling := boolean); |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
207 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
208 |
(* some settings will be accessible via Isabelle -> Settings *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
209 |
val _ = ProofGeneralPgip.add_preference "Proof" |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
210 |
{name = "ATP - Provers (e,vampire,spass)", |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
211 |
descr = "Which external automatic provers (seperated by commas)", |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
212 |
default = !atps, |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
213 |
pgiptype = PgipTypes.Pgipstring, |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
214 |
get = fn () => !atps, |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
215 |
set = set_atps} handle Error => warning "Preference already exists"; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
216 |
val _ = ProofGeneralPgip.add_preference "Proof" |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
217 |
{name = "ATP - Maximum number", |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
218 |
descr = "How many provers may run parallel", |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
219 |
default = Int.toString (! maximum_atps), |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
220 |
pgiptype = PgipTypes.Pgipstring, |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
221 |
get = fn () => Int.toString (! maximum_atps), |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
222 |
set = (fn str => let val int_opt = Int.fromString str |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
223 |
val nr = if isSome int_opt then valOf int_opt else 1 |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
224 |
in set_max_atp nr end)} handle Error => warning "Preference already exists"; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
225 |
val _ = ProofGeneralPgip.add_preference "Proof" |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
226 |
{name = "ATP - Timeout", |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
227 |
descr = "ATPs will be interrupted after this time (in seconds)", |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
228 |
default = Int.toString (! timeout), |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
229 |
pgiptype = PgipTypes.Pgipstring, |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
230 |
get = fn () => Int.toString (! timeout), |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
231 |
set = (fn str => let val int_opt = Int.fromString str |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
232 |
val nr = if isSome int_opt then valOf int_opt else 60 |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
233 |
in set_timeout nr end)} handle Error => warning "Preference already exists"; |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
234 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
235 |
(* Additional Provers can be added as follows: |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
236 |
SPASS with max_new 40 and theory_const false, timeout 60 |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
237 |
setup{* AtpManager.Provers.map (Symtab.update ("spass2", AtpThread.spass 40 false 60)) *} |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
238 |
arbitrary prover supporting tptp-input/output |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
239 |
setup{* AtpManagerProvers.map (Symtab.update ("tptp", AtpThread.tptp_prover "path/to/prover -options" 60)) *} |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
240 |
*) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
241 |
structure Provers = TheoryDataFun |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
242 |
( |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
243 |
type T = (Toplevel.state -> (Thread.thread * string)) Symtab.table |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
244 |
val empty = Symtab.empty |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
245 |
val copy = I |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
246 |
val extend = I |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
247 |
fun merge _ = Symtab.merge (K true) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
248 |
); |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
249 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
250 |
(* sledghammer: *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
251 |
fun sledgehammer state = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
252 |
let |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
253 |
val proverids = String.tokens (fn c => c = #",") (! atps) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
254 |
(* get context *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
255 |
val (ctxt, _) = Proof.get_goal (Toplevel.proof_of state) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
256 |
val thy = ProofContext.theory_of ctxt |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
257 |
(* get prover-functions *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
258 |
val lookups = map (fn prover => Symtab.lookup (Provers.get thy) prover) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
259 |
proverids |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
260 |
val filtered_calls = filter (fn call => isSome call) lookups |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
261 |
val calls = map (fn some => valOf some) filtered_calls |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
262 |
(* call provers *) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
263 |
val threads_names = map (fn call => call state) calls |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
264 |
val birthtime = Time.now() |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
265 |
val deadtime = Time.now() + (Time.fromSeconds (! timeout)) |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
266 |
val _ = map (register birthtime deadtime) threads_names |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
267 |
in () end |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
268 |
|
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
269 |
val _ = |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
270 |
OuterSyntax.command "sledgehammer" "call all automatic theorem provers" OuterKeyword.diag |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
271 |
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer)); |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff
changeset
|
272 |
end; |