src/HOL/Tools/ATP_Manager/atp_manager.ML
author wenzelm
Thu, 15 Oct 2009 10:59:10 +0200
changeset 32938 63a364ed3f8d
parent 32937 34f66c9dd8a2
child 32939 1b5a401c78cb
permissions -rw-r--r--
misc tuning and clarification;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32327
0971cc0b6a57 src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
wenzelm
parents: 31793
diff changeset
     1
(*  Title:      HOL/Tools/ATP_Manager/atp_manager.ML
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
     2
    Author:     Fabian Immler, TU Muenchen
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
     3
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
     4
ATP threads are registered here.
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
     5
Threads with the same birth-time are seen as one group.
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
     6
All threads of a group are killed when one thread of it has been successful,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
     7
or after a certain time,
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
     8
or when the maximum number of threads exceeds; then the oldest thread is killed.
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
     9
*)
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
signature ATP_MANAGER =
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    12
sig
32937
34f66c9dd8a2 structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32936
diff changeset
    13
  val atps: string Unsynchronized.ref
34f66c9dd8a2 structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32936
diff changeset
    14
  val get_atps: unit -> string list
34f66c9dd8a2 structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32936
diff changeset
    15
  val max_atps: int Unsynchronized.ref
34f66c9dd8a2 structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32936
diff changeset
    16
  val timeout: int Unsynchronized.ref
34f66c9dd8a2 structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32936
diff changeset
    17
  val full_types: bool Unsynchronized.ref
28586
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
    18
  val kill: unit -> unit
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
    19
  val info: unit -> unit
29112
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
    20
  val messages: int option -> unit
32936
9491bec20595 modernized structure names;
wenzelm
parents: 32865
diff changeset
    21
  val add_prover: string * ATP_Wrapper.prover -> theory -> theory
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
    22
  val print_provers: theory -> unit
32936
9491bec20595 modernized structure names;
wenzelm
parents: 32865
diff changeset
    23
  val get_prover: string -> theory -> ATP_Wrapper.prover option
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
    24
  val sledgehammer: string list -> Proof.state -> unit
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    25
end;
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    26
32936
9491bec20595 modernized structure names;
wenzelm
parents: 32865
diff changeset
    27
structure ATP_Manager: ATP_MANAGER =
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    28
struct
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    29
28586
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
    30
(** preferences **)
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
    31
29112
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
    32
val message_store_limit = 20;
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
    33
val message_display_limit = 5;
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
    34
32937
34f66c9dd8a2 structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32936
diff changeset
    35
val atps = Unsynchronized.ref "e spass remote_vampire";
34f66c9dd8a2 structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32936
diff changeset
    36
fun get_atps () = String.tokens (Symbol.is_ascii_blank o String.str) (! atps);
28586
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
    37
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
    38
val max_atps = Unsynchronized.ref 5;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
    39
fun excessive_atps active =
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
    40
  let val max = ! max_atps
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
    41
  in max >= 0 andalso length active > max end;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
    42
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32510
diff changeset
    43
val timeout = Unsynchronized.ref 60;
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32510
diff changeset
    44
val full_types = Unsynchronized.ref false;
28586
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
    45
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
    46
val _ =
30982
7882a1268a48 use predefined preferences categories;
wenzelm
parents: 30830
diff changeset
    47
  ProofGeneralPgip.add_preference Preferences.category_proof
28586
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
    48
    (Preferences.string_pref atps
28589
581b2ab9827a adding preferences is now permissive, no error handling here;
wenzelm
parents: 28586
diff changeset
    49
      "ATP: provers" "Default automatic provers (separated by whitespace)");
28586
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
    50
30982
7882a1268a48 use predefined preferences categories;
wenzelm
parents: 30830
diff changeset
    51
val _ =
7882a1268a48 use predefined preferences categories;
wenzelm
parents: 30830
diff changeset
    52
  ProofGeneralPgip.add_preference Preferences.category_proof
28586
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
    53
    (Preferences.int_pref max_atps
28589
581b2ab9827a adding preferences is now permissive, no error handling here;
wenzelm
parents: 28586
diff changeset
    54
      "ATP: maximum number" "How many provers may run in parallel");
28586
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
    55
30982
7882a1268a48 use predefined preferences categories;
wenzelm
parents: 30830
diff changeset
    56
