equal
deleted
inserted
replaced
11 type mode = Sledgehammer_Prover.mode |
11 type mode = Sledgehammer_Prover.mode |
12 type prover = Sledgehammer_Prover.prover |
12 type prover = Sledgehammer_Prover.prover |
13 |
13 |
14 val atp_dest_dir : string Config.T |
14 val atp_dest_dir : string Config.T |
15 val atp_problem_prefix : string Config.T |
15 val atp_problem_prefix : string Config.T |
16 val atp_completish : bool Config.T |
16 val atp_completish : int Config.T |
17 val atp_full_names : bool Config.T |
17 val atp_full_names : bool Config.T |
18 |
18 |
19 val is_ho_atp : Proof.context -> string -> bool |
19 val is_ho_atp : Proof.context -> string -> bool |
20 |
20 |
21 val run_atp : mode -> string -> prover |
21 val run_atp : mode -> string -> prover |
39 |
39 |
40 (* Empty string means create files in Isabelle's temporary files directory. *) |
40 (* Empty string means create files in Isabelle's temporary files directory. *) |
41 val atp_dest_dir = Attrib.setup_config_string @{binding sledgehammer_atp_dest_dir} (K "") |
41 val atp_dest_dir = Attrib.setup_config_string @{binding sledgehammer_atp_dest_dir} (K "") |
42 val atp_problem_prefix = |
42 val atp_problem_prefix = |
43 Attrib.setup_config_string @{binding sledgehammer_atp_problem_prefix} (K "prob") |
43 Attrib.setup_config_string @{binding sledgehammer_atp_problem_prefix} (K "prob") |
44 val atp_completish = Attrib.setup_config_bool @{binding sledgehammer_atp_completish} (K false) |
44 val atp_completish = Attrib.setup_config_int @{binding sledgehammer_atp_completish} (K 0) |
45 (* In addition to being easier to read, readable names are often much shorter, especially if types |
45 (* In addition to being easier to read, readable names are often much shorter, especially if types |
46 are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short |
46 are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short |
47 names are enabled by default. *) |
47 names are enabled by default. *) |
48 val atp_full_names = Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false) |
48 val atp_full_names = Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false) |
49 |
49 |
144 val full_proofs = isar_proofs |> the_default (mode = Minimize) |
144 val full_proofs = isar_proofs |> the_default (mode = Minimize) |
145 val local_name = perhaps (try (unprefix remote_prefix)) name |
145 val local_name = perhaps (try (unprefix remote_prefix)) name |
146 val waldmeister_new = (local_name = waldmeister_newN) |
146 val waldmeister_new = (local_name = waldmeister_newN) |
147 val spassy = (local_name = pirateN orelse local_name = spassN) |
147 val spassy = (local_name = pirateN orelse local_name = spassN) |
148 |
148 |
149 val atp_mode = if Config.get ctxt atp_completish then Sledgehammer_Completish else Sledgehammer |
149 val completish = Config.get ctxt atp_completish |
|
150 val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer |
150 val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt |
151 val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt |
151 val (dest_dir, problem_prefix) = |
152 val (dest_dir, problem_prefix) = |
152 if overlord then overlord_file_location_of_prover name |
153 if overlord then overlord_file_location_of_prover name |
153 else (Config.get ctxt atp_dest_dir, Config.get ctxt atp_problem_prefix) |
154 else (Config.get ctxt atp_dest_dir, Config.get ctxt atp_problem_prefix) |
154 val problem_file_name = |
155 val problem_file_name = |