1.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Fri Jul 20 22:19:45 2012 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4      val ord = effective_term_order ctxt atp
     1.5      val _ = problem |> lines_for_atp_problem format ord (K [])
     1.6                      |> File.write_list prob_file
     1.7 -    val path = getenv (List.last (fst exec)) ^ "/" ^ snd exec
     1.8 +    val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
     1.9      val command =
    1.10        File.shell_path (Path.explode path) ^
    1.11        " " ^ arguments ctxt false "" (seconds 1.0) (ord, K [], K []) ^ " " ^

     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 20 22:19:45 2012 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 20 22:19:45 2012 +0200
     2.3 @@ -14,8 +14,7 @@
     2.4  
     2.5    type slice_spec = int * atp_format * string * string * bool
     2.6    type atp_config =
     2.7 -    {exec : string list * string,
     2.8 -     required_vars : string list list,
     2.9 +    {exec : string list * string list,
    2.10       arguments :
    2.11         Proof.context -> bool -> string -> Time.time
    2.12         -> term_order * (unit -> (string * int) list)
    2.13 @@ -87,8 +86,7 @@
    2.14  type slice_spec = int * atp_format * string * string * bool
    2.15  
    2.16  type atp_config =
    2.17 -  {exec : string list * string,
    2.18 -   required_vars : string list list,
    2.19 +  {exec : string list * string list,
    2.20     arguments :
    2.21       Proof.context -> bool -> string -> Time.time
    2.22       -> term_order * (unit -> (string * int) list)
    2.23 @@ -190,8 +188,7 @@
    2.24  val alt_ergo_tff1 = TFF (Polymorphic, TPTP_Explicit)
    2.25  
    2.26  val alt_ergo_config : atp_config =
    2.27 -  {exec = (["WHY3_HOME"], "why3"),
    2.28 -   required_vars = [],
    2.29 +  {exec = (["WHY3_HOME"], ["why3"]),
    2.30     arguments =
    2.31       fn _ => fn _ => fn _ => fn timeout => fn _ =>
    2.32          "--format tff1 --prover alt-ergo --timelimit " ^
    2.33 @@ -263,7 +260,7 @@
    2.34      \--prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
    2.35      \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^
    2.36      e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^
    2.37 -    "(SimulateSOS, " ^
    2.38 +    "(SimulateSOS," ^
    2.39      (e_selection_heuristic_case heuristic
    2.40           e_default_fun_weight e_default_sym_offs_weight
    2.41       |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
    2.42 @@ -303,8 +300,7 @@
    2.43  fun e_kbo () = if is_recent_e_version () then "KBO6" else "KBO"
    2.44  
    2.45  val e_config : atp_config =
    2.46 -  {exec = (["E_HOME"], "eproof"),
    2.47 -   required_vars = [],
    2.48 +  {exec = (["E_HOME"], ["eproof_ram", "eproof"]),
    2.49     arguments =
    2.50       fn ctxt => fn full_proof => fn heuristic => fn timeout =>
    2.51          fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
    2.52 @@ -314,11 +310,7 @@
    2.53          "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^
    2.54          "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
    2.55          e_shell_level_argument full_proof,
    2.56 -   proof_delims =
    2.57 -     (* work-around for bug in "epclextract" version 1.6 *)
    2.58 -     ("# SZS status Theorem\n# SZS output start Saturation.",
    2.59 -      "# SZS output end Saturation.") ::
    2.60 -     tstp_proof_delims,
    2.61 +   proof_delims = tstp_proof_delims,
    2.62     known_failures =
    2.63       [(TimedOut, "Failure: Resource limit exceeded (time)"),
    2.64        (TimedOut, "time limit exceeded")] @
    2.65 @@ -348,8 +340,7 @@
    2.66    THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs)
    2.67  
    2.68  val leo2_config : atp_config =
    2.69 -  {exec = (["LEO2_HOME"], "leo"),
    2.70 -   required_vars = [],
    2.71 +  {exec = (["LEO2_HOME"], ["leo"]),
    2.72     arguments =
    2.73       fn _ => fn _ => fn _ => fn timeout => fn _ =>
    2.74          "--foatp e --atp e=\"$E_HOME\"/eprover \
    2.75 @@ -377,8 +368,7 @@
    2.76    THF (Monomorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
    2.77  
    2.78  val satallax_config : atp_config =
    2.79 -  {exec = (["SATALLAX_HOME"], "satallax"),
    2.80 -   required_vars = [],
    2.81 +  {exec = (["SATALLAX_HOME"], ["satallax"]),
    2.82     arguments =
    2.83       fn _ => fn _ => fn _ => fn timeout => fn _ =>
    2.84          "-p hocore -t " ^ string_of_int (to_secs 1 timeout),
    2.85 @@ -405,8 +395,7 @@
    2.86  
    2.87  (* FIXME: Make "SPASS_NEW_HOME" legacy. *)
    2.88  val spass_config : atp_config =
    2.89 -  {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], "SPASS"),
    2.90 -   required_vars = [],
    2.91 +  {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
    2.92     arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ =>
    2.93       ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
    2.94       |> extra_options <> "" ? prefix (extra_options ^ " "),
    2.95 @@ -447,8 +436,7 @@
    2.96  val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit)
    2.97  
    2.98  val vampire_config : atp_config =
    2.99 -  {exec = (["VAMPIRE_HOME"], "vampire"),
   2.100 -   required_vars = [],
   2.101 +  {exec = (["VAMPIRE_HOME"], ["vampire"]),
   2.102     arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
   2.103       "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
   2.104       " --proof tptp --output_axiom_names on\
   2.105 @@ -491,8 +479,7 @@
   2.106  val z3_tff0 = TFF (Monomorphic, TPTP_Implicit)
   2.107  
   2.108  val z3_tptp_config : atp_config =
   2.109 -  {exec = (["Z3_HOME"], "z3"),
   2.110 -   required_vars = [],
   2.111 +  {exec = (["Z3_HOME"], ["z3"]),
   2.112     arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
   2.113       "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
   2.114     proof_delims = [],
   2.115 @@ -513,8 +500,7 @@
   2.116  (* Not really a prover: Experimental Polymorphic THF and DFG output *)
   2.117  
   2.118  fun dummy_config format type_enc : atp_config =
   2.119 -  {exec = (["ISABELLE_ATP"], "scripts/dummy_atp"),
   2.120 -   required_vars = [],
   2.121 +  {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
   2.122     arguments = K (K (K (K (K "")))),
   2.123     proof_delims = [],
   2.124     known_failures = known_szs_status_failures,
   2.125 @@ -577,8 +563,7 @@
   2.126  
   2.127  fun remote_config system_name system_versions proof_delims known_failures
   2.128                    prem_role best_slice : atp_config =
   2.129 -  {exec = (["ISABELLE_ATP"], "scripts/remote_atp"),
   2.130 -   required_vars = [],
   2.131 +  {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]),
   2.132     arguments = fn _ => fn _ => fn command => fn timeout => fn _ =>
   2.133       (if command <> "" then "-c " ^ quote command ^ " " else "") ^
   2.134       "-s " ^ the_system system_name system_versions ^ " " ^
   2.135 @@ -660,8 +645,8 @@
   2.136  val supported_atps = Symtab.keys o Data.get
   2.137  
   2.138  fun is_atp_installed thy name =
   2.139 -  let val {exec, required_vars, ...} = get_atp thy name () in
   2.140 -    forall (exists (fn var => getenv var <> "")) (fst exec :: required_vars)
   2.141 +  let val {exec, ...} = get_atp thy name () in
   2.142 +    exists (fn var => getenv var <> "") (fst exec)
   2.143    end
   2.144  
   2.145  fun refresh_systems_on_tptp () =

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jul 20 22:19:45 2012 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jul 20 22:19:45 2012 +0200
     3.3 @@ -631,9 +631,8 @@
     3.4  val mono_max_privileged_facts = 10
     3.5  
     3.6  fun run_atp mode name
     3.7 -        ({exec, required_vars, arguments, proof_delims, known_failures,
     3.8 -          prem_role, best_slices, best_max_mono_iters,
     3.9 -          best_max_new_mono_instances, ...} : atp_config)
    3.10 +        ({exec, arguments, proof_delims, known_failures, prem_role, best_slices,
    3.11 +          best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
    3.12          (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
    3.13                      uncurried_aliases, max_facts, max_mono_iters,
    3.14                      max_new_mono_instances, isar_proof, isar_shrink_factor,
    3.15 @@ -660,9 +659,17 @@
    3.16          Path.append (Path.explode dest_dir) problem_file_name
    3.17        else
    3.18          error ("No such directory: " ^ quote dest_dir ^ ".")
    3.19 -    val command =
    3.20 +    val command0 =
    3.21        case find_first (fn var => getenv var <> "") (fst exec) of
    3.22 -        SOME var => Path.explode (getenv var ^ "/" ^ snd exec)
    3.23 +        SOME var =>
    3.24 +        let
    3.25 +          val pref = getenv var ^ "/"
    3.26 +          val paths = map (Path.explode o prefix pref) (snd exec)
    3.27 +        in
    3.28 +          case find_first File.exists paths of
    3.29 +            SOME path => path
    3.30 +          | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ ".")
    3.31 +        end
    3.32        | NONE => error ("The environment variable " ^ quote (hd (fst exec)) ^
    3.33                         " is not set.")
    3.34      fun split_time s =
    3.35 @@ -680,179 +687,162 @@
    3.36            raw_explode #> Scan.read Symbol.stopper time #> the_default 0
    3.37        in (output, as_time t |> Time.fromMilliseconds) end
    3.38      fun run_on prob_file =
    3.39 -      case find_first (forall (fn var => getenv var = ""))
    3.40 -                      (fst exec :: required_vars) of
    3.41 -        SOME home_vars =>
    3.42 -        error ("The environment variable " ^ quote (hd home_vars) ^
    3.43 -               " is not set.")
    3.44 -      | NONE =>
    3.45 -        if File.exists command then
    3.46 +      let
    3.47 +        (* If slicing is disabled, we expand the last slice to fill the entire
    3.48 +           time available. *)
    3.49 +        val actual_slices = get_slices slice (best_slices ctxt)
    3.50 +        val num_actual_slices = length actual_slices
    3.51 +        fun monomorphize_facts facts =
    3.52            let
    3.53 -            (* If slicing is disabled, we expand the last slice to fill the
    3.54 -               entire time available. *)
    3.55 -            val actual_slices = get_slices slice (best_slices ctxt)
    3.56 -            val num_actual_slices = length actual_slices
    3.57 -            fun monomorphize_facts facts =
    3.58 -              let
    3.59 -                val ctxt =
    3.60 -                  ctxt
    3.61 -                  |> repair_monomorph_context max_mono_iters best_max_mono_iters
    3.62 -                          max_new_mono_instances best_max_new_mono_instances
    3.63 -                (* pseudo-theorem involving the same constants as the subgoal *)
    3.64 -                val subgoal_th =
    3.65 -                  Logic.list_implies (hyp_ts, concl_t)
    3.66 -                  |> Skip_Proof.make_thm thy
    3.67 -                val rths =
    3.68 -                  facts |> chop mono_max_privileged_facts
    3.69 -                        |>> map (pair 1 o snd)
    3.70 -                        ||> map (pair 2 o snd)
    3.71 -                        |> op @
    3.72 -                        |> cons (0, subgoal_th)
    3.73 -              in
    3.74 -                Monomorph.monomorph atp_schematic_consts_of rths ctxt
    3.75 -                |> fst |> tl
    3.76 -                |> curry ListPair.zip (map fst facts)
    3.77 -                |> maps (fn (name, rths) =>
    3.78 -                            map (pair name o zero_var_indexes o snd) rths)
    3.79 -              end
    3.80 -            fun run_slice time_left (cache_key, cache_value)
    3.81 -                    (slice, (time_frac, (complete,
    3.82 -                        (key as (best_max_facts, format, best_type_enc,
    3.83 -                                 best_lam_trans, best_uncurried_aliases),
    3.84 -                                 extra)))) =
    3.85 -              let
    3.86 -                val num_facts =
    3.87 -                  length facts |> is_none max_facts ? Integer.min best_max_facts
    3.88 -                val soundness = if strict then Strict else Non_Strict
    3.89 -                val type_enc =
    3.90 -                  type_enc |> choose_type_enc soundness best_type_enc format
    3.91 -                val sound = is_type_enc_sound type_enc
    3.92 -                val real_ms = Real.fromInt o Time.toMilliseconds
    3.93 -                val slice_timeout =
    3.94 -                  ((real_ms time_left
    3.95 -                    |> (if slice < num_actual_slices - 1 then
    3.96 -                          curry Real.min (time_frac * real_ms timeout)
    3.97 -                        else
    3.98 -                          I))
    3.99 -                   * 0.001) |> seconds
   3.100 -                val generous_slice_timeout =
   3.101 -                  Time.+ (slice_timeout, atp_timeout_slack)
   3.102 -                val _ =
   3.103 -                  if debug then
   3.104 -                    quote name ^ " slice #" ^ string_of_int (slice + 1) ^
   3.105 -                    " with " ^ string_of_int num_facts ^ " fact" ^
   3.106 -                    plural_s num_facts ^ " for " ^
   3.107 -                    string_from_time slice_timeout ^ "..."
   3.108 -                    |> Output.urgent_message
   3.109 -                  else
   3.110 -                    ()
   3.111 -                val readable_names = not (Config.get ctxt atp_full_names)
   3.112 -                val lam_trans =
   3.113 -                  case lam_trans of
   3.114 -                    SOME s => s
   3.115 -                  | NONE => best_lam_trans
   3.116 -                val uncurried_aliases =
   3.117 -                  case uncurried_aliases of
   3.118 -                    SOME b => b
   3.119 -                  | NONE => best_uncurried_aliases
   3.120 -                val value as (atp_problem, _, fact_names, _, _) =
   3.121 -                  if cache_key = SOME key then
   3.122 -                    cache_value
   3.123 -                  else
   3.124 -                    facts
   3.125 -                    |> map untranslated_fact
   3.126 -                    |> not sound
   3.127 -                       ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
   3.128 -                    |> take num_facts
   3.129 -                    |> not (is_type_enc_polymorphic type_enc)
   3.130 -                       ? monomorphize_facts
   3.131 -                    |> map (apsnd prop_of)
   3.132 -                    |> prepare_atp_problem ctxt format prem_role type_enc
   3.133 -                                           atp_mode lam_trans uncurried_aliases
   3.134 -                                           readable_names true hyp_ts concl_t
   3.135 -                fun sel_weights () = atp_problem_selection_weights atp_problem
   3.136 -                fun ord_info () = atp_problem_term_order_info atp_problem
   3.137 -                val ord = effective_term_order ctxt name
   3.138 -                val full_proof = debug orelse isar_proof
   3.139 -                val args = arguments ctxt full_proof extra slice_timeout
   3.140 -                                     (ord, ord_info, sel_weights)
   3.141 -                val command =
   3.142 -                  File.shell_path command ^ " " ^ args ^ " " ^
   3.143 -                  File.shell_path prob_file
   3.144 -                  |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1"
   3.145 -                val _ =
   3.146 -                  atp_problem
   3.147 -                  |> lines_for_atp_problem format ord ord_info
   3.148 -                  |> cons ("% " ^ command ^ "\n")
   3.149 -                  |> File.write_list prob_file
   3.150 -                val ((output, run_time), (atp_proof, outcome)) =
   3.151 -                  TimeLimit.timeLimit generous_slice_timeout
   3.152 -                                      Isabelle_System.bash_output command
   3.153 -                  |>> (if overlord then
   3.154 -                         prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
   3.155 -                       else
   3.156 -                         I)
   3.157 -                  |> fst |> split_time
   3.158 -                  |> (fn accum as (output, _) =>
   3.159 -                         (accum,
   3.160 -                          extract_tstplike_proof_and_outcome verbose complete
   3.161 -                              proof_delims known_failures output
   3.162 -                          |>> atp_proof_from_tstplike_proof atp_problem
   3.163 -                          handle UNRECOGNIZED_ATP_PROOF () =>
   3.164 -                                 ([], SOME ProofIncomplete)))
   3.165 -                  handle TimeLimit.TimeOut =>
   3.166 -                         (("", slice_timeout), ([], SOME TimedOut))
   3.167 -                val outcome =
   3.168 -                  case outcome of
   3.169 -                    NONE =>
   3.170 -                    (case used_facts_in_unsound_atp_proof ctxt fact_names
   3.171 -                                                          atp_proof
   3.172 -                          |> Option.map (sort string_ord) of
   3.173 -                       SOME facts =>
   3.174 -                       let
   3.175 -                         val failure =
   3.176 -                           UnsoundProof (is_type_enc_sound type_enc, facts)
   3.177 -                       in
   3.178 -                         if debug then
   3.179 -                           (warning (string_for_failure failure); NONE)
   3.180 -                         else
   3.181 -                           SOME failure
   3.182 -                       end
   3.183 -                     | NONE => NONE)
   3.184 -                  | _ => outcome
   3.185 -              in ((SOME key, value), (output, run_time, atp_proof, outcome)) end
   3.186 -            val timer = Timer.startRealTimer ()
   3.187 -            fun maybe_run_slice slice
   3.188 -                    (result as (cache, (_, run_time0, _, SOME _))) =
   3.189 -                let
   3.190 -                  val time_left = Time.- (timeout, Timer.checkRealTimer timer)
   3.191 -                in
   3.192 -                  if Time.<= (time_left, Time.zeroTime) then
   3.193 -                    result
   3.194 -                  else
   3.195 -                    run_slice time_left cache slice
   3.196 -                    |> (fn (cache, (output, run_time, atp_proof, outcome)) =>
   3.197 -                           (cache, (output, Time.+ (run_time0, run_time),
   3.198 -                                    atp_proof, outcome)))
   3.199 -                end
   3.200 -              | maybe_run_slice _ result = result
   3.201 +            val ctxt =
   3.202 +              ctxt
   3.203 +              |> repair_monomorph_context max_mono_iters best_max_mono_iters
   3.204 +                      max_new_mono_instances best_max_new_mono_instances
   3.205 +            (* pseudo-theorem involving the same constants as the subgoal *)
   3.206 +            val subgoal_th =
   3.207 +              Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy
   3.208 +            val rths =
   3.209 +              facts |> chop mono_max_privileged_facts
   3.210 +                    |>> map (pair 1 o snd)
   3.211 +                    ||> map (pair 2 o snd)
   3.212 +                    |> op @
   3.213 +                    |> cons (0, subgoal_th)
   3.214            in
   3.215 -            ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
   3.216 -             ("", Time.zeroTime, [], SOME InternalError))
   3.217 -            |> fold maybe_run_slice actual_slices
   3.218 +            Monomorph.monomorph atp_schematic_consts_of rths ctxt |> fst |> tl
   3.219 +            |> curry ListPair.zip (map fst facts)
   3.220 +            |> maps (fn (name, rths) =>
   3.221 +                        map (pair name o zero_var_indexes o snd) rths)
   3.222            end
   3.223 -        else
   3.224 -          error ("Bad executable: " ^ Path.print command)
   3.225 +        fun run_slice time_left (cache_key, cache_value)
   3.226 +                (slice, (time_frac, (complete,
   3.227 +                     (key as (best_max_facts, format, best_type_enc,
   3.228 +                              best_lam_trans, best_uncurried_aliases),
   3.229 +                      extra)))) =
   3.230 +          let
   3.231 +            val num_facts =
   3.232 +              length facts |> is_none max_facts ? Integer.min best_max_facts
   3.233 +            val soundness = if strict then Strict else Non_Strict
   3.234 +            val type_enc =
   3.235 +              type_enc |> choose_type_enc soundness best_type_enc format
   3.236 +            val sound = is_type_enc_sound type_enc
   3.237 +            val real_ms = Real.fromInt o Time.toMilliseconds
   3.238 +            val slice_timeout =
   3.239 +              ((real_ms time_left
   3.240 +                |> (if slice < num_actual_slices - 1 then
   3.241 +                      curry Real.min (time_frac * real_ms timeout)
   3.242 +                    else
   3.243 +                      I))
   3.244 +               * 0.001) |> seconds
   3.245 +            val generous_slice_timeout =
   3.246 +              Time.+ (slice_timeout, atp_timeout_slack)
   3.247 +            val _ =
   3.248 +              if debug then
   3.249 +                quote name ^ " slice #" ^ string_of_int (slice + 1) ^
   3.250 +                " with " ^ string_of_int num_facts ^ " fact" ^
   3.251 +                plural_s num_facts ^ " for " ^
   3.252 +                string_from_time slice_timeout ^ "..."
   3.253 +                |> Output.urgent_message
   3.254 +              else
   3.255 +                ()
   3.256 +            val readable_names = not (Config.get ctxt atp_full_names)
   3.257 +            val lam_trans =
   3.258 +              case lam_trans of
   3.259 +                SOME s => s
   3.260 +              | NONE => best_lam_trans
   3.261 +            val uncurried_aliases =
   3.262 +              case uncurried_aliases of
   3.263 +                SOME b => b
   3.264 +              | NONE => best_uncurried_aliases
   3.265 +            val value as (atp_problem, _, fact_names, _, _) =
   3.266 +              if cache_key = SOME key then
   3.267 +                cache_value
   3.268 +              else
   3.269 +                facts
   3.270 +                |> map untranslated_fact
   3.271 +                |> not sound
   3.272 +                   ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
   3.273 +                |> take num_facts
   3.274 +                |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
   3.275 +                |> map (apsnd prop_of)
   3.276 +                |> prepare_atp_problem ctxt format prem_role type_enc atp_mode
   3.277 +                                       lam_trans uncurried_aliases
   3.278 +                                       readable_names true hyp_ts concl_t
   3.279 +            fun sel_weights () = atp_problem_selection_weights atp_problem
   3.280 +            fun ord_info () = atp_problem_term_order_info atp_problem
   3.281 +            val ord = effective_term_order ctxt name
   3.282 +            val full_proof = debug orelse isar_proof
   3.283 +            val args = arguments ctxt full_proof extra slice_timeout
   3.284 +                                 (ord, ord_info, sel_weights)
   3.285 +            val command =
   3.286 +              File.shell_path command0 ^ " " ^ args ^ " " ^
   3.287 +              File.shell_path prob_file
   3.288 +              |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1"
   3.289 +            val _ =
   3.290 +              atp_problem
   3.291 +              |> lines_for_atp_problem format ord ord_info
   3.292 +              |> cons ("% " ^ command ^ "\n")
   3.293 +              |> File.write_list prob_file
   3.294 +            val ((output, run_time), (atp_proof, outcome)) =
   3.295 +              TimeLimit.timeLimit generous_slice_timeout
   3.296 +                                  Isabelle_System.bash_output command
   3.297 +              |>> (if overlord then
   3.298 +                     prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
   3.299 +                   else
   3.300 +                     I)
   3.301 +              |> fst |> split_time
   3.302 +              |> (fn accum as (output, _) =>
   3.303 +                     (accum,
   3.304 +                      extract_tstplike_proof_and_outcome verbose complete
   3.305 +                          proof_delims known_failures output
   3.306 +                      |>> atp_proof_from_tstplike_proof atp_problem
   3.307 +                      handle UNRECOGNIZED_ATP_PROOF () =>
   3.308 +                             ([], SOME ProofIncomplete)))
   3.309 +              handle TimeLimit.TimeOut =>
   3.310 +                     (("", slice_timeout), ([], SOME TimedOut))
   3.311 +            val outcome =
   3.312 +              case outcome of
   3.313 +                NONE =>
   3.314 +                (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof
   3.315 +                      |> Option.map (sort string_ord) of
   3.316 +                   SOME facts =>
   3.317 +                   let
   3.318 +                     val failure =
   3.319 +                       UnsoundProof (is_type_enc_sound type_enc, facts)
   3.320 +                   in
   3.321 +                     if debug then (warning (string_for_failure failure); NONE)
   3.322 +                     else SOME failure
   3.323 +                   end
   3.324 +                 | NONE => NONE)
   3.325 +              | _ => outcome
   3.326 +          in ((SOME key, value), (output, run_time, atp_proof, outcome)) end
   3.327 +        val timer = Timer.startRealTimer ()
   3.328 +        fun maybe_run_slice slice
   3.329 +                (result as (cache, (_, run_time0, _, SOME _))) =
   3.330 +            let
   3.331 +              val time_left = Time.- (timeout, Timer.checkRealTimer timer)
   3.332 +            in
   3.333 +              if Time.<= (time_left, Time.zeroTime) then
   3.334 +                result
   3.335 +              else
   3.336 +                run_slice time_left cache slice
   3.337 +                |> (fn (cache, (output, run_time, atp_proof, outcome)) =>
   3.338 +                       (cache, (output, Time.+ (run_time0, run_time),
   3.339 +                                atp_proof, outcome)))
   3.340 +            end
   3.341 +          | maybe_run_slice _ result = result
   3.342 +      in
   3.343 +        ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
   3.344 +         ("", Time.zeroTime, [], SOME InternalError))
   3.345 +        |> fold maybe_run_slice actual_slices
   3.346 +      end
   3.347  
   3.348      (* If the problem file has not been exported, remove it; otherwise, export
   3.349         the proof file too. *)
   3.350      fun cleanup prob_file =
   3.351        if dest_dir = "" then try File.rm prob_file else NONE
   3.352      fun export prob_file (_, (output, _, _, _)) =
   3.353 -      if dest_dir = "" then
   3.354 -        ()
   3.355 -      else
   3.356 -        File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
   3.357 +      if dest_dir = "" then ()
   3.358 +      else File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
   3.359      val ((_, (_, pool, fact_names, _, sym_tab)),
   3.360           (output, run_time, atp_proof, outcome)) =
   3.361        with_path cleanup export run_on problem_path_name