val _ =
7882a1268a48 use predefined preferences categories;
wenzelm
parents: 30830
diff changeset
    57
  ProofGeneralPgip.add_preference Preferences.category_proof
28586
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
    58
    (Preferences.int_pref timeout
28589
581b2ab9827a adding preferences is now permissive, no error handling here;
wenzelm
parents: 28586
diff changeset
    59
      "ATP: timeout" "ATPs will be interrupted after this time (in seconds)");
28586
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
    60
31791
c9a1caf218c8 New ATP option: full types
nipkow
parents: 31752
diff changeset
    61
val _ =
c9a1caf218c8 New ATP option: full types
nipkow
parents: 31752
diff changeset
    62
  ProofGeneralPgip.add_preference Preferences.category_proof
c9a1caf218c8 New ATP option: full types
nipkow
parents: 31752
diff changeset
    63
    (Preferences.bool_pref full_types
c9a1caf218c8 New ATP option: full types
nipkow
parents: 31752
diff changeset
    64
      "ATP: full types" "ATPs will use full type information");
c9a1caf218c8 New ATP option: full types
nipkow
parents: 31752
diff changeset
    65
28586
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
    66
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
    67
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
    68
(** thread management **)
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
    69
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
    70
(* data structures over threads *)
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
    71
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
    72
structure Thread_Heap = HeapFun
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
    73
(
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
    74
  type elem = Time.time * Thread.thread;
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
    75
  fun ord ((a, _), (b, _)) = Time.compare (a, b);
28595
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
    76
);
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
    77
31368
763f4b0fd579 made SML/NJ happy;
wenzelm
parents: 31037
diff changeset
    78
fun lookup_thread xs = AList.lookup Thread.equal xs;
763f4b0fd579 made SML/NJ happy;
wenzelm
parents: 31037
diff changeset
    79
fun update_thread xs = AList.update Thread.equal xs;
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
    80
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
    81
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
    82
(* state of thread manager *)
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
    83
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
    84
type state =
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
    85
 {manager: Thread.thread option,
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
    86
  timeout_heap: Thread_Heap.T,
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
    87
  oldest_heap: Thread_Heap.T,
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
    88
  active: (Thread.thread * (Time.time * Time.time * string)) list,
29112
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
    89
  cancelling: (Thread.thread * (Time.time * Time.time * string)) list,
29620
dc1257eaa4f2 moved all output to watcher-thread
immler@in.tum.de
parents: 29598
diff changeset
    90
  messages: string list,
dc1257eaa4f2 moved all output to watcher-thread
immler@in.tum.de
parents: 29598
diff changeset
    91
  store: string list};
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
    92
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
    93
fun make_state manager timeout_heap oldest_heap active cancelling messages store =
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
    94
  {manager = manager, timeout_heap = timeout_heap, oldest_heap = oldest_heap,
29620
dc1257eaa4f2 moved all output to watcher-thread
immler@in.tum.de
parents: 29598
diff changeset
    95
    active = active, cancelling = cancelling, messages = messages, store = store};
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
    96
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
    97
val global_state = Synchronized.var "atp_manager"
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
    98
  (make_state NONE Thread_Heap.empty Thread_Heap.empty [] [] [] []);
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
    99
31368
763f4b0fd579 made SML/NJ happy;
wenzelm
parents: 31037
diff changeset
   100
29150
8af5ee47f30c unregister: refrain from cancelling self, which sometimes caused sledghammer to fail just before printing the result;
wenzelm
parents: 29116
diff changeset
   101
