--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Apr 23 15:48:34 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Apr 23 16:15:35 2010 +0200
@@ -49,9 +49,6 @@
type prover =
params -> minimize_command -> Time.time -> problem -> prover_result
- val atps: string Unsynchronized.ref
- val timeout: int Unsynchronized.ref
- val full_types: bool Unsynchronized.ref
val kill_atps: unit -> unit
val running_atps: unit -> unit
val messages: int option -> unit
@@ -121,26 +118,6 @@
val message_store_limit = 20;
val message_display_limit = 5;
-val atps = Unsynchronized.ref ""; (* set in "ATP_Wrapper" *)
-val timeout = Unsynchronized.ref 60;
-val full_types = Unsynchronized.ref false;
-
-val _ =
- ProofGeneralPgip.add_preference Preferences.category_proof
- (Preferences.string_pref atps
- "ATP: provers" "Default automatic provers (separated by whitespace)");
-
-val _ =
- ProofGeneralPgip.add_preference Preferences.category_proof
- (Preferences.int_pref timeout
- "ATP: timeout" "ATPs will be interrupted after this time (in seconds)");
-
-val _ =
- ProofGeneralPgip.add_preference Preferences.category_proof
- (Preferences.bool_pref full_types
- "ATP: full types" "ATPs will use full type information");
-
-
(** thread management **)
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Apr 23 15:48:34 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Apr 23 16:15:35 2010 +0200
@@ -1,5 +1,6 @@
(* Title: HOL/Tools/ATP_Manager/atp_wrapper.ML
Author: Fabian Immler, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
Wrapper functions for external ATPs.
*)
@@ -14,6 +15,7 @@
val measure_runtime : bool Config.T
val refresh_systems_on_tptp : unit -> unit
+ val default_atps_param_value : unit -> string
val setup : theory -> theory
end;
@@ -389,6 +391,13 @@
tptp_prover (remotify (fst spass))
(remote_prover_config "SPASS---" "-x" spass_config)
+fun maybe_remote (name, _) ({home, ...} : prover_config) =
+ name |> home = "" ? remotify
+
+fun default_atps_param_value () =
+ space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
+ remotify (fst vampire)]
+
val provers =
[spass, spass_tptp, vampire, e, remote_vampire, remote_spass, remote_e]
val prover_setup = fold add_prover provers
@@ -397,11 +406,6 @@
destdir_setup
#> problem_prefix_setup
#> measure_runtime_setup
- #> prover_setup;
+ #> prover_setup
-fun maybe_remote (name, _) ({home, ...} : prover_config) =
- name |> home = "" ? remotify
-
-val _ = atps := ([maybe_remote e e_config, maybe_remote spass spass_config,
- remotify (fst vampire)] |> space_implode " ")
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 23 15:48:34 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 23 16:15:35 2010 +0200
@@ -8,6 +8,9 @@
sig
type params = ATP_Manager.params
+ val atps: string Unsynchronized.ref
+ val timeout: int Unsynchronized.ref
+ val full_types: bool Unsynchronized.ref
val default_params : theory -> (string * string) list -> params
end;
@@ -35,6 +38,29 @@
fun merge_relevance_overrides rs =
fold merge_relevance_override_pairwise rs (only_relevance_override [])
+(*** parameters ***)
+
+val atps = Unsynchronized.ref (default_atps_param_value ())
+val timeout = Unsynchronized.ref 60
+val full_types = Unsynchronized.ref false
+
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_proof
+ (Preferences.string_pref atps
+ "Sledgehammer: ATPs"
+ "Default automatic provers (separated by whitespace)")
+
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_proof
+ (Preferences.int_pref timeout
+ "Sledgehammer: Time limit"
+ "ATPs will be interrupted after this time (in seconds)")
+
+val _ =
+ ProofGeneralPgip.add_preference Preferences.category_proof
+ (Preferences.bool_pref full_types
+ "Sledgehammer: Full types" "ATPs will use full type information")
+
type raw_param = string * string list
val default_default_params =