# HG changeset patch # User blanchet # Date 1297177810 -3600 # Node ID ab3f6d76fb236da90f6f650364fd508f56289ac8 # Parent 1ef01508bb9ba3e536c647aaf2328fcfae00e399 available_provers ~> supported_provers (for clarity) diff -r 1ef01508bb9b -r ab3f6d76fb23 NEWS --- a/NEWS Tue Feb 08 16:10:09 2011 +0100 +++ b/NEWS Tue Feb 08 16:10:10 2011 +0100 @@ -11,6 +11,13 @@ usedir option -Q. +*** HOL *** + +* Sledgehammer: + sledgehammer available_provers ~> sledgehammer supported_provers + INCOMPATIBILITY. + + *** Document preparation *** * New term style "isub" as ad-hoc conversion of variables x1, y23 into diff -r 1ef01508bb9b -r ab3f6d76fb23 doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Tue Feb 08 16:10:09 2011 +0100 +++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Feb 08 16:10:10 2011 +0100 @@ -303,7 +303,7 @@ due to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a limit on the number of messages to display (5 by default). -\item[$\bullet$] \textbf{\textit{available\_provers}:} Prints the list of +\item[$\bullet$] \textbf{\textit{supported\_provers}:} Prints the list of automatic provers supported by Sledgehammer. See \S\ref{installation} and \S\ref{mode-of-operation} for more information on how to install automatic provers. diff -r 1ef01508bb9b -r ab3f6d76fb23 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Feb 08 16:10:09 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Feb 08 16:10:10 2011 +0100 @@ -39,7 +39,7 @@ val remote_prefix : string val add_atp : string * atp_config -> theory -> theory val get_atp : theory -> string -> atp_config - val available_atps : theory -> string list + val supported_atps : theory -> string list val is_atp_installed : theory -> string -> bool val refresh_systems_on_tptp : unit -> unit val setup : theory -> theory @@ -307,7 +307,7 @@ the (Symtab.lookup (Data.get thy) name) |> fst handle Option.Option => error ("Unknown ATP: " ^ name ^ ".") -val available_atps = Symtab.keys o Data.get +val supported_atps = Symtab.keys o Data.get fun is_atp_installed thy name = let val {exec, required_execs, ...} = get_atp thy name in diff -r 1ef01508bb9b -r ab3f6d76fb23 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Feb 08 16:10:09 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Feb 08 16:10:10 2011 +0100 @@ -113,7 +113,7 @@ fun is_prover_list ctxt s = case space_explode " " s of - ss as _ :: _ => forall (is_prover_available ctxt) ss + ss as _ :: _ => forall (is_prover_supported ctxt) ss | _ => false fun check_and_repair_raw_param ctxt (name, value) = @@ -141,23 +141,23 @@ fun merge data : T = AList.merge (op =) (K true) data ) -fun remotify_prover_if_available_and_not_already_remote ctxt name = +fun remotify_prover_if_supported_and_not_already_remote ctxt name = if String.isPrefix remote_prefix name then SOME name else let val remote_name = remote_prefix ^ name in - if is_prover_available ctxt remote_name then SOME remote_name else NONE + if is_prover_supported ctxt remote_name then SOME remote_name else NONE end fun remotify_prover_if_not_installed ctxt name = - if is_prover_available ctxt name andalso is_prover_installed ctxt name then + if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name else - remotify_prover_if_available_and_not_already_remote ctxt name + remotify_prover_if_supported_and_not_already_remote ctxt name fun avoid_too_many_local_threads _ _ [] = [] | avoid_too_many_local_threads ctxt 0 provers = - map_filter (remotify_prover_if_available_and_not_already_remote ctxt) + map_filter (remotify_prover_if_supported_and_not_already_remote ctxt) provers | avoid_too_many_local_threads ctxt n (prover :: provers) = let val n = if String.isPrefix remote_prefix prover then n else n - 1 in @@ -270,7 +270,7 @@ val runN = "run" val minimizeN = "minimize" val messagesN = "messages" -val available_proversN = "available_provers" +val supported_proversN = "supported_provers" val running_proversN = "running_provers" val kill_proversN = "kill_provers" val refresh_tptpN = "refresh_tptp" @@ -305,8 +305,8 @@ (#add relevance_override) state else if subcommand = messagesN then messages opt_i - else if subcommand = available_proversN then - available_provers ctxt + else if subcommand = supported_proversN then + supported_provers ctxt else if subcommand = running_proversN then running_provers () else if subcommand = kill_proversN then diff -r 1ef01508bb9b -r ab3f6d76fb23 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Feb 08 16:10:09 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Feb 08 16:10:10 2011 +0100 @@ -71,7 +71,7 @@ val das_Tool : string val select_smt_solver : string -> Proof.context -> Proof.context val is_smt_prover : Proof.context -> string -> bool - val is_prover_available : Proof.context -> string -> bool + val is_prover_supported : Proof.context -> string -> bool val is_prover_installed : Proof.context -> string -> bool val default_max_relevant_for_prover : Proof.context -> string -> int val is_built_in_const_for_prover : @@ -89,7 +89,7 @@ val smt_weighted_fact : theory -> int -> prover_fact * int -> (string * locality) * (int option * thm) - val available_provers : Proof.context -> unit + val supported_provers : Proof.context -> unit val kill_provers : unit -> unit val running_provers : unit -> unit val messages : int option -> unit @@ -121,16 +121,14 @@ fun is_smt_prover ctxt name = member (op =) (SMT_Solver.available_solvers_of ctxt) name -fun is_prover_available ctxt name = +fun is_prover_supported ctxt name = let val thy = ProofContext.theory_of ctxt in - is_smt_prover ctxt name orelse member (op =) (available_atps thy) name + is_smt_prover ctxt name orelse member (op =) (supported_atps thy) name end fun is_prover_installed ctxt = is_smt_prover ctxt orf is_atp_installed (ProofContext.theory_of ctxt) -fun available_smt_solvers ctxt = SMT_Solver.available_solvers_of ctxt - fun default_max_relevant_for_prover ctxt name = let val thy = ProofContext.theory_of ctxt in if is_smt_prover ctxt name then @@ -205,15 +203,15 @@ fun relevance_fudge_for_prover ctxt name = if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge -fun available_provers ctxt = +fun supported_provers ctxt = let val thy = ProofContext.theory_of ctxt val (remote_provers, local_provers) = - sort_strings (available_atps thy) @ - sort_strings (available_smt_solvers ctxt) + sort_strings (supported_atps thy) @ + sort_strings (SMT_Solver.available_solvers_of ctxt) |> List.partition (String.isPrefix remote_prefix) in - Output.urgent_message ("Available provers: " ^ + Output.urgent_message ("Supported provers: " ^ commas (local_provers @ remote_provers) ^ ".") end @@ -672,7 +670,7 @@ let val thy = ProofContext.theory_of ctxt in if is_smt_prover ctxt name then run_smt_solver auto name - else if member (op =) (available_atps thy) name then + else if member (op =) (supported_atps thy) name then run_atp auto name (get_atp thy name) else error ("No such prover: " ^ name ^ ".") diff -r 1ef01508bb9b -r ab3f6d76fb23 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Feb 08 16:10:09 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Feb 08 16:10:10 2011 +0100 @@ -183,7 +183,7 @@ val (_, hyp_ts, concl_t) = strip_subgoal goal i val no_dangerous_types = types_dangerous_types type_sys val _ = () |> not blocking ? kill_provers - val _ = case find_first (not o is_prover_available ctxt) provers of + val _ = case find_first (not o is_prover_supported ctxt) provers of SOME name => error ("No such prover: " ^ name ^ ".") | NONE => () val _ = if auto then () else Output.urgent_message "Sledgehammering..."