equal
deleted
inserted
replaced
141 val ctxt = Proof.context_of state |
141 val ctxt = Proof.context_of state |
142 |
142 |
143 val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters, |
143 val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters, |
144 best_max_new_mono_instances, ...} = get_atp thy name () |
144 best_max_new_mono_instances, ...} = get_atp thy name () |
145 |
145 |
|
146 val full_proofs = isar_proofs |> the_default (mode = Minimize) |
146 val local_name = perhaps (try (unprefix remote_prefix)) name |
147 val local_name = perhaps (try (unprefix remote_prefix)) name |
147 val waldmeister_new = (local_name = waldmeister_newN) |
148 val waldmeister_new = (local_name = waldmeister_newN) |
148 val spass = (local_name = spassN orelse local_name = spass_pirateN) |
149 val spass = (local_name = spassN orelse local_name = spass_pirateN) |
149 |
150 |
150 val atp_mode = if Config.get ctxt atp_completish then Sledgehammer_Completish else Sledgehammer |
151 val atp_mode = if Config.get ctxt atp_completish then Sledgehammer_Completish else Sledgehammer |
160 File.tmp_path problem_file_name |
161 File.tmp_path problem_file_name |
161 else if File.exists (Path.explode dest_dir) then |
162 else if File.exists (Path.explode dest_dir) then |
162 Path.append (Path.explode dest_dir) problem_file_name |
163 Path.append (Path.explode dest_dir) problem_file_name |
163 else |
164 else |
164 error ("No such directory: " ^ quote dest_dir ^ ".") |
165 error ("No such directory: " ^ quote dest_dir ^ ".") |
165 val exec = exec () |
166 val exec = exec full_proofs |
166 val command0 = |
167 val command0 = |
167 (case find_first (fn var => getenv var <> "") (fst exec) of |
168 (case find_first (fn var => getenv var <> "") (fst exec) of |
168 SOME var => |
169 SOME var => |
169 let |
170 let |
170 val pref = getenv var ^ "/" |
171 val pref = getenv var ^ "/" |
274 |
275 |
275 fun sel_weights () = atp_problem_selection_weights atp_problem |
276 fun sel_weights () = atp_problem_selection_weights atp_problem |
276 fun ord_info () = atp_problem_term_order_info atp_problem |
277 fun ord_info () = atp_problem_term_order_info atp_problem |
277 |
278 |
278 val ord = effective_term_order ctxt name |
279 val ord = effective_term_order ctxt name |
279 val full_proof = isar_proofs |> the_default (mode = Minimize) |
|
280 val args = |
280 val args = |
281 arguments ctxt full_proof extra slice_timeout (File.shell_path prob_path) |
281 arguments ctxt full_proofs extra slice_timeout (File.shell_path prob_path) |
282 (ord, ord_info, sel_weights) |
282 (ord, ord_info, sel_weights) |
283 val command = |
283 val command = |
284 "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")" |
284 "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")" |
285 |> enclose "TIMEFORMAT='%3R'; { time " " ; }" |
285 |> enclose "TIMEFORMAT='%3R'; { time " " ; }" |
286 |
286 |