do the right thing with provers that exist only remotely (e.g. e_sine)
authorblanchet
Thu Feb 13 16:21:43 2014 +0100 (2014-02-13 ago)
changeset 55458d3b72d260d4a
parent 55457 e373c9f60db1
child 55459 1cd927ca8296
do the right thing with provers that exist only remotely (e.g. e_sine)
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Feb 13 15:51:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Feb 13 16:21:43 2014 +0100
     1.3 @@ -197,7 +197,7 @@
     1.4  (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
     1.5     timeout, it makes sense to put E first. *)
     1.6  fun default_provers_param_value mode thy =
     1.7 -  [eN, spassN, z3N, vampireN, e_sineN, yicesN]
     1.8 +  [eN, spassN, z3N, e_sineN, vampireN, yicesN]
     1.9    |> map_filter (remotify_atp_if_not_installed thy)
    1.10    (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
    1.11    |> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Feb 13 15:51:54 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Feb 13 16:21:43 2014 +0100
     2.3 @@ -120,14 +120,12 @@
     2.4  
     2.5  fun remotify_atp_if_not_installed thy name =
     2.6    if is_atp thy name then
     2.7 -    if String.isPrefix remote_prefix name orelse is_atp_installed thy name then
     2.8 -      SOME name
     2.9 -    else
    2.10 -      let val remote_name = remote_prefix ^ name in
    2.11 -        if is_atp thy remote_name then SOME remote_name else NONE
    2.12 -      end
    2.13 +    if String.isPrefix remote_prefix name orelse is_atp_installed thy name then SOME name
    2.14 +    else NONE
    2.15    else
    2.16 -    SOME name
    2.17 +    let val remote_name = remote_prefix ^ name in
    2.18 +      SOME (if is_atp thy remote_name then remote_name else name)
    2.19 +    end
    2.20  
    2.21  type params =
    2.22    {debug : bool,