--- a/src/HOL/Tools/atp_manager.ML Tue Oct 14 13:01:57 2008 +0200
+++ b/src/HOL/Tools/atp_manager.ML Tue Oct 14 13:01:58 2008 +0200
@@ -12,11 +12,10 @@
signature ATP_MANAGER =
sig
val kill_all: unit -> unit
- val info: unit -> string
+ val info: unit -> unit
val set_atps: string -> unit
val set_max_atp: int -> unit
val set_timeout: int -> unit
-
val atp_thread: (unit -> 'a option) -> ('a -> string) -> Thread.thread
val add_prover: string -> (int -> Proof.state -> Thread.thread) -> theory -> theory
val print_provers: theory -> unit
@@ -26,157 +25,141 @@
structure AtpManager : ATP_MANAGER =
struct
- structure ThreadHeap = HeapFun
- (
- type elem = Time.time * Thread.thread;
- fun ord ((a, _), (b, _)) = Time.compare (a, b);
- )
+(* data structures over threads *)
+
+structure ThreadHeap = HeapFun
+(
+ type elem = Time.time * Thread.thread;
+ fun ord ((a, _), (b, _)) = Time.compare (a, b);
+)
+
+val lookup_thread = AList.lookup Thread.equal;
+val delete_thread = AList.delete Thread.equal;
+val update_thread = AList.update Thread.equal;
+
+
+(* state of thread manager *)
- (* state of threadmanager *)
- datatype T = State of {
- timeout_heap: ThreadHeap.T,
- oldest_heap: ThreadHeap.T,
- (* managed threads *)
- active: (Thread.thread * (Time.time * Time.time * string)) list,
- cancelling: (Thread.thread * (Time.time * Time.time * string)) list
- }
- val state = ref (State {
- timeout_heap = ThreadHeap.empty,
- oldest_heap = ThreadHeap.empty,
- active = [],
- cancelling = []})
-
- (* synchronizing *)
- val lock = Mutex.mutex ()
- val state_change = ConditionVar.conditionVar ()
- (* watches over running threads and interrupts them if required *)
- val managing_thread = ref (NONE: Thread.thread option);
+datatype T = State of
+ {timeout_heap: ThreadHeap.T,
+ oldest_heap: ThreadHeap.T,
+ active: (Thread.thread * (Time.time * Time.time * string)) list,
+ cancelling: (Thread.thread * (Time.time * Time.time * string)) list};
+
+fun make_state timeout_heap oldest_heap active cancelling =
+ State {timeout_heap = timeout_heap, oldest_heap = oldest_heap,
+ active = active, cancelling = cancelling};
+
+val state = Synchronized.var "atp_manager" (make_state ThreadHeap.empty ThreadHeap.empty [] []);
- (* active and cancelling are association lists *)
- val lookup_th = AList.lookup Thread.equal;
- val delete_th = AList.delete Thread.equal;
- val update_th = AList.update Thread.equal;
-
-
- (* waiting for a condition, checking it after time or when signalled
- then changing state with returning a result *)
- fun protected_wait_change_result P time f = uninterruptible (fn restore => fn () =>
- let
- val _ = Mutex.lock lock;
- val _ = while not (P (! state)) do ConditionVar.waitUntil (state_change, lock, time (! state));
- val res = Exn.Result (restore (fn () => change_result state f) ()) handle exn => Exn.Exn exn
- val _ = ConditionVar.broadcast state_change;
- val _ = Mutex.unlock lock;
- in Exn.release res end) ()
-
- fun protected_change f = protected_wait_change_result (fn _ => true) (fn _ => Time.zeroTime) f;
-
- fun protected f = protected_change (`f);
+
+(* the thread manager thread *)
+
+(*watches over running threads and interrupts them if required*)
+val managing_thread = ref (NONE: Thread.thread option);
- (* unregister Thread from Threadmanager = move to cancelling *)
- fun unregister success message thread = protected_change (fn State {timeout_heap, oldest_heap, active, cancelling} =>
+
+(* unregister thread from thread manager -- move to cancelling *)
+
+fun unregister success message thread = Synchronized.change_result state
+ (fn State {timeout_heap, oldest_heap, active, cancelling} =>
let
- val info = lookup_th active thread
- (* get birthtime of unregistering thread if successful - for group-killing*)
- val birthtime = case info of NONE => Time.zeroTime
- | SOME (tb, _, _) => if success then tb else Time.zeroTime
- (* move unregistering thread to cancelling *)
- val active' = delete_th thread active
- val cancelling' = case info of NONE => cancelling
- | SOME (tb, _, desc) => update_th (thread, (tb, Time.now(), desc)) cancelling
- (* move all threads of the same group to cancelling *)
- val group_threads = map_filter (fn (th, (tb, _, desc)) =>
- if tb = birthtime then SOME (th, (tb, Time.now(), desc)) else NONE)
- active
- val active'' = filter_out (fn (_, (tb, _, _)) => tb = birthtime) active'
- val cancelling'' = append group_threads cancelling'
- (* message for user *)
- val message = case info of NONE => ""
- | SOME (_, _, desc) => "Sledgehammer: " ^ desc ^ "\n " ^ message ^
- (if length group_threads > 1
- then "\n\nInterrupted " ^ Int.toString (length group_threads - 1) ^ " others of group."
- else "")
- in (message, State {timeout_heap = timeout_heap,
- oldest_heap = oldest_heap,
- active = active'',
- cancelling = cancelling''})
- end)
-
- (* start a watching thread which runs forever - only one may exist => checked by register *)
- fun start () = managing_thread := SOME (SimpleThread.fork false (fn () =>
+ val info = lookup_thread active thread
+
+ (* get birthtime of unregistering thread if successful - for group-killing*)
+ val birthtime = case info of NONE => Time.zeroTime
+ | SOME (tb, _, _) => if success then tb else Time.zeroTime
+
+ (* move unregistering thread to cancelling *)
+ val active' = delete_thread thread active
+ val cancelling' = case info of NONE => cancelling
+ | SOME (tb, _, desc) => update_thread (thread, (tb, Time.now (), desc)) cancelling
+
+ (* move all threads of the same group to cancelling *)
+ val group_threads = active |> map_filter (fn (th, (tb, _, desc)) =>
+ if tb = birthtime then SOME (th, (tb, Time.now (), desc)) else NONE)
+ val active'' = filter_out (fn (_, (tb, _, _)) => tb = birthtime) active'
+ val cancelling'' = append group_threads cancelling'
+
+ (* message for user *)
+ val message' = case info of NONE => ""
+ | SOME (_, _, desc) => "Sledgehammer: " ^ desc ^ "\n " ^ message ^
+ (if null group_threads then ""
+ else "\nInterrupted " ^ Int.toString (length group_threads - 1) ^ " other group members")
+ in (message', make_state timeout_heap oldest_heap active'' cancelling'') end);
+
+
+(* start a watching thread which runs forever -- only one may exist *)
+
+fun check_thread_manager () =
+ if (case ! managing_thread of SOME thread => Thread.isActive thread | NONE => false)
+ then () else managing_thread := SOME (SimpleThread.fork false (fn () =>
let
- val min_wait_time = Time.fromMilliseconds 300
- val max_wait_time = Time.fromSeconds 10
- (* action is required when there are cancelling threads, or a thread is to be cancelled *)
- fun P (State {timeout_heap, oldest_heap, active, cancelling}) =
- length cancelling > 0 orelse
- (not (ThreadHeap.is_empty timeout_heap) andalso
- Time.< (#1 (ThreadHeap.min timeout_heap), Time.now ()))
- (* wait for next thread to cancel, or a maximum of 10 Seconds*)
- fun time (State {timeout_heap, oldest_heap, active, cancelling}) =
- if ThreadHeap.is_empty timeout_heap then Time.+ (Time.now(), max_wait_time)
- else #1 (ThreadHeap.min timeout_heap)
- (* action: cancel find threads whose timeout is reached, and interrupt cancelling threads *)
- fun action (State {timeout_heap, oldest_heap, active, cancelling}) =
- let
- (* find out threads wich reached their timeout *)
- fun find_threads (heap, threads) =
- if ThreadHeap.is_empty heap then (heap, threads) else
- let val (mintime, minthread) = ThreadHeap.min heap
- in if Time.> (mintime, Time.now())
- then (heap, threads)
- else find_threads (ThreadHeap.delete_min heap, minthread :: threads)
- end
- val (timeout_heap', timeout_threads) = find_threads (timeout_heap, [])
- val _ = List.app (SimpleThread.interrupt o fst) cancelling
- val cancelling' = filter (fn (t, _) => Thread.isActive t) cancelling
- (* return threads with timeout and changed state *)
- in (timeout_threads, State {timeout_heap = timeout_heap',
- oldest_heap = oldest_heap,
- active = active,
- cancelling = cancelling'})
- end
- in while true do
- (* cancel threads found by 'action' *)
- (map (priority o (unregister false "Interrupted (reached timeout)")) (protected_wait_change_result P time action);
+ val min_wait_time = Time.fromMilliseconds 300
+ val max_wait_time = Time.fromSeconds 10
+
+ (* wait for next thread to cancel, or maximum*)
+ fun time_limit (State {timeout_heap, ...}) =
+ (case try ThreadHeap.min timeout_heap of
+ NONE => SOME (Time.+ (Time.now (), max_wait_time))
+ | SOME (time, _) => SOME time)
+
+ (* action: cancel find threads whose timeout is reached, and interrupt cancelling threads *)
+ fun action (State {timeout_heap, oldest_heap, active, cancelling}) =
+ let val (timeout_threads, timeout_heap') =
+ ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap
+ in
+ if null timeout_threads andalso null cancelling then NONE
+ else
+ let
+ val _ = List.app (SimpleThread.interrupt o #1) cancelling
+ val cancelling' = filter (Thread.isActive o #1) cancelling
+ val state' = make_state timeout_heap' oldest_heap active cancelling'
+ in SOME (map #2 timeout_threads, state') end
+ end
+ in
+ while true do
+ ((* cancel threads found by action *)
+ Synchronized.timed_access state time_limit action
+ |> these
+ |> List.app (priority o unregister false "Interrupted (reached timeout)");
(* give threads time to respond to interrupt *)
OS.Process.sleep min_wait_time)
- end))
+ end));
+
+
+(* thread is registered here by sledgehammer *)
- (* calling thread is registered here by sledgehammer *)
- fun register birthtime deadtime (thread, desc) = protected_change (
- fn State {timeout_heap, oldest_heap, active, cancelling} =>
- let val _ = (* create the atp-managing-thread if this is the first call to register *)
- if (case ! managing_thread of SOME thread => Thread.isActive thread | NONE => false)
- then () else start ()
- (* insertion *)
- in ((),State {timeout_heap = ThreadHeap.insert (deadtime, thread) timeout_heap,
- oldest_heap = ThreadHeap.insert (birthtime, thread) oldest_heap,
- active = update_th (thread, (birthtime, deadtime, desc)) active,
- cancelling = cancelling})
- end)
+fun register birthtime deadtime (thread, desc) =
+ (check_thread_manager ();
+ Synchronized.change state (fn State {timeout_heap, oldest_heap, active, cancelling} =>
+ let
+ val timeout_heap' = ThreadHeap.insert (deadtime, thread) timeout_heap
+ val oldest_heap' = ThreadHeap.insert (birthtime, thread) oldest_heap
+ val active' = update_thread (thread, (birthtime, deadtime, desc)) active
+ in make_state timeout_heap' oldest_heap' active' cancelling end));
- (* Move all threads to cancelling *)
- fun kill_all () = protected_change (fn State {timeout_heap, oldest_heap, active, cancelling} =>
- let
- val active' = (map (fn (th, (tb, _, desc)) => (th, (tb, Time.now(), desc))) active)
- in ((),State {timeout_heap = timeout_heap,
- oldest_heap = oldest_heap,
- active = [],
- cancelling = append active' cancelling})
- end)
-
- (* give information on running threads *)
- fun info () = protected (fn State {timeout_heap, oldest_heap, active, cancelling} =>
- let
+(* move all threads to cancelling *)
+
+fun kill_all () = Synchronized.change state
+ (fn State {timeout_heap, oldest_heap, active, cancelling} =>
+ let val formerly_active = map (fn (th, (tb, _, desc)) => (th, (tb, Time.now (), desc))) active
+ in make_state timeout_heap oldest_heap [] (formerly_active @ cancelling) end);
+
+
+(* information on running threads *)
+
+fun info () =
+ let
+ val State {timeout_heap, oldest_heap, active, cancelling} = Synchronized.value state
fun running_info (_, (birth_time, dead_time, desc)) = "Running: "
- ^ ((Int.toString o Time.toSeconds) (Time.- (Time.now(), birth_time)))
+ ^ ((Int.toString o Time.toSeconds) (Time.- (Time.now (), birth_time)))
^ " s -- "
- ^ ((Int.toString o Time.toSeconds) (Time.- (dead_time, Time.now())))
+ ^ ((Int.toString o Time.toSeconds) (Time.- (dead_time, Time.now ())))
^ " s to live:\n" ^ desc
fun cancelling_info (_, (_, dead_time, desc)) = "Trying to interrupt thread since "
- ^ (Int.toString o Time.toSeconds) (Time.- (Time.now(), dead_time))
+ ^ (Int.toString o Time.toSeconds) (Time.- (Time.now (), dead_time))
^ " s:\n" ^ desc
val running = if null active then "No ATPs running."
else String.concatWith "\n\n" ("--- RUNNING ATPs ---" ::
@@ -184,147 +167,156 @@
val interrupting = if null cancelling then ""
else String.concatWith "\n\n" ("--- TRYING TO INTERRUPT FOLLOWING ATPs ---" ::
(map (fn entry => cancelling_info entry) cancelling))
- in running ^ "\n" ^ interrupting end)
+ in writeln (running ^ "\n" ^ interrupting) end;
+
+
+(* thread wrapping an atp-call *)
-
- (* thread wrapping an atp-call *)
-
- fun atp_thread call_prover produce_answer =
- SimpleThread.fork true (fn () =>
- let
- val result = call_prover ()
- val message = case result of NONE => "Failed."
- | SOME result => "Try this command: " ^ produce_answer result
- in priority (unregister (isSome result) message (Thread.self()))
- end handle Interrupt => ()
- )
+fun atp_thread call_prover produce_answer =
+ SimpleThread.fork true (fn () =>
+ let
+ val result = call_prover ()
+ val message = case result of NONE => "Failed."
+ | SOME result => "Try this command: " ^ produce_answer result
+ in priority (unregister (is_some result) message (Thread.self ()))
+ end handle Interrupt => ());
+
-
- (* preferences *)
+(* preferences *)
- val atps = ref "e spass"
- val maximum_atps = ref 5 (* ~1 means infinite number of atps*)
- val timeout = ref 60
- val groupkilling = ref true
- fun set_atps str = CRITICAL (fn () => atps := str);
- fun set_max_atp number = CRITICAL (fn () => maximum_atps := number);
- fun set_timeout time = CRITICAL (fn () => timeout := time);
+val atps = ref "e spass";
+val maximum_atps = ref 5; (* ~1 means infinite number of atps*)
+val timeout = ref 60;
+
+fun set_atps str = CRITICAL (fn () => atps := str);
+fun set_max_atp number = CRITICAL (fn () => maximum_atps := number);
+fun set_timeout time = CRITICAL (fn () => timeout := time);
- val _ = ProofGeneralPgip.add_preference "Proof"
- {name = "ATP - Provers (see print_atps)",
- descr = "Default automatic provers (seperated by whitespace)",
- default = !atps,
- pgiptype = PgipTypes.Pgipstring,
- get = fn () => !atps,
- set = set_atps}
- handle ERROR _ => warning "Preference already exists";
+val _ = ProofGeneralPgip.add_preference "Proof"
+ {name = "ATP - Provers (see print_atps)",
+ descr = "Default automatic provers (seperated by whitespace)",
+ default = !atps,
+ pgiptype = PgipTypes.Pgipstring,
+ get = fn () => !atps,
+ set = set_atps}
+ handle ERROR _ => warning "Preference already exists";
- val _ = ProofGeneralPgip.add_preference "Proof"
- {name = "ATP - Maximum number",
- descr = "How many provers may run in parallel",
- default = Int.toString (! maximum_atps),
- pgiptype = PgipTypes.Pgipstring,
- get = fn () => Int.toString (! maximum_atps),
- set = fn str => set_max_atp (the_default 1 (Int.fromString str))}
- handle ERROR _ => warning "Preference already exists";
+val _ = ProofGeneralPgip.add_preference "Proof"
+ {name = "ATP - Maximum number",
+ descr = "How many provers may run in parallel",
+ default = Int.toString (! maximum_atps),
+ pgiptype = PgipTypes.Pgipstring,
+ get = fn () => Int.toString (! maximum_atps),
+ set = fn str => set_max_atp (the_default 1 (Int.fromString str))}
+ handle ERROR _ => warning "Preference already exists";
- val _ = ProofGeneralPgip.add_preference "Proof"
- {name = "ATP - Timeout",
- descr = "ATPs will be interrupted after this time (in seconds)",
- default = Int.toString (! timeout),
- pgiptype = PgipTypes.Pgipstring,
- get = fn () => Int.toString (! timeout),
- set = fn str => set_timeout (the_default 60 (Int.fromString str))}
- handle ERROR _ => warning "Preference already exists";
+val _ = ProofGeneralPgip.add_preference "Proof"
+ {name = "ATP - Timeout",
+ descr = "ATPs will be interrupted after this time (in seconds)",
+ default = Int.toString (! timeout),
+ pgiptype = PgipTypes.Pgipstring,
+ get = fn () => Int.toString (! timeout),
+ set = fn str => set_timeout (the_default 60 (Int.fromString str))}
+ handle ERROR _ => warning "Preference already exists";
- (* named provers *)
-
- fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
+(* named provers *)
- structure Provers = TheoryDataFun
- (
- type T = ((int -> Proof.state -> Thread.thread) * stamp) Symtab.table
- val empty = Symtab.empty
- val copy = I
- val extend = I
- fun merge _ tabs : T = Symtab.merge (eq_snd op =) tabs
- handle Symtab.DUP dup => err_dup_prover dup;
- );
+fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
- fun add_prover name prover_fn =
- Provers.map (Symtab.update_new (name, (prover_fn, stamp ())))
- handle Symtab.DUP dup => err_dup_prover dup;
-
- fun print_provers thy = Pretty.writeln
- (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
-
- fun prover_desc state subgoal name =
- let val (ctxt, (chain_ths, goal)) = Proof.get_goal state
- in "External prover " ^ quote name ^ " for Subgoal " ^ Int.toString subgoal^ ":\n" ^ Syntax.string_of_term ctxt (List.nth(prems_of goal, subgoal-1)) end
-
- fun run_prover state subgoal name =
- (case Symtab.lookup (Provers.get (Proof.theory_of state)) name of
- NONE => (warning ("Unknown external prover: " ^ quote name); NONE)
- | SOME (prover_fn, _) => SOME (prover_fn subgoal state, prover_desc state subgoal name));
+structure Provers = TheoryDataFun
+(
+ type T = ((int -> Proof.state -> Thread.thread) * stamp) Symtab.table
+ val empty = Symtab.empty
+ val copy = I
+ val extend = I
+ fun merge _ tabs : T = Symtab.merge (eq_snd op =) tabs
+ handle Symtab.DUP dup => err_dup_prover dup;
+);
- fun kill_one () =
- let
- val oldest = protected_change (fn (s as State {timeout_heap , oldest_heap, active, cancelling}) =>
- if ThreadHeap.is_empty oldest_heap orelse length active <= !maximum_atps orelse ! maximum_atps = ~1 then (NONE, s)
- else
- let val (_, oldest_thread) = ThreadHeap.min (oldest_heap)
- in (SOME oldest_thread, State {timeout_heap = timeout_heap,
- oldest_heap = ThreadHeap.delete_min oldest_heap,
- active = active,
- cancelling = cancelling}) end)
- in case oldest of NONE => ()
- | SOME thread => priority (unregister false "Interrupted (Maximum number of ATPs exceeded)." thread) end
-
- fun kill_oldest (State {timeout_heap, oldest_heap, active, cancelling}) =
- if length active > !maximum_atps andalso !maximum_atps > ~1
- then let val _ = kill_one () in kill_oldest (! state) end
- else ()
-
-
- (* sledghammer for first subgoal *)
+fun add_prover name prover_fn =
+ Provers.map (Symtab.update_new (name, (prover_fn, stamp ())))
+ handle Symtab.DUP dup => err_dup_prover dup;
+
+fun print_provers thy = Pretty.writeln
+ (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
- fun sledgehammer names proof_state =
- let
- val proverids = case names of
- [] => String.tokens (Symbol.is_ascii_blank o String.str) (! atps)
- | names => names
- val threads_names = map_filter (run_prover proof_state 1) proverids
- val birthtime = Time.now()
- val deadtime = Time.+ (Time.now(), Time.fromSeconds (! timeout))
- val _ = List.app (register birthtime deadtime) threads_names
- (*maximum number of atps must not exceed*)
- val _ = kill_oldest (! state)
- in () end
+fun prover_desc state subgoal name =
+ let val (ctxt, (chain_ths, goal)) = Proof.get_goal state
+ in "External prover " ^ quote name ^ " for Subgoal " ^ Int.toString subgoal^ ":\n" ^ Syntax.string_of_term ctxt (List.nth(prems_of goal, subgoal-1)) end
+
+fun run_prover state subgoal name =
+ (case Symtab.lookup (Provers.get (Proof.theory_of state)) name of
+ NONE => (warning ("Unknown external prover: " ^ quote name); NONE)
+ | SOME (prover_fn, _) => SOME (prover_fn subgoal state, prover_desc state subgoal name));
- (* concrete syntax *)
+(* kill excessive atp threads *)
- local structure K = OuterKeyword and P = OuterParse in
+local
- val _ =
- OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill_all));
+fun excessive_atps active =
+ let val max = ! maximum_atps
+ in length active > max andalso max > ~1 end;
- val _ =
- OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (priority o info)));
-
- val _ =
- OuterSyntax.improper_command "print_atps" "print external provers" K.diag
- (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
- Toplevel.keep (print_provers o Toplevel.theory_of)));
-
- val _ =
- OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
- (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
- Toplevel.keep ((sledgehammer names) o Toplevel.proof_of)));
-
+fun kill_oldest () =
+ let exception Unchanged in
+ Synchronized.change_result state (fn State {timeout_heap, oldest_heap, active, cancelling} =>
+ if ThreadHeap.is_empty oldest_heap orelse not (excessive_atps active)
+ then raise Unchanged
+ else
+ let val ((_, oldest_thread), oldest_heap') = ThreadHeap.min_elem oldest_heap
+ in (oldest_thread, make_state timeout_heap oldest_heap' active cancelling) end)
+ |> (priority o unregister false "Interrupted (Maximum number of ATPs exceeded).")
+ handle Unchanged => ()
end;
+in
+
+fun kill_excessive () =
+ let val State {active, ...} = Synchronized.value state
+ in if excessive_atps active then (kill_oldest (); kill_excessive ()) else () end;
+
end;
+
+
+(* sledghammer for first subgoal *)
+
+fun sledgehammer names proof_state =
+ let
+ val proverids =
+ if null names then String.tokens (Symbol.is_ascii_blank o String.str) (! atps)
+ else names
+ val threads_names = map_filter (run_prover proof_state 1) proverids
+ val birthtime = Time.now ()
+ val deadtime = Time.+ (Time.now (), Time.fromSeconds (! timeout))
+ val _ = List.app (register birthtime deadtime) threads_names
+ val _ = kill_excessive ()
+ in () end
+
+
+(* concrete syntax *)
+
+local structure K = OuterKeyword and P = OuterParse in
+
+val _ =
+ OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill_all));
+
+val _ =
+ OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
+
+val _ =
+ OuterSyntax.improper_command "print_atps" "print external provers" K.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
+ Toplevel.keep (print_provers o Toplevel.theory_of)));
+
+val _ =
+ OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
+ (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
+ Toplevel.keep ((sledgehammer names) o Toplevel.proof_of)));
+
+end;
+
+end;