# HG changeset patch # User blanchet # Date 1272032135 -7200 # Node ID 8c83ea1a7740b6d98f9a5dfbbf5379b015a3f3e1 # Parent a4f601daa17516e8b373e6d0471c46233349508a move the Sledgehammer menu options to "sledgehammer_isar.ML" diff -r a4f601daa175 -r 8c83ea1a7740 src/HOL/Tools/ATP_Manager/atp_manager.ML --- 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 **) diff -r a4f601daa175 -r 8c83ea1a7740 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- 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; diff -r a4f601daa175 -r 8c83ea1a7740 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 =