(* unregister thread *)
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   102
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   103
fun unregister (success, message) thread = Synchronized.change global_state
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   104
  (fn state as {manager, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
29150
8af5ee47f30c unregister: refrain from cancelling self, which sometimes caused sledghammer to fail just before printing the result;
wenzelm
parents: 29116
diff changeset
   105
    (case lookup_thread active thread of
8af5ee47f30c unregister: refrain from cancelling self, which sometimes caused sledghammer to fail just before printing the result;
wenzelm
parents: 29116
diff changeset
   106
      SOME (birthtime, _, description) =>
8af5ee47f30c unregister: refrain from cancelling self, which sometimes caused sledghammer to fail just before printing the result;
wenzelm
parents: 29116
diff changeset
   107
        let
8af5ee47f30c unregister: refrain from cancelling self, which sometimes caused sledghammer to fail just before printing the result;
wenzelm
parents: 29116
diff changeset
   108
          val (group, active') =
8af5ee47f30c unregister: refrain from cancelling self, which sometimes caused sledghammer to fail just before printing the result;
wenzelm
parents: 29116
diff changeset
   109
            if success then List.partition (fn (_, (tb, _, _)) => tb = birthtime) active
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   110
            else List.partition (fn (th, _) => Thread.equal (th, thread)) active;
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   111
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   112
          val now = Time.now ();
29150
8af5ee47f30c unregister: refrain from cancelling self, which sometimes caused sledghammer to fail just before printing the result;
wenzelm
parents: 29116
diff changeset
   113
          val cancelling' =
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   114
            fold (fn (th, (tb, _, desc)) => update_thread (th, (tb, now, desc))) group cancelling;
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   115
29620
dc1257eaa4f2 moved all output to watcher-thread
immler@in.tum.de
parents: 29598
diff changeset
   116
          val message' = description ^ "\n" ^ message ^
29596
7b710756609c do not interrupt successful thread
immler@in.tum.de
parents: 29595
diff changeset
   117
            (if length group <= 1 then ""
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   118
             else "\nInterrupted " ^ string_of_int (length group - 1) ^ " other group members");
29620
dc1257eaa4f2 moved all output to watcher-thread
immler@in.tum.de
parents: 29598
diff changeset
   119
          val store' = message' ::
dc1257eaa4f2 moved all output to watcher-thread
immler@in.tum.de
parents: 29598
diff changeset
   120
            (if length store <= message_store_limit then store
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   121
             else #1 (chop message_store_limit store));
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   122
        in
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   123
          make_state manager timeout_heap oldest_heap
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   124
            active' cancelling' (message' :: messages) store'
30830
263064c4d0c3 included managing_thread in state of AtpManager:
immler@in.tum.de
parents: 30800
diff changeset
   125
        end
30800
95cbadcd47fc tuned spacing and formatting;
wenzelm
parents: 30798
diff changeset
   126
    | NONE => state));
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   127
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   128
28595
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   129
(* kill excessive atp threads *)
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   130
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   131
local
28595
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   132
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   133
exception UNCHANGED of unit;
28595
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   134
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   135
fun kill_oldest () =
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   136
  Synchronized.change_result global_state
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   137
    (fn {manager, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   138
      if Thread_Heap.is_empty oldest_heap orelse not (excessive_atps active)
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   139
      then raise UNCHANGED ()
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   140
      else
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   141
        let
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   142
          val ((_, oldest_thread), oldest_heap') = Thread_Heap.min_elem oldest_heap;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   143
          val state' =
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   144
            make_state manager timeout_heap oldest_heap' active cancelling messages store;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   145
        in (oldest_thread, state') end)
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   146
    |> unregister (false, "Interrupted (maximum number of ATPs exceeded)")
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   147
  handle UNCHANGED () => ();
28595
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   148
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   149
in
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   150
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   151
fun kill_excessive () =
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   152
  let val {active, ...} = Synchronized.value global_state
28595
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   153
  in if excessive_atps active then (kill_oldest (); kill_excessive ()) else () end;
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   154
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   155
end;
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   156
29620
dc1257eaa4f2 moved all output to watcher-thread
immler@in.tum.de
parents: 29598
diff changeset
   157
fun print_new_messages () =
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   158
  let val msgs = Synchronized.change_result global_state
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   159
    (fn {manager, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   160
      (messages, make_state manager timeout_heap oldest_heap active cancelling [] store))
30800
95cbadcd47fc tuned spacing and formatting;
wenzelm
parents: 30798
diff changeset
   161
  in
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   162
    if null msgs then ()
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   163
    else priority ("Sledgehammer: " ^ space_implode "\n\n" msgs)
30800
95cbadcd47fc tuned spacing and formatting;
wenzelm
parents: 30798
diff changeset
   164
  end;
29620
dc1257eaa4f2 moved all output to watcher-thread
immler@in.tum.de
parents: 29598
diff changeset
   165
28595
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   166
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   167
(* start manager thread -- only one may exist *)
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   168
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   169
val min_wait_time = Time.fromMilliseconds 300;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   170
val max_wait_time = Time.fromSeconds 10;
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   171
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   172
fun check_thread_manager () = Synchronized.change global_state
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   173
  (fn {manager, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   174
    if (case manager of SOME thread => Thread.isActive thread | NONE => false)
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   175
    then make_state manager timeout_heap oldest_heap active cancelling messages store
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   176
    else let val manager = SOME (SimpleThread.fork false (fn () =>
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   177
      let
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   178
        fun time_limit timeout_heap =
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   179
          (case try Thread_Heap.min timeout_heap of
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   180
            NONE => Time.+ (Time.now (), max_wait_time)
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   181
          | SOME (time, _) => time);
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   182
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   183
        (*action: find threads whose timeout is reached, and interrupt cancelling threads*)
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   184
        fun action {manager, timeout_heap, oldest_heap, active, cancelling, messages, store} =
30830
263064c4d0c3 included managing_thread in state of AtpManager:
immler@in.tum.de
parents: 30800
diff changeset
   185
          let val (timeout_threads, timeout_heap') =
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   186
            Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
30830
263064c4d0c3 included managing_thread in state of AtpManager:
immler@in.tum.de
parents: 30800
diff changeset
   187
          in
263064c4d0c3 included managing_thread in state of AtpManager:
immler@in.tum.de
parents: 30800
diff changeset
   188
            if null timeout_threads andalso null cancelling andalso not (excessive_atps active)
263064c4d0c3 included managing_thread in state of AtpManager:
immler@in.tum.de
parents: 30800
diff changeset
   189
            then NONE
263064c4d0c3 included managing_thread in state of AtpManager:
immler@in.tum.de
parents: 30800
diff changeset
   190
            else
263064c4d0c3 included managing_thread in state of AtpManager:
immler@in.tum.de
parents: 30800
diff changeset
   191
              let
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   192
                val _ = List.app (SimpleThread.interrupt o #1) cancelling;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   193
                val cancelling' = filter (Thread.isActive o #1) cancelling;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   194
                val state' =
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   195
                  make_state manager timeout_heap' oldest_heap active cancelling' messages store;
30830
263064c4d0c3 included managing_thread in state of AtpManager:
immler@in.tum.de
parents: 30800
diff changeset
   196
              in SOME (map #2 timeout_threads, state') end
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   197
          end;
30830
263064c4d0c3 included managing_thread in state of AtpManager:
immler@in.tum.de
parents: 30800
diff changeset
   198
      in
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   199
        while Synchronized.change_result global_state
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   200
          (fn state as {timeout_heap, oldest_heap, active, cancelling, messages, store, ...} =>
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   201
            if null active andalso null cancelling andalso null messages
30830
263064c4d0c3 included managing_thread in state of AtpManager:
immler@in.tum.de
parents: 30800
diff changeset
   202
            then (false, make_state NONE timeout_heap oldest_heap active cancelling messages store)
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   203
            else (true, state))
30830
263064c4d0c3 included managing_thread in state of AtpManager:
immler@in.tum.de
parents: 30800
diff changeset
   204
        do
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   205
          (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
30830
263064c4d0c3 included managing_thread in state of AtpManager:
immler@in.tum.de
parents: 30800
diff changeset
   206
            |> these
263064c4d0c3 included managing_thread in state of AtpManager:
immler@in.tum.de
parents: 30800
diff changeset
   207
            |> List.app (unregister (false, "Interrupted (reached timeout)"));
263064c4d0c3 included managing_thread in state of AtpManager:
immler@in.tum.de
parents: 30800
diff changeset
   208
            kill_excessive ();
263064c4d0c3 included managing_thread in state of AtpManager:
immler@in.tum.de
parents: 30800
diff changeset
   209
            print_new_messages ();
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   210
            (*give threads some time to respond to interrupt*)
30830
263064c4d0c3 included managing_thread in state of AtpManager:
immler@in.tum.de
parents: 30800
diff changeset
   211
            OS.Process.sleep min_wait_time)
263064c4d0c3 included managing_thread in state of AtpManager:
immler@in.tum.de
parents: 30800
diff changeset
   212
      end))
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   213
    in make_state manager timeout_heap oldest_heap active cancelling messages store end);
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   214
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   215
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   216
(* thread is registered here by sledgehammer *)
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   217
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   218
fun register birthtime deadtime (thread, desc) =
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   219
 (Synchronized.change global_state
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   220
    (fn {manager, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
29112
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
   221
      let
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   222
        val timeout_heap' = Thread_Heap.insert (deadtime, thread) timeout_heap;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   223
        val oldest_heap' = Thread_Heap.insert (birthtime, thread) oldest_heap;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   224
        val active' = update_thread (thread, (birthtime, deadtime, desc)) active;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   225
        val state' =
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   226
          make_state manager timeout_heap' oldest_heap' active' cancelling messages store;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   227
      in state' end);
30798
36b41d297d65 terminate watching thread
immler@in.tum.de
parents: 30537
diff changeset
   228
  check_thread_manager ());
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   229
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   230
28586
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
   231
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
   232
(** user commands **)
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   233
28586
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
   234
(* kill: move all threads to cancelling *)
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
   235
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   236
fun kill () = Synchronized.change global_state
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   237
  (fn {manager, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   238
    let
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   239
      val formerly_active = map (fn (th, (tb, _, desc)) => (th, (tb, Time.now (), desc))) active;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   240
      val state' =
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   241
        make_state manager timeout_heap oldest_heap [] (formerly_active @ cancelling) messages store;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   242
    in state' end);
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   243
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   244
29112
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
   245
(* ATP info *)
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   246
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   247
fun seconds time = string_of_int (Time.toSeconds time) ^ "s";
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   248
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   249
fun info () =
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   250
  let
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   251
    val {active, cancelling, ...} = Synchronized.value global_state;
29112
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
   252
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   253
    val now = Time.now ();
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   254
    fun running_info (_, (birth_time, dead_time, desc)) =
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   255
      "Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   256
        seconds (Time.- (dead_time, now)) ^ " to live:\n" ^ desc;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   257
    fun cancelling_info (_, (_, dead_time, desc)) =
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   258
      "Trying to interrupt thread since " ^ seconds (Time.- (now, dead_time)) ^ ":\n" ^ desc;
29112
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
   259
28589
581b2ab9827a adding preferences is now permissive, no error handling here;
wenzelm
parents: 28586
diff changeset
   260
    val running =
581b2ab9827a adding preferences is now permissive, no error handling here;
wenzelm
parents: 28586
diff changeset
   261
      if null active then "No ATPs running."
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   262
      else space_implode "\n\n" ("Running ATPs:" :: map running_info active);
28589
581b2ab9827a adding preferences is now permissive, no error handling here;
wenzelm
parents: 28586
diff changeset
   263
    val interrupting =
581b2ab9827a adding preferences is now permissive, no error handling here;
wenzelm
parents: 28586
diff changeset
   264
      if null cancelling then ""
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   265
      else
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   266
        space_implode "\n\n"
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   267
          ("Trying to interrupt the following ATPs:" :: map cancelling_info cancelling);
29112
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
   268
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   269
  in writeln (running ^ "\n" ^ interrupting) end;
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   270
29112
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
   271
fun messages opt_limit =
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
   272
  let
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
   273
    val limit = the_default message_display_limit opt_limit;
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   274
    val {store, ...} = Synchronized.value global_state;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   275
    val header =
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   276
      "Recent ATP messages" ^
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   277
        (if length store <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):");
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   278
  in writeln (space_implode "\n\n" (header :: #1 (chop limit store))) end;
29112
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
   279
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   280
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   281
28586
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
   282
(** The Sledgehammer **)
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   283
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   284
(* named provers *)
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   285
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   286
fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
diff changeset
   287
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   288
structure Provers = TheoryDataFun
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   289
(
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   290
  type T = (ATP_Wrapper.prover * stamp) Symtab.table;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   291
  val empty = Symtab.empty;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   292
  val copy = I;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   293
  val extend = I;
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   294
  fun merge _ tabs : T = Symtab.merge (eq_snd op =) tabs
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   295
    handle Symtab.DUP dup => err_dup_prover dup;
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   296
);
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   297
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32824
diff changeset
   298
fun add_prover (name, prover) thy =
28595
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   299
  Provers.map (Symtab.update_new (name, (prover, stamp ()))) thy
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   300
    handle Symtab.DUP dup => err_dup_prover dup;
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   301
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   302
fun print_provers thy = Pretty.writeln
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   303
  (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
28571
47d88239658d ** Update from Fabian **
wenzelm
parents: 28543
diff changeset
   304
32863
5e8cef567042 eliminated dead code;
wenzelm
parents: 32824
diff changeset
   305
fun get_prover name thy =
5e8cef567042 eliminated dead code;
wenzelm
parents: 32824
diff changeset
   306
  (case Symtab.lookup (Provers.get thy) name of
5e8cef567042 eliminated dead code;
wenzelm
parents: 32824
diff changeset
   307
    NONE => NONE
5e8cef567042 eliminated dead code;
wenzelm
parents: 32824
diff changeset
   308
  | SOME (prover, _) => SOME prover);
5e8cef567042 eliminated dead code;
wenzelm
parents: 32824
diff changeset
   309
28586
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
   310
28595
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   311
(* start prover thread *)
28484
4ed9239b09c1 misc simplifcation and tuning;
wenzelm
parents: 28478
diff changeset
   312
28595
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   313
fun start_prover name birthtime deadtime i proof_state =
31037
ac8669134e7a added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents: 30982
diff changeset
   314
  (case get_prover name (Proof.theory_of proof_state) of
28595
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   315
    NONE => warning ("Unknown external prover: " ^ quote name)
31037
ac8669134e7a added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents: 30982
diff changeset
   316
  | SOME prover =>
28595
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   317
      let
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   318
        val (ctxt, (_, goal)) = Proof.get_goal proof_state;
28595
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   319
        val desc =
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   320
          "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   321
            Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
28595
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   322
        val _ = SimpleThread.fork true (fn () =>
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   323
          let
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   324
            val _ = register birthtime deadtime (Thread.self (), desc);
32937
34f66c9dd8a2 structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32936
diff changeset
   325
            val problem =
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   326
              ATP_Wrapper.atp_problem_of_goal (! full_types) i (Proof.get_goal proof_state);
31037
ac8669134e7a added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents: 30982
diff changeset
   327
            val result =
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   328
              let val ATP_Wrapper.Prover_Result {success, message, ...} = prover problem (! timeout);
31037
ac8669134e7a added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents: 30982
diff changeset
   329
              in (success, message) end
32937
34f66c9dd8a2 structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32936
diff changeset
   330
              handle ResHolClause.TOO_TRIVIAL =>   (* FIXME !? *)
34f66c9dd8a2 structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32936
diff changeset
   331
                  (true, "Empty clause: Try this command: " ^
34f66c9dd8a2 structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
wenzelm
parents: 32936
diff changeset
   332
                    Markup.markup Markup.sendback "apply metis")
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   333
                | ERROR msg => (false, "Error: " ^ msg);
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   334
            val _ = unregister result (Thread.self ());
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   335
          in () end handle Exn.Interrupt => ())
28595
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   336
      in () end);
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   337
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   338
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   339
(* sledghammer for first subgoal *)
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   340
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   341
fun sledgehammer names proof_state =
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   342
  let
32938
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   343
    val provers = if null names then get_atps () else names;
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   344
    val birthtime = Time.now ();
63a364ed3f8d misc tuning and clarification;
wenzelm
parents: 32937
diff changeset
   345
    val deadtime = Time.+ (birthtime, Time.fromSeconds (! timeout));
28595
67e3945b53f1 add_prover: plain prover function, without thread;
wenzelm
parents: 28589
diff changeset
   346
  in List.app (fn name => start_prover name birthtime deadtime 1 proof_state) provers end;
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   347
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   348
28586
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
   349
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
   350
(** Isar command syntax **)
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   351
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   352
local structure K = OuterKeyword and P = OuterParse in
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   353
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   354
val _ =
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   355
  OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
28586
d238b83ba3fc renamed kill_all to kill, in conformance with atp_kill command;
wenzelm
parents: 28582
diff changeset
   356
    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   357
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   358
val _ =
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   359
  OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   360
    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   361
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   362
val _ =
29112
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
   363
  OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
   364
    (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
   365
      (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
   366
f2b45eea6dac added 'atp_messages' command, which displays recent messages synchronously;
wenzelm
parents: 28835
diff changeset
   367
val _ =
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   368
  OuterSyntax.improper_command "print_atps" "print external provers" K.diag
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   369
    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   370
      Toplevel.keep (print_provers o Toplevel.theory_of)));
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   371
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   372
val _ =
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   373
  OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   374
    (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
30800
95cbadcd47fc tuned spacing and formatting;
wenzelm
parents: 30798
diff changeset
   375
      Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
28582
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   376
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   377
end;
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   378
c269a3045fdf info: back to plain printing;
wenzelm
parents: 28571
diff changeset
   379
end;
30537
0dd8dfe424cf use goal instead of Proof State
immler@in.tum.de
parents: 29784
diff changeset
